Vorwort

Der Integrierte Netz Analysator INA ist ein Programm, mit dessen Hilfe Petri-Netze verschiedenster Typen unter verschiedenen Schaltregeln, insbesondere unter Zeitbewertung, hinsichtlich allgemeiner Eigenschaften untersucht werden können. Typische Eigenschaften, die durch Analyse nachgewiesen werden, sind Beschränktheit von Plätzen, Lebendigkeit von Transitionen, Erreichbarkeit bzw. Nicht-Erreichbarkeit von Markierungen bzw. Zuständen.

Mit der Modellierung eines (vorhandenen oder geplanten) Systems in der Sprache der Petri-Netze, d.h. dem Entwurf eines Petri-Netz-Modells, ist eine Abstraktion verbunden, bei der bestimmten Eigenschaften des Systems Eigenschaften des Netzes zugordnet sind, z.B. kann der Verklemmungsfreiheit des Systems die Nichterreichbarkeit einer toten Markierung entsprechen.

Der Lebenszyklus eines Netzmodells kann grob als

• Entwurf
• Analyse
• Interpretation
• Neuentwurf

skizziert werden. Dabei kommt der Interpretation der Analyseergebnisse eine nicht zu unterschätzende Bedeutung zu.

INA wurde von Prof. Dr. Peter H. Starke entwickelt. Mit diesem interaktiven, menügesteuerten Programm können Sie Netze editieren, reduzieren, ausführen und analysieren. Es umfasst die in früheren Werkzeugen ,,Petri-Netz-Maschine``, ,,PAN``, ,,CPNA`` und ,,ATNA`` angebotenen Analyseverfahren und ist von Dr. Karsten Schmidt, Dipl.-Inf. Lutz Pogrell, Dipl.-Inf. Karsten Lüttke und Stephan Roch wesentlich erweitert worden.

Dieses Handbuch beschreibt die Funktionalität der Version 2.1 von INA . Es wurde von Stephan Roch in Zusammenarbeit mit Prof. Peter H. Starke erstellt.

In der nun vorliegenden Programmversion gibt es einige Erweiterungen, neue Funktionen und effizientere Algorithmen, besonders im Bereich der Graphberechnung und -analyse.

Erstmals steht das Programm kostenlos als Vollversion zur Verfügung, Konditionen für Quelltexte werden auf Anfrage genannt (siehe auch Seite ).

Folgende neue Funktionen werden beschrieben:

• Schneller (struktureller) Beschränktheitstest mittels Platzsubinvarianten, ohne diese explizit zu berechen (siehe Seite im Kapitel 6.4.1)
• Schneller (struktureller) Nichterreichbarkeitstest mittels der Zustandsgleichung (siehe Seite im Kapitel 6.4.2)
• Berechnung minimaler Pfade zu Zuständen, bei denen ein Zustandsprädikat erfüllt ist (siehe Seite im Kapitel 6.5.3)
• Modelchecking mit Zustandsprädikaten basierend auf Formeln der Computational Tree Logic (CTL - siehe ab Seite im Kapitel 6.5.2 bzw. ab Seite im Kapitel 6.5.4).

Die Graphanalyse basiert jetzt nicht mehr auf der Erzeugung der Datei STATES.gra, sondern schließt unmittelbar an die Graphberechnung an. Zusammen mit dem abschaltbaren Überdeckbarkeitstests während der Berechnung und interner Reorganisation ergibt sich durch diese Änderung eine schnellere und effizientere Berechung. Bei einer symmetrischen Reduktion des Zustandsgraphen werden nun nicht mehr alle Symmetrien, sondern nur noch deren Generatoren berechnet. Im ungüstigen Fall hat ein Netz exponentiell viele Symmetrien, die Anzahl der Generatoren ist aber polynomial in der Netzgröße. Aus den Generatoren können die Symmetrien beim Aufbau des Graphen kombiniert werden. Das implementierte Verfahren hat im allgemeinen ein gutes Laufzeitverhalten, der Speicherbedarf ist auf jeden Fall wesentlich geringer.

Für die Graphberechnung müssen nur wenige Optionen gesetzt werden, die weitere Graphanalyse ist nun in einem eigenen Untermenü in beliebiger Reihenfolge durchführbar. Bis zur Version 1.7 war die Graphanalyse in einen Berechnungs- und einen Analyseteil gespalten. Im Gegensatz zu früheren Versionen kann nun die Graphanalyse nicht später auf einem bereits berechneten Graphen mittels der Datei STATES.gra erneut durchgeführt werden. Die weitere Analyse von Überdeckbarkeitsgraphen wird ebenfalls nicht mehr unterstützt.

