nach oben

Erschienen in:

2014 | OriginalPaper | Buchkapitel

A Canonical Contraction for Safe Petri Nets

verfasst von : Thomas Chatain, Stefan Haar

Erschienen in: Transactions on Petri Nets and Other Models of Concurrency IX

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Under maximal semantics, the occurrence of an event \(a\) in a concurrent run of an occurrence net may imply the occurrence of other events, not causally related to \(a\), in the same run. In recent works, we have formalized this phenomenon as the reveals relation, and used it to obtain a contraction of sets of events called facets in the context of occurrence nets. Here, we extend this idea to propose a canonical contraction of general safe Petri nets into pieces of partial-order behaviour which can be seen as “macro-transitions” since all their events must occur together in maximal semantics. On occurrence nets, our construction coincides with the facets abstraction.Our contraction preserves the maximal semantics in the sense that the maximal processes of the contracted net are in bijection with those of the original net.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Modeling Organizational Structures and Agent Knowledge for Mulan Applications

Nächstes Kapitel Symbolic Termination and Confluence Checking for ECA Rules

Notice that \((B, E, F, {^{\bullet }{E'}} \setminus {{E'}^{\bullet }})\) is not an occurrence net in general: it satisfies items 3, 4 and 5 of Definition 2, but items 1 and 2 may not hold.

The depth of an event \(e\) is the size of the longest path from an initial condition to \(e\).

By “\(\phi \) starts by \(t\)”, we mean that there exists an event in \(\phi \) which is mapped to \(t\) and consumes only initial conditions of \(\phi \).

Balaguer, S., Chatain, T., Haar, S.: Building tight occurrence nets from reveals relations. In: Proceedings of the 11th International Conference on Application of Concurrency to System Design, pp. 44–53. IEEE Computer Society Press (2011)

Balaguer, S., Chatain, T., Haar, S.: Building occurrence nets from reveals relations. Fundam. Inform. 123(3), 245–272 (2013)MATHMathSciNet

Berthelot, G.: Checking properties of nets using transformation. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222, pp. 19–40. Springer, Heidelberg (1986)CrossRef

Best, E., Randell, B.: A formal model of atomicity in asynchronous systems. Acta Inform. 16(1), 93–124 (1981)CrossRefMATH

Desel, J., Merceron, A.: Vicinity respecting homomorphisms for abstracting system requirements. In: Proceedings of International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC) (2009)

Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Trans. Autom. Control 55(10), 2310–2320 (2010)CrossRefMathSciNet

Haar, S., Kern, C., Schwoon, S.: Computing the reveals relation in occurrence nets. In: Proceedings of GandALF’11. Electronic Proceedings in Theoretical Computer Science, vol. 54, pp. 31–44 (2011)

Kumar, R., Takai, S.: Decentralized prognosis of failures in discrete event systems. IEEE Trans. Autom. Control 55(1), 48–59 (2010)CrossRefMathSciNet

Madalinski, A., Khomenko, V.: Diagnosability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Control and Fault-Tolerant Systems (SysTol’2010), pp. 398–403. IEEE Computing Society Press (2010)

10.

Madalinski, A., Khomenko, V.: Predictability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Proceedings of the 8th IFAC Symposium on Fault Detection, Diagnosis and Safety of Technical Processes (SAFEPROCESS’2012), pp. 1232–1237 (2012)

11.

Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theoret. Comput. Sci. 13, 85–108 (1981)CrossRefMATHMathSciNet

12.

Zielonka, W.: Notes on finite asynchronous automata. RAIRO Theoret. Inform. Appl. 21, 99–135 (1987)MATHMathSciNet

Titel: A Canonical Contraction for Safe Petri Nets
verfasst von: Thomas Chatain
Stefan Haar
Verlag: Springer Berlin Heidelberg
Buch: Transactions on Petri Nets and Other Models of Concurrency IX
Print ISBN: 978-3-662-45729-0

Electronic ISBN: 978-3-662-45730-6

Copyright-Jahr: 2014
DOI: https://doi.org/10.1007/978-3-662-45730-6_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"