autonomous mobile robot menggunakan metode formal logika temporal linear

Abstract

Logika temporal linear (LTL) dikontruksi dari formulasi logika tingkah laku sistem yang diharapkan dari waktu ke waktu secara linear. Dengan demikian jika pada bagian atau waktu tertentu terjadi kesalahan pada sistem, kesalahan itu dapat segera diantisipasi. Dalam hal ini penggunaan perencanaan logika temporal linear tidak hanya digunakan pada autonomous mobile robot untuk mencapai sebuah tujuan atau menghindari rintangan, tetapi juga untuk perangkaian, perluasan atau penugasan sementara (temporal ordering) pada sebuah rangkaian tugas yang berbeda dalam satu waktu. Dalam LTL untuk menghasilkan lintasan robot dilakukan tiga tahap tahap aktivitas, yaitu pendefinisan abstraksi diskrit pergerakan robot, perencanaan logika temporal menggunakan model checking, dan implementasi kontinu rencana diskret (continuous implementations of discrete plan).