Quantitative Verification of Stochastic Regular Expressions

• Autorzy: Getir Yaman Sinem , Pavese Esteban , Grunske Lars

Identyfikatory

DOI

10.3233/FI-2021-2018

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

action based logic; formal models; probabilistic regular expressions; probabilistic verification; quantitative verification; stochastic algebra; stochastic regular expressions

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 179, nr 2
• Strony: 135--163
• Opis fizyczny: Bibliogr. 24 poz., rys., tab.

Twórcy

autor

Getir Yaman Sinem

• Humboldt University, Berlin, Germany
• Ege University, Izmir, Turkey

autor

Pavese Esteban

• Humboldt University, Berlin, Germany

autor

Grunske Lars

• Humboldt University, Berlin, Germany

Bibliografia

• [1] McIver A, Rabehaja TM, Struth G. Probabilistic Concurrent Kleene Algebra. In: Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013. 2013 pp. 97-115. doi:10.4204/EPTCS.117.7.
• [2] Kartzow A, Weidner T. Model Checking Constraint LTL over Trees. CoRR, 2015.
• [3] Weidner T. Probabilistic Logic, Probabilistic Regular Expressions, and Constraint Temporal Logic. PhD dissertation, University Leipzig, 2012.
• [4] Getir S, Pavese E, Grunske L. Formal Semantics for Probabilistic Verification of Stochastic Regular Expressions. In: Proceedings of the 27th International Workshop on Concurrency, Specification and Programming, Berlin, Germany, September 24-26, 2018. 2018.
• [5] Katoen JP. The Probabilistic Model Checking Landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16. ACM. ISBN 978-1-4503-4391-6, 2016 pp. 31-45. doi:10.1145/2933575.2934574. URL http://doi.acm.org/10.1145/2933575.2934574.
• [6] Kwiatkowska M, Norman G, Parker D. Probabilistic model checking in practice: Case studies with PRISM. ACM SIGMETRICS Performance Evaluation Review, 2005. 32(4):16-21.
• [7] Baier C, Katoen JP. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. ISBN 026202649X, 9780262026499.
• [8] Marsan MA. Stochastic Petri nets: An elementary introduction. In: Rozenberg G (ed.), Advances in Petri Nets 1989. Springer Berlin Heidelberg, 1990 pp. 1-29.
• [9] Ghezzi C. Evolution, Adaptation, and the Quest for Incrementality. In: Monterey Workshop. 2012 pp. 369-379.
• [10] Ross BJ. Probabilistic Pattern Matching and the Evolution of Stochastic Regular Expressions. Applied Intelligence, 2000. 13(3):285-300.
• [11] Baier C, Cloth L, Haverkort BR, Kuntz M, Siegle M. Model Checking Markov Chains with Actions and State Labels. IEEE Trans. Software Eng., 2007. 33(4):209-224. doi:10.1109/TSE.2007.36.
• [12] Rabin MO. Probabilistic Automata. Information and Control, 1963. 6(3):230-245. doi:10.1016/S0019-9958(63)90290-0.
• [13] Garg VK, Kumar R, Marcus SI. A probabilistic language formalism for stochastic discrete-event systems. IEEE Transactions on Automatic Control, 1999. 44(2):280-293. doi:10.1109/9.746254.
• [14] Kumar R, Garg VK. Control of stochastic discrete event systems modeled by probabilistic languages. IEEE Trans. Automat. Contr., 2001. 46(4):593-606. doi:10.1109/9.917660.
• [15] Stoy JE. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1981. ISBN 0262690764.
• [16] De Nicola R, Vaandrager F. Action versus state based logics for transition systems. In: Guessarian I (ed.), Semantics of Systems of Concurrent Processes. Springer Berlin Heidelberg. ISBN 978-3-540-46897-4, 1990 pp. 407-419.
• [17] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994. 6(5):512-535. doi:10.1007/BF01211866.
• [18] Grunske L. Specification patterns for probabilistic quality properties. In: Schäfer W, Dwyer MB, Gruhn V (eds.), 30th International Conference on Software Engineering (ICSE 2008). ACM, 2008 pp. 31-40. doi:10.1145/1368088.1368094. URL https://doi.org/10.1145/1368088.1368094.
• [19] Thomo A. Implication of regular expressions. Appl. Math. Lett., 2012. 25(10):1394-1398. doi:10.1016/j.aml.2011.12.009. URL https://doi.org/10.1016/j.aml.2011.12.009.
• [20] Leucker M, Sánchez C. Regular Linear Temporal Logic. In: Jones CB, Liu Z, Woodcock J (eds.), Theoretical Aspects of Computing - ICTAC 2007. Springer Berlin Heidelberg, 2007 pp. 291-305.
• [21] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan G, Qadeer S (eds.), Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS. Springer, 2011 pp. 585-591.
• [22] Etessami K, Stewart A, Yannakakis M. Stochastic Context-Free Grammars, Regular Languages, and Newton’s Method. In: Fomin FV, Freivalds R, Kwiatkowska M, Peleg D (eds.), Automata, Languages, and Programming. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-39212-2, 2013 pp. 199-211.
• [23] Bollig B, Gastin P, Monmege B, Zeitoun M. A Probabilistic Kleene Theorem. In: Automated Technology for Verification and Analysis -10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings. 2012 pp. 400-415. doi:10.1007/978-3-642-33386-6\_31.
• [24] Comon H. Tree Automata Techniques and Applications. http://www.grappa.univ-lille3.fr/tata, 1997. URL https://ci.nii.ac.jp/naid/10017663851/en/.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).