ABSTRAK

Pada karya tulis ini kami melakukan investigasi mengenai keterkaitan antara logika temporal Allen (Allen’s temporal logic, ATL) dengan dua logika temporal in- terval lain, yaitu logika lingkungan kanan proposisi (right propositional neighborhood logic, RPNL) dan kalkulus durasi terrestriksi berbasis logika lingkungan kanan (right neighborhood logic-based restricted duration calculus, RNL-RDC). Kami mende…ni- sikan dua varian dari ATL, yaitu ATL+ B dan ATL􀀀B yang keduanya diinterpretasikan pada model atas sebarang struktur urutan linier yang terbatas bawah. Kami me- nunjukkan bahwa setiap formula pada ATL+ B dan ATL􀀀B secara berturutan dapat ditranslasikan dalam waktu linier ke formula yang ekui-terpenuhi (equisatis…able) pada RPNL dan RNL-RDC. Penelitian kami didasarkan pada hasil penelitian yang dilakukan oleh Ro¸su dan Bensalem (2006) yang berhasil mentranslasikan setiap formula pada ALTL (suatu varian dari ATL yang diinterpretasikan pada model atas sebarang struktur urutan linier diskrit yang terbatas bawah) ke formula yang ekui-terpenuhi pada LTL (linear- time temporal logic, logika temporal linier). Dari karya tulis ini diperoleh dua hal penting. Pertama, veri…kasi terhadap suatu sistem yang spesi…kasinya dideskrip- sikan menggunakan formula ATL+ B dan ATL􀀀B secara berturutan dapat dilakukan menggunakan metode veri…kasi untuk RPNL dan RNL-RDC. Kedua, translasi dari ATL+ B ke RPNL juga mengakibatkan keterputusan (decidability) dari masalah keter- penuhan formula (satis…ability problem) untuk ATL+ B atas semua jenis struktur urutan linier.