Fakten, d.h. Transitionen, für die angenommen wird, daß sie nie schalten (tote Transitionen), wurden bis zur Version 1.7 benutzt, um den Zustandsgraphen zu beschränken: Ein Zustand, in dem ein Fakt Konzession erhält, wurde nicht weiter entwickelt und als ,,schlecht`` bezeichnet. In Version 2.1 ist die Beschränkung der Berechnung des Zustandsgraphen durch ein sogenanntes ,,bad`` Prädikat möglich. Zustände, bei denen dieses Prädikat erfüllt ist, werden nun als ,,schlecht`` bezeichnet, der weitere Aufbau des Graphen wird an dieser Stelle abgebrochen. Änderungen ergeben sich durch den Wegfall von Fakten bei der Netzeingabe, im Dateiformat und beim Reduzieren.

Nicht mehr unterstützt werden folgende Funktionalitäten:

• Zeitbewertung von Plätzen mit einer Verweilzeit [Sta90, Kapitel 18 (197-208)]

  Die Berechnung von Zuständen erforderte bei dieser Zeitbewertung einen großen Zeit- und Speicherbedarf, da Matrizen gespeichert werden müssen. Zumeist wird aber nur eine Bewertung von Transitionen bzw. Bögen gewünscht. Deshalb wird diese Form der Zeitbewertung nicht mehr unterstützt.

  Sichere Netze mit einer Zeitbewertung von Plätzen können durch Netze mit Zeitintervallen an den Bögen simuliert werden: Falls eine Marke auf einem Platz p dort d Zeiteinheiten zu warten hat, dann wird jedem von p abgehenden Bogen das Intervalls $[d,\infty]$ zugeordnet. Das Schaltverhalten ist gleich, solange keine weitere Marke die Uhr auf dem Platz p zurückstellt.

• Selbstmodifizierende Netze [Sta90, (106)]

  In selbstmodifizierenden Netzen kann ein Bogen mit einer formalen Summe von Plätzen beschriftet werden. Die Vielfachheit dieses Platzes ist die korrespondierende Summe der aktuellen Markierung.

  Bis zur Version 1.7 gab es eine einfache Implementation, die als Korrespondenz nur die Markierung eines Platzes als Vielfachheit eines Bogens zuließ. Da dies nicht den gewünschten Anforderungen entspricht, unterbleibt die weitere Unterstützung.

• Baumdarstellung des Zustandsgraphen

  Die Ausgabe des Zustandsgraphen in einer flachen Form wird nicht mehr weiter unterstützt. Stattdesen kann ein Überblick über die Graphstruktur durch die Graphmatrix erhalten werden.

Weitere Änderungen ergeben sich

• bei den Dateiextensionen: neue, weggefallene bzw. geänderte Dateiformate (siehe Seite im Kapitel 2.3.2)
• im Editor: zwei neue Funktionen zur Einführung eines Laufplatzes und einer Schleife (siehe Seite im Kapitel 3.1)
• beim Schalten: Ausgabe der Systemzeit bei Zeitbewertungen (siehe Seite im Kapitel 4.4.1)
• bei der Berechnung starker Zusammenhangskomponenten des Zustandsgraphen: Ausgabe aller starken Zusammenhangskomponenten (zuvor nur terminale - siehe Seite im Kapitel 6.5.4)
• im Format der Datei OPTIONS.ina: Durch erweiterte Optionsspeicherung hat sich das Format geändert. Löschen Sie bitte alle mit früheren Versionen erstellte Optionsdateien. Das gleiche gilt für die Kommandodatei COMMAND.ina (siehe auch Seite im Kapitel 2.3.1).

Zum Verständnis des Programms ist eine gewisse Kenntnis der Netztheorie, mindestens ihrer grundlegenden Definitionen notwendig. Wir verweisen dazu auf das Buch ,,Analyse von Petri-Netz-Modellen`` erschienen 1990 in der Reihe ,,Leitfäden und Monographien der Informatik`` beim B. G. Teubner Verlag in Stuttgart [Sta90]. Darin sind auch viele der in INA implementierten Algorithmen näher beschrieben.

Für Fehler in diesem Handbuch oder im Programm wird keine Haftung übernommen.

Berlin im April 1998

Peter H. Starke und Stephan Roch