Quantitative Verification of Stochastic Regular Expressions
Küçük Resim Yok
Tarih
2021
Dergi Başlığı
Dergi ISSN
Cilt Başlığı
Yayıncı
Ios Press
Erişim Hakkı
info:eu-repo/semantics/closedAccess
Özet
In this article, we introduce a probabilistic verification algorithm for stochastic regular expressions over a probabilistic extension of the Action based Computation Tree Logic (ACTL*). The main results include a novel model checking algorithm and a semantics on the probabilistic action logic for stochastic regular expressions (SREs). Specific to our model checking algorithm is that SREs are defined via local probabilistic functions. Such functions are beneficial since they enable to verify properties locally for sub-components. This ability provides a flexibility to reuse the local results for the global verification of the system; hence, the framework can be used for iterative verification. We demonstrate how to model a system with an SRE and how to verify it with the probabilistic action based logic and present a preliminary performance evaluation with respect to the execution time of the reachability algorithm.
Açıklama
Anahtar Kelimeler
quantitative verification, probabilistic verification, formal models, stochastic regular expressions, probabilistic regular expressions, stochastic algebra, action based logic
Kaynak
Fundamenta Informaticae
WoS Q Değeri
Q3
Scopus Q Değeri
Q3
Cilt
179
Sayı
2
