MODEL CHECKING FOR PARAMETRIC DISCRETE-TIME MARKOV CHAINS

Pengecekan model sistem stokastik, seperti parametric discrete-time Markov chain, dilakukan dengan metode numerik atau statistik. Tujuan dari penelitian ini adalah untuk membandingkan kedua metode perihal waktu eksekusi dan akurasi dan presisi, dan untuk menyarankan penggunaan satu metode di atas yang lain untuk kondisi tertentu. Pendekatan numerik dan statistik untuk parametric discrete-time Markov chain akan dibandingkan dengan menggunakan pemeriksa model PRISM, dengan IPv4 Zeroconf Protocol dan Crowds Protocol sebagai contoh model parametrik. Program Python dirancang untuk menjalankan beberapa perintah PRISM, mengumpulkan hasilnya, dan menghasilkan data untuk analisis. Pendekatan numerik akan menghasilkan persamaan probabilitas untuk properti dalam hal variabel parametric discrete-time Markov chain, yang kemudian digunakan untuk menghitung nilai probabilitas untuk variabel. Nilai-nilai tersebut kemudian dibandingkan dengan nilai yang dihasilkan dari pengecekan model statistik untuk menganalisis akurasi, presisi, dan kinerja. Hasil pendekatan statistik dihasilkan menggunakan selang kepercayaan. Hasil eksperimen menunjukkan bahwa metode numerik memiliki waktu eksekusi yang lebih cepat dibandingkan dengan metode statistik untuk verifikasi IPv4 Zeroconf Protocol, yang dianggap sebagai sistem kecil dan sederhana. Namun, untuk Crowds Protocol, model yang besar dan kompleks, waktu yang dibutuhkan untuk pengecekan model numerik meningkat secara eksponensial, membuatnya tidak efektif dalam waktu dan memori. Selain itu, membandingkan hasil statistik dengan yang numerik, akurasi untuk hasil statistik ditentukan menjadi rendah untuk nilai probabilitas mendekati 0, dan ketepatan untuk hasil statistik juga ditentukan menjadi rendah untuk nilai probabilitas mendekati 0. Model checking of stochastic systems, including parametric discrete-time Markov chains, is done with either numerical or statistical methods. The purpose of this research is to perform comparison of the two model checking methods in terms of execution time and accuracy and precision, and to suggest the use of one method over the other for certain conditions. The numerical and statistical approaches for parametric discrete-time Markov chains will be compared using PRISM model checker, with IPv4 Zeroconf Protocol and Crowds Protocol as the parametric model examples. A Python program is designed to run multiple PRISM commands, collect the results, and generate data for analysis. The numerical approach will generate a probability equation for a property in terms of the parametric variables of the Markov chain, which is then used to calculate probability values for the variables. The values are then compared with the resulting values from statistical model checking to analyze the accuracy, precision, and performance. The statistical approach outcomes are generated using confidence interval. The results of the experiments show that the numerical method has a faster execution time compared to the statistical one for verification IPv4 Zeroconf Protocol, considered a small and simple system. However, for Crowds Protocol, a large and complex model, the time taken for numerical model checking exponentially increases, rendering it ineffective in terms of time and memory. In addition, comparing statistical results to numerical ones, the accuracy for statistical results are determined to be low for probability values near 0, and the precision for statistical results are also determined to be low for probability values near 0.