<![CDATA[Dalam penelitian ini dibahas mengenai cara untuk melakukan verifikasi terhadap sistem penjadwalan keberangkatan kereta api atas Aljabar Max-Plus berdasarkan suatu property keamanan yang akan diamati. Lebih khusus, sistem yang digunakan sebagai representasi dari sistem penjadwalan keberangkatan kereta api, yaitu: Sistem uncertain Max-Plus Linear (uMPL). Sistem uMPL tersebut dapat dikonstruksi berdasarkan graf berarah yang merepresentasikan jalur lintasan kereta api. Jika diberikan suatu Sistem uMPL autonomous yang merepresentasikan sistem penjadwalan keberangkatan kereta api, maka proses untuk melakukan verifikasi keamanan terhadap sistem tersebut berdasarkan property yang diberikan dapat dilakukan dengan menggunakan analisis reachability. Lebih lanjut, jika diberikan Sistem uMPL, suatu initial conditions yang tak kosong, time horizon, dan unsafe set, maka verifikasi keamanan terhadap Sistem uMPL dapat dilakukan dengan melihat apakah state dari sistem tersebut mampu mencapai unsafe set atau tidak. Jika state dari Sistem uMPL mampu mencapai unsafe set berdasarkan time horizon yang diberikan, maka Sistem uMPL tersebut tidak aman. Sebaliknya, jika state sistem tidak mampu mencapai unsafe set berdasarkan time horizon yang diberikan, maka sistem tersebut dikatakan aman.]]>
