Modular Construction of Finite and Complete Prefixes of Petri net Unfoldings

• Autorzy: Madalinski A. , Fabre E.
• Języki publikacji: EN

Abstrakty

EN

This paper considers distributed systems, defined as a collection of components interacting through interfaces. Components, interfaces and distributed systems are modeled as Petri nets. It is well known that the unfolding of such a distributed system factorises, in the sense that it can be expressed as the composition of unfoldings of its components. This factorised form of the unfolding generally provides a more compact representation of the system runs, because each component does not need to represent the possible choices (conflicts) appearing in the other components. Moreover, the unfolding factorisation makes it possible to analyse the system by parts. The paper focuses on the derivation of a finite and complete prefix (FCP) in the unfolding of a distributed system. Specifically, one would like to directly obtain such a FCP in factorised form, without computing first a FCP of the global distributed system and then factorising it. The construction of such a “modular FCP” is based on deriving summaries of component behaviours w.r.t. their interfaces, that are then communicated to the neighbouring components. The latter combine these summaries with their local behaviours, and prepare interface summaries for the next components. This globally takes the form of a message passing algorithm, where the global system is never considered.

Słowa kluczowe

EN

Petri net; unfoldings; finite complete prefix; distributed systems; modular computation; pullback; category theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 95, nr 1
• Strony: 219--244
• Opis fizyczny: Bibliogr. 20 poz., wykr.

Twórcy

autor

Madalinski A.

autor

Fabre E.

• Facultad de Ciencias de la Ingenieria, Universidad Austral de Chile, Campus Miraflores, General Lagos 2086, Valdivia, Chile,

Bibliografia

• [1] Baldan, P., Haar, S., Kőnig, B.: Distributed Unfolding of Petri Nets, FoSSaCS'06, LNCS 3921, pp. 126-141, 2006.
• [2] Couvreur, J.-M., Grivet, S., Poitrenaud, D.: Unfolding of Products of Symmetrical Petri Nets, Lecture Notes in Computer Science, 2075, 2001, pp. 121-143.
• [3] Engelfriet, J.: Branching Processes of Petri Nets., Acta Informatica, 28, 1991, pp. 575-591, NewsletterInfo: 38, 40.
• [4] Esparza, J., Heljanko, K.: Unfoldings: a Partial-Order Approach to Model Checking, EATCS monographs on Theoretical Computer Science, Springer-Verlag, 2008.
• [5] Esparza, J., Rőmer, S.: An Unfolding Algorithm for Synchronous Products of Transition Systems, International Conference on Concurrency Theory, LNCS 1664, pp. 2-20, 1999.
• [6] Esparza, J., Rőmer, S., Vogler, W.: An Improvement of McMillan's Unfolding Algorithm, Formal methods in systems design, 2002.
• [7] Fabre, E.: Factorization of Unfoldings for Distributed Tile Systems, Part 1 : Reduced Interaction Case, Technical Report 1529, IRISA, April 2003.
• [8] Fabre, E.: Factorization of Unfoldings for Distributed Tile Systems, Part 2 : General Case, Technical Report 1606, IRISA, May 2004.
• [9] Fabre, E.: Distributed Diagnosis based on Trellis Processes, 44th Conf. on Decision and Control (CDC), Seville, Spain, December 2005.
• [10] Fabre, E.: On the Construction of Pullbacks for Safe Petri Nets, Applications and Theory of Petri Nets and other Models of Concurrency, ATPN'06, Turku, Finland, June 2006.
• [11] Fabre, E.: Bayesian Networks of Dynamic Systems, Habilitation Thesis, available at http://www.irisa.fr/distribcom/Personal Pages/fabre/Papiers/hdr.pdf, June 2007.
• [12] Fabre, E., Benveniste, A., Haar, S., Jard, C.: Distributed Monitoring of Concurrent and Asynchronous Systems, Journal of Discrete Event Systems, special issue, May 2005, pp. 33-84.
• [13] Khomenko, V.: Model Checking Based on Petri Net Unfolding Prefixes, Ph.D. Thesis, University of Newcastle upon Tyne, 2002.
• [14] Khomenko, V., Koutny, M., Vogler, W.: Canonical Prefixes of Petri Net Unfoldings, Acta Informatica, Volume 40, Number 2, October 2003, pp. 95-118.
• [15] McMillan, K. L.: Symbolic Model Checking: an approach to the state explosion problem, Ph.D. Thesis, 1992.
• [16] McMillan, K. L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, Proc. International Workshop on Computer Aided Verification, July 1992.
• [17] Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, Event Structures and Domains, Part I, Theor. Computer Science, 13(1), January 1980, pp. 85-108.
• [18] Winskel, G.: A New Definition of Morphism on Petri Nets, STACS '84: Proceedings of the Symposium of Theoretical Aspects of Computer Science, Springer-Verlag, London, UK, 1984, ISBN 3-540-12920-0.
• [19] Winskel, G.: Categories of Models for Concurrency, Seminar on Concurrency, Carnegie-Mellon University, Springer-Verlag, London, UK, 1985, ISBN 3-540-15670-4.
• [20] Winskel, G.: Petri Nets, Algebras, Morphisms, and Compositionality, Information and Computation, 72, 1987, pp. 197-238.