Using splitter ordering heuristics to improve bisimulation in probabilistic model checking

• Autorzy: Mohagheghi Mohammadsadegh , Salehi Khayyam
• Języki publikacji: EN

Abstrakty

EN

Model checking is used to verify computer-based and cyber-physical systems,but faces challenges due to state space explosion. Bisimulation minimization reduces states in transition systems, easing this issue. Probabilistic bisimulation further simplifies models with stochastic behaviors. Recent techniques aim to improve the time complexity of iterative methods in computing probabilistic bisimulation for stochastic systems with nondeterministic behaviors. In this paper, we propose several techniques to accelerate iterative processes to partition the state space of a given probabilistic model to its bisimulation classes. The first technique applies two ordering heuristics for choosing splitter blocks. The second technique uses hash tables to reduce the running time and the average time complexity of the standard iterative method. The proposed approaches are implemented and run on several conventional case studies and reduce the running time by one order of magnitude on average.

Słowa kluczowe

EN

probabilistic bisimulation; Markov decision process; model checking; splitter ordering

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2025
• Tom: T. 26 (2)
• Strony: 1--26
• Opis fizyczny: Bibliogr. 45 poz., rys., tab.

Twórcy

autor

Mohagheghi Mohammadsadegh

• Vali-e-Asr University of Rafsanjan, Department of Computer Science, Rafsanjan, Iran

autor

Salehi Khayyam

• Shahrekord University, Department of Computer Science, Shahrekord, Iran