Abstract
In this paper we describe how both, memory and time requirements for stochastic model checking of SPDL (stochastic propositional dynamic logic) formulae can significantly be reduced. SPDL is the stochastic extension of the multi-modal program logic PDL. SPDL provides means to specify path-based properties with or without timing restrictions. Paths can be characterised by so-called programs, essentially regular expressions, where the executability can be made dependent on the validity of test formulae. For model-checking SPDL path formulae it is necessary to build a product transition system (PTS) between the system model and the program automaton belonging to the path formula that is to be verified. In many cases, this PTS can be drastically reduced during the model checking procedure, as the program restricts the number of potentially satisfying paths. Therefore, we propose an approach that directly generates the reduced PTS from a given SPA specification and an SPDL path formula. The feasibility of this approach is shown through a selection of case studies, which show enormous state space reductions, at no increase in generation time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Marsan, M.A., Balbo, G., Conte, G.: A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Transactions on Computer Systems 2(2), 93–122 (1984)
Aziz, A., Shiple, T., Singhal, V., Brayton, R., Sangiovanni-Vincentelli, A.: Formula-Dependent Equivalence for Compositional CTL Model Checking. Form. Methods Syst. Des. 21(2), 193–224 (2002)
Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model Checking Markov Chains with Actions and State Labels. IEEE Transactions on Software Engineering 33(4), 209–224 (2007)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(7), 1–18 (2003)
Bell, A.: Distributed Evaluation of Stochastic Petri Nets. PhD thesis, RWTH Aachen, Fakultät für Mathematik, Informatik und Naturwissenschaften (2003)
Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Ciardo, G., Tilgner, M.: On the use of Kronecker operators for the solution of generalized stochastic Petri nets. Technical Report 96-35, ICASE (1996)
Clarke, E.M., Emerson, E.A., Sistla, A.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In: 10th ACM Annual Symp. on Principles of Programming Languages, pp. 117–126. ACM Press, New York (1983)
Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. System Sci. 18, 194–211 (1979)
Fujita, M., McGeer, P., Yang, J.C.-Y.: Multi-terminal Binary Decision Diagrams: An efficient data structure for matrix representation. Formal Methods in System Design 10(2/3), 149–169 (1997)
Hermanns, H., Herzog, U., Katoen, J.-P.: Process Algebra for Performance Evaluation. Theoretical Computer Science 274(1-2), 43–87 (2002)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: TACAS 2007. LNCS, vol. 4424, pp. 76–92. Springer, Heidelberg (2007)
Kuntz, M.: Symbolic Semantics and Verification of Stochastic Process Algebras. PhD thesis, Universität Erlangen-Nürnberg, Institut für Informatik 7 (2006)
Kuntz, M., Siegle, M.: Deriving symbolic representations from stochastic process algebras. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 188–206. Springer, Heidelberg (2002)
Kuntz, M., Siegle, M., Werner, E.: CASPA - A Tool for Symbolic Performance and Dependability Evaluation. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol. 3236, p. 293. Springer, Heidelberg (2004)
Sanders, W.H., Malhis, L.M.: Dependability Evaluation Using Composed SAN-Based Reward Models. Journal of Parallel and Distributed Computing 15(3), 238–254 (1992)
Siegle, M.: Advances in model representation. In: de Alfaro, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 1–22. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kuntz, M., Haverkort, B.R. (2007). Faster SPDL Model Checking Through Property-Driven State Space Generation. In: Wolter, K. (eds) Formal Methods and Stochastic Models for Performance Evaluation. EPEW 2007. Lecture Notes in Computer Science, vol 4748. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75211-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-75211-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75210-3
Online ISBN: 978-3-540-75211-0
eBook Packages: Computer ScienceComputer Science (R0)