Abstract
In this paper, we address the modular verification problem for a Petri net obtained by composition of two subnets. At first, we show how to transform an asynchronous composition into a synchronous one where the new subnets are augmented from the original ones by means of linear invariants. Then we introduce a non-constraining rela- tion between subnets based on their behaviour. Whenever this relation is satisfied, standard properties like the liveness and the boundedness and generic properties specified by a linear time logic may be checked by examination of the augmented subnets in isolation. Finally, we give a sufficient condition for this relation which can be detected modularly using an efficient algorithm.
Chapter PDF
Similar content being viewed by others
References
Benalycherif, M.-L., Girault, C.: Behavioural and structural composition rules preserving liveness by synchronisation for colored FIFO nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 73–92. Springer, Heidelberg (1996)
Christensen, S., Petrucci, L.: Modular analysis of petri nets. Computer Journal 43(3), 224–242 (2000)
Haddad, S., Ilié, J.-M., Klai, K.: An incremental verification technique using decomposition of petri net. In: Proc. of the IEEE SMC 2002 - Systems, Man and Cybernetics, Hammamet, Tunisia (2002)
Haddad, S., Ilié, J.-M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Proc. of Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3 (2004)
Ilié, J.-M., Klai, K., Zouari, B.: A modular verification methodology for dnri petri nets. In: Proc. of the International Conference ACS/IEEE 2003 on Computer Systems and Applications (AICCSA-2003), Tunis, Tunisia, pp. 14–18 (2003)
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)
Noord, V.: Treatment of epsilon moves in subset construction. In: Computational Linguistics, MIT Press for the Association for Computational Linguistics, vol. 26 (2000)
Santone, A.: Compositionality for Improving Model Checking. In: Proc. of FORTE 2000, in Proc. of Formal Methods for Distributed System Development (October 2000)
Sibertin-Blanc, C.: A client-server protocol for composition of Petri nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691. Springer, Heidelberg (1993)
Souissi, Y., Memmi, G.: Compositions of nets via a communication medium. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 457–470. Springer, Heidelberg (1991)
Valmari, A.: Compositional state space generation. In: Proc. of ICATPN 1990, LNCS (May 1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Klai, K., Haddad, S., Ilié, JM. (2005). Modular Verification of Petri Nets Properties: A Structure-Based Approach. In: Wang, F. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2005. FORTE 2005. Lecture Notes in Computer Science, vol 3731. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562436_15
Download citation
DOI: https://doi.org/10.1007/11562436_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29189-3
Online ISBN: 978-3-540-32084-5
eBook Packages: Computer ScienceComputer Science (R0)