×

Static analysis techniques for parameterised Boolean equation systems. (English) Zbl 1234.68263

Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 230-245 (2009).
Summary: Parameterised Boolean Equation Systems (PBESs) can be used to encode and solve various types of model checking and equivalence checking problems. PBESs are typically solved by symbolic approximation or by instantiation to Boolean Equation Systems (BESs). The latter technique suffers from something similar to the state space explosion problem and we propose to tackle it by static analysis techniques, which we tailor for PBESs. We introduce a method to eliminate redundant parameters and a method to detect constant parameters. Both lead to a better performance of the instantiation and they can sometimes even reduce problems that are intractable due to the infinity of the underlying BES to tractable ones.
For the entire collection see [Zbl 1157.68007].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q65 Abstract data types; algebraic specification
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized boolean equation systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 120–135. Springer, Heidelberg (2007) · Zbl 1151.68521 · doi:10.1007/978-3-540-74407-8_9
[2] Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
[3] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977) · Zbl 1149.68389 · doi:10.1145/512950.512973
[4] van Dam, A., Ploeger, B., Willemse, T.A.C.: Instantiation for parameterised boolean equation systems. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 440–454. Springer, Heidelberg (2008) · Zbl 1161.68596 · doi:10.1007/978-3-540-85762-4_30
[5] Gallardo, M.M., Joubert, C., Merino, P.: Implementing influence analysis using parameterised boolean equation systems. In: Proc. ISOLA 2006. IEEE Comp. Soc. Press, Los Alamitos (2006)
[6] Groote, J.F., Lisser, B.: Computer assisted manipulation of algebraic process specifications. SIGPLAN Notices 37(12), 98–107 (2002) · doi:10.1145/636517.636531
[7] Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Sci. Comput. Program 56(3), 251–273 (2005) · Zbl 1082.68067 · doi:10.1016/j.scico.2004.08.002
[8] Groote, J.F., Willemse, T.A.C.: Parameterised boolean equation systems. Theor. Comput. Sci. 343(3), 332–369 (2005) · Zbl 1077.68061 · doi:10.1016/j.tcs.2005.06.016
[9] Hentze, N., McAllester, D.: Linear-time subtransitive control flow analysis. In: Proc. PLDI 1997. ACM, New York (1997)
[10] Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 155. Springer, Heidelberg (2001) · Zbl 0987.68849 · doi:10.1007/3-540-45309-1_11
[11] Mateescu, R.: Local model-checking of an alternation-free value-based modal mu-calculus. In: Proc. 2nd Int’l Workshop on VMCAI (September 1998)
[12] Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008) · Zbl 05293133 · doi:10.1007/978-3-540-68237-0_12
[13] Orzan, S., Willemse, T.A.C.: Invariants for parameterised boolean equation systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 187–202. Springer, Heidelberg (2008) · Zbl 1160.68446 · doi:10.1007/978-3-540-85361-9_18
[14] van de Pol, J.C., Valero Espada, M.: Modal abstractions in {\(\mu\)}CRL*. In: Proc. AMAST (2004) · Zbl 1108.68533 · doi:10.1007/978-3-540-27815-3_32
[15] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Mathematics 5(2), 285–309 (1955) · Zbl 0064.26004 · doi:10.2140/pjm.1955.5.285
[16] Watanabe, H., Nishizawa, K., Takaki, O.: A coalgebraic representation of reduction by cone of influence. In: Proc. of Workshop on Coalgebraic Methods in Computer Science, vol. 164(1), pp. 177–194 (2006) · Zbl 1276.68112 · doi:10.1016/j.entcs.2006.06.011
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.