In: Farn Wang (Eds.): Lecture Notes in Computer Science, 3731: Formal Techniques for Networked and Distributed Systems - FORTE 2005: 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005., pages 189-203. Springer-Verlag, October 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1156243615,.
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.
Keywords: Abstraction, modular verification,(de)composition,Petri nets.