| Abstrak |
: |
Penelitian ini diinspirasikan oleh kebutuhan desain kontrol navigasi robot FATETA pada KRCI 2006. KRCI (Kontes Robot Cerdas Indonesia) adalah kontes robot yang diselenggarakan di Indonesia setiap tahunnya. Aturan kontes mensyaratkan robot mengunjungi setiap ruangan tepat 1 (satu) kali. FATETA pada waktu itu membuat robot desain kontrol navigasi yang tidak diformaisasi, sehingga sangat mungkin bagi robot untuk gagal kembali ke starting point (tempat start), menemukan ruangan yang belum dikunjungi, dan mengunjungi ruangan lebih dali 1 (satu) kali. Tujuan penelitian ini adalah membangun prototipe sistem navigasi mobile robot yang dispesifikasikan dengan bahasa spesifikasi Linear Temporal Logic (LTL) dan terverifikasi. Sedangkan untuk metodologi penelitian adalah merumuskan sistem informal, menspesifikasikan sistem secara formal, melakukan verifikasi prototipe sistem, dan merekomendasikan hasil prototipe tersebut untuk diterapkan. Akhirnya hasil dari penelitian telah membuktikan Linear Temporal Logic (LTL) melalui prototipe tersebut dapat memecahkan masalah kendali navigasi, sehingga prototipe ini dapat diusulkan untuk digunakan oleh robot FATETA dan atau siapa saja pada kontes robot berikutnya. |
Dosen & Pendukung 
