Abstract
When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (Ltss), and whose temporal properties of interest can be formulated in modal μ-calculus (L μ ). First, we determine, for any L μ formula, the maximal set of actions that can be hidden in the Lts without changing the interpretation of the formula. Then, we define \(L_\mu^{\it dsbr}\), a fragment of L μ which is compatible with divergence-sensitive branching bisimulation. This enables us to apply the maximal hiding and to reduce the Lts on-the-fly using divergence-sensitive τ-confluence during the verification of any \(L_\mu^{\it dsbr}\) formula. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of on-the-fly verification.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, H.R.: Model checking and boolean graphs. Theoretical Computer Science 126(1), 3–30 (1994)
Baeten, J.C.M.: A Brief History of Process Algebra. Theoretical Computer Science 335(2-3), 131–146 (2005)
Barbuti, R., de Francesco, N., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. Journal of Computer and System Science 59(3), 537–556 (1999)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design 2(2), 121–147 (1993)
Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 128–142. Springer, Heidelberg (2010)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of ICSE 1999 (May 1999)
Fantechi, A., Gnesi, S., Ristori, G.: From ACTL to Mu-Calculus. In: Proc. of the ERCIM Workshop on Theory and Practice in Verification, IEI-CNR (1992)
Fernandez, J.-C., Mounier, L.: On the fly verification of behavioural equivalences and preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)
Garavel, H., Lang, F.: Svl: a scripting language for compositional verification. In: Proc. of FORTE 2001, IFIP, pp. 377–392. Kluwer Academic Publishers, Boston (August 2001); Full Version available as INRIA Research Report RR-4223
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2010: A toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
van Glabbeek, R.J., Luttik, B., Trčka, N.: Branching Bisimilarity with Explicit Divergence. Fundamenta Informaticae 93(4), 371–392 (2009)
van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), 555–600 (1996)
Groote, J.F., Sellink, M.P.A.: Confluence for process verification. Theoretical Computer Science 170(1-2), 47–81 (1996)
Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Mateescu, R.: On-the-fly state space reductions for weak equivalences. In: Proc. of FMICS 2005, pp. 80–89. ACM Computer Society Press, New York (2005)
Mateescu, R.: Caesar_solve: A generic library for on-the-fly resolution of alternation-free boolean equation systems. Springer International Journal on Software Tools for Technology Transfer (STTT) 8(1), 37–56 (2006); Full version available as INRIA Research Report RR-5948 (July 2006)
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Science of Computer Programming 46(3), 255–281 (2003)
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Mateescu, R., Wijs, A.: Efficient on-the-fly computation of weak tau-confluence. Research Report RR-7000, INRIA (2009)
Mateescu, R., Wijs, A.: Sequential and distributed on-the-fly computation of weak tau-confluence. Science of Computer Programming (2011) (to appear)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
De Nicola, R., Vaandrager, F.W.: Action versus State Based Logics for Transition Systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Pace, G.J., Lang, F., Mateescu, R.: Calculating τ-confluence compositionally. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 446–459. Springer, Heidelberg (2003)
Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelburg (2001)
Streett, R.: Propositional dynamic logic of looping and converse. Information and Control (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mateescu, R., Wijs, A. (2011). Property-Dependent Reductions for the Modal Mu-Calculus. In: Groce, A., Musuvathi, M. (eds) Model Checking Software. SPIN 2011. Lecture Notes in Computer Science, vol 6823. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22306-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-22306-8_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22305-1
Online ISBN: 978-3-642-22306-8
eBook Packages: Computer ScienceComputer Science (R0)