A Survey of Elementary Object Systems - Part I: Decidability Results
| URL | http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/174/ |
|---|---|
| Dokumentart: | ResearchPaper |
| Institut: | Fachbereich Informatik |
| Sprache: | Englisch |
| Erstellungsjahr: | 2011 |
| Publikationsdatum: | 04.11.2011 |
| Freie Schlagwörter (Deutsch): | Petrinetze , Netze-in-Netzen , Netze als Marken , Objektnetze , Sicherheit , Erreichbarkeit , Lebendigkeit , Beschränktheit |
| Freie Schlagwörter (Englisch): | Petri nets , nets-within-nets , nets as tokens , object nets , safeness , reachability , liveness , boundedness |
| DDC-Sachgruppe: | Informatik |
| BK - Klassifikation: | 54.10 |
Kurzfassung auf Englisch:
This contribution presents the formalism of Elementary Object Systems (Eos). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. Since object nets in general are immediately Turing complete, we introduce the restricted class of elementary object nets which restrict the nesting of nets to the depth of two. In this work we study the relationship of Eos to existing Petri net formalisms. It turns out that Eos are more powerful than classical p/t nets which is demonstrated by the fact that e.g. reachability and liveness become undecidable problems for Eos. Despite these undecidability results other properties can be extended to Eos using a monotonicity argument similar to that for p/t nets. Also linear algebraic techniques, especially the theory of linear invariants and semiflows, can be extended in an appropriate way. The invariant calculus for Eos even enjoys the property of compositionality, i.e. invariants of the whole system can be composed of invariants of the object nets, which reduces the computational effort. To obtain a finer level of insight we also study several subclasses. Among these variants the subclass of generalised state machines is worth mentioning since it combines the decidability of many theoretically interesting properties with a quite rich practical modelling expressiveness. We also study safe Eos, a generalisation of safe p/t nets which are bounded systems with bound b = 1. Four different variants of safeness are studied. It turns out that variants are equivalent for p/t like Eos. While reachability and liveness remain undecidable for the two weaker classes of safe Eos, the two most strongest variants are restrictive enough to guarantee decidability. In fact, both problems are PSpace-complete.
Kurzfassung auf Deutsch:
Dieser Artikel präsentiert den Formalismus der Elementaren Objektsysteme (Eos). Objektnetze sind Petrinetze, die wiederum Petrinetze als Marken besitzen – ein Ansatz der auch als das Paradigma der Netze-in-Netzen bekannt ist. Da Objektnetze im allgemeinen die Audrucksstärke von Turing-Maschinen besitzen, beschränken wir die Betrachtung hier auf die Klasse der elementaren Objektnetze, deren Schachtelungstiefe auf zwei Ebenen festgelegt ist. Wir betrachten die Beziehungen von Eos zu anderen Petrinetzformalismen. Es zeigt sich, dass Eos ausdrucksmächtiger als die klassischen P/T-Netze sind, was sich darin äußert, dass insbesondere das Erreichbarkeits- und das Lebendigkeitsproblem für Eos unentscheidbar sind. Trotz dieser Unentscheidbarkeitsresultate können andere Eigenschaften auch für Eos als entscheidbar nachgewiesen werden, indem man die Monotonie der Schaltregel – wie sie bekanntermaßen für P/T-Netze gilt – auch für Eos nachweist. Wir betrachten außerdem Techniken aus der linearen Algebra, hier insbesondere lineare Invarianten, die sich auch für Eos geignet definieren lassen. Wir zeigen, dass der Invariantenkalkül der Eos kompositional ist, d.h. man kann Invarianten des Gesamtsystems aus den Teil-Invarianten der Objektnetze erzeugen, was sinnvoll ist, um den Berech- nungsaufwand zu reduzieren. Um ein besseres Verständnis der Ausdrucksstärke der Objektnetze zu bekommen, betrachten wir auch strukturelle Teilklassen des Formalismus. Eine besonders interessante Teilklasse ist die der generalised state machines, da eine Vielzahl von Eigenschaften für diese Klasse entscheidbar ist und viele praktisch vorkommende Szenarien sich mit Netzen dieser Klasse modellieren lassen. Wir betrachten auch noch sichere Eos – eine Verallgemeinerung sicherer P/T-Netze. P/T-Netze heißen sicher, wenn alle Plätze die Kapazitätsschranke b = 1 besitzen. Wir studieren hier vier verschiedene Varianten der Sicherheit in Eos. Wir zeigen, dass diese Varianten für P/T-artige Eos zueinander äquivalent sind, während sie für Eos eine Hierarchie bilden. Während Erreichbarkeit und Lebendigkeit für die beiden schwächeren Formern der Sicherheit von Eos unentscheidbar bleiben, garantieren die beiden stärkeren Formen ihre Entscheidbarkeit. Man kann sogar konkreter zeigen, dass die Probleme in beiden Varianten PSpace-vollständige Probleme sind.
Hinweis zum Urherberrecht
Für Dokumente, die in elektronischer Form über Datenenetze angeboten werden, gilt uneingeschränkt das Urheberrechtsgesetz (UrhG). Insbesondere gilt:
Einzelne Vervielfältigungen, z.B. Kopien und Ausdrucke, dürfen nur zum privaten und sonstigen eigenen Gebrauch angefertigt werden (Paragraph 53 Urheberrecht). Die Herstellung und Verbreitung von weiteren Reproduktionen ist nur mit ausdrücklicher Genehmigung des Urhebers gestattet.
Der Benutzer ist für die Einhaltung der Rechtsvorschriften selbst verantwortlich und kann bei Mißbrauch haftbar gemacht werden.