2017 : ABSTRAKSI BERHINGGA PADA PETRI NET DAN APLIKASINYA PADA SISTEM ANTRIAN

Dr. Subiono M.Sc.
Dr. Dieky Adzkiya S.Si, M.Si

External link

Type

RESEARCH

Keywords

-


Abstract

Petri net dapat digunakan untuk memodelkan sistem event diskrit yang mengandung sinkronisasi dan konkurensi. Model ini telah diterapkan pada banyak aplikasi, misalnya pada pemodelan sistem antrian, sistem inventori, sistem pengolahan air. Di literatur, sifat-sifat yang dapat dianalisis terbatas pada boundedness, liveness, reachability dan coverability. Penelitian ini bertujuan untuk mengembangkan sebuah metode yang dapat digunakan untuk menganalisis banyak sifat dari Petri net. Sifat-sifat tersebut diekspresikan ke dalam sebuah spesikasi yang dikenal dengan linear temporal logic (LTL).\n\nProses untuk mengetahui apakah sebuah model memenuhi sebuah spesikasi disebut verikasi. Pada penelitian ini, model yang digunakan adalah Petri net dan spesikasi yang digunakan adalah LTL. Jika kardinalitas ruang keadaan berhingga, salah satu perangkat lunak yang mampu melakukan verikasi secara otomatis adalah SPIN. Kenyataannya kardinalitas ruang keadaan suatu Petri net tidak selalu berhingga. Hal ini mendorong dilakukannya suatu penelitian untuk mengembangkan metode abstraksi berhingga pada Petri net. Abstraksi adalah sebuah konsep fundamental yang memungkinan analisis (atau verikasi) dari sebuah model dengan kardinalitas dari ruang keadaan yang besar atau bahkan takhingga. Jadi tujuan dari penelitian ini adalah mengembangkan sebuah metode yang memungkinkan untuk menganalisis banyak sifat dari Petri net dan prosesnya berlangsung secara otomatis.\n\nSebagai studi kasus dari penelitian ini, Penulis memilih sistem antrian karena sistem ini banyak dipakai pada kehidupan sehari-hari (antrian pada bank, supermarket, persimpangan jalan dll), manufaktur, dll. Meskipun pada penelitian ini aplikasi yang dibahas adalah sistem antrian, metode ini juga dapat diterapkan pada aplikasi-aplikasi yang lain dari Petri net.