Abstract
Model-checking is a powerful and widespread technique for the verification of finite state concurrent systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. Modular verification is a promising natural approach to tackle this problem. It is based on the ”divide and conquer” principle and aims at deducing the properties of the system from those of its components analysed in isolation. Unfortunately, several issues make the use of modular verification techniques difficult in practice. First, deciding how to partition the system into components is not trivial and can have a significant impact on the resources needed for verification. Second, when model-checking a component in isolation, how should the environment of this component be described? In this paper, we address these problems in the framework of model-checking LTL∖X action-based properties on Petri nets. We propose an incremental and modular verification approach where the system model is partitioned according to the actions occurring in the property to be verified and where the environment of a component is taken into account using the linear place invariants of the system.
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
Bhat, G., Peled, D.: Adding partial orders to linear temporal logic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 119–134. Springer, Heidelberg (1997)
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Christensen, S., Petrucci, L.: Søren Christensen and Laure Petrucci. Computer Journal 43(3), 224–242 (2000)
Cobleigh, J., Giannakopoulou, D., Pasareanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, Springer, Heidelberg (2003)
Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 253–271. Springer, Heidelberg (1999)
Couvreur, J.-M.: A bdd-like implementation of an automata package. In: CIAA 2004. LNCS, vol. 3317, pp. 310–311. Springer, Heidelberg (2004)
Geldenhuys, J., Valmari, A.: Techniques for smaller intermediary bdds. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 233–247. Springer, Heidelberg (2001)
Girault, C., Valk, R.: Petri Nets for Systems Engineering — A Guide to Modeling, Verification, and Applications. Springer, Heidelberg (2003)
Haddad, S., Ilié, J.-M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, Springer, Heidelberg (2004)
Henzinger, T.A., Kupferman, O., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 514–529. Springer, Heidelberg (1996)
Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Springer, Three Volumes (1997)
Klai, K., Haddad, S., Ilié, J.-M.: Modular verification of Petri nets properties: A structure-based approach. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 189–203. Springer, Heidelberg (2005)
Lakos, C., Petrucci, L.: Modular analysis of systems composed of semiautonomous subsystems. In: Int.Conf. on Application of Concurrency to System Design (ACSD), pp. 185–194. IEEE Comp. Soc. Press, Los Alamitos (2004)
Latvala, T., Mäkelä, M.: LTL model-checking for modular Petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 298–311. Springer, Heidelberg (2004)
McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 312–327. Springer, Heidelberg (2000)
Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986)
Sibertin-Blanc, C.: A client-server protocol for composition of Petri nets. In: Ajmone Marsan, M. (ed.) Application and Theory of Petri Nets 1993. LNCS, vol. 691, Springer, Heidelberg (1993)
Souissi, Y., Memmi, G.: Compositions of nets via a communication medium. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 457–470. Springer, Heidelberg (1991)
Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design 1(4), 297–322 (1992)
Valmari, A.: Composition and abstraction. In: Valmari, A. (ed.) MOVEP. LNCS, vol. 2067, pp. 58–98. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Klai, K., Petrucci, L., Reniers, M. (2007). An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets. In: Derrick, J., Vain, J. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2007. FORTE 2007. Lecture Notes in Computer Science, vol 4574. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73196-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-73196-2_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73195-5
Online ISBN: 978-3-540-73196-2
eBook Packages: Computer ScienceComputer Science (R0)