Bus Rapid Transit (BRT) adalah transportasi publik yang menjadi solusi dari kemacetan. Jalur khusus BRT ini menggunakan sistem jalur lawan arus agar dapat mengurangi peman-faatan jalur oleh kendaraan non-BRT. Sistem lampu lalu lintas dengan jalur lawan arus pada BRT ini mempunyai masalah ketika diterapkan di persimpangan. Pada penelitian se-belumnya, sistem lalu lintas ini telah dibangun dengan model Linear Temporal Logic (LTL). Namun, sistem yang dibangun tidak memaksimalkan jumlah lampu hijau yang menyala. Hal ini mengakibatkan jumlah transisi lampu lalu lintas pada setiap state yang diajukan untuk persimpangan terlalu banyak. Oleh karena itu, dibangun sistem lalu lintas dengan cara me-maksimalkan jumlah lampu hijau yang menyala dan mereduksi jumlah transisi lampu pada setiap state. Kemudian sistem lampu lalu lintas akan dikembangkan dengan model timed automata yang dapat menangani kendala waktu. Model LTL dikonstruksi ke dalam timed automata menggunakan model checker UPPAAL dengan bahasa Timed Computation Tree Logic (TCTL). Hasil pemodelan sistem lalu lintas yang dibangun dengan LTL dan timed automata diveri kasi terkait spesi kasi keamanan, ketercapaian dan keadilan.