Synthesizing Petri nets from LTL specifications – An engineering approach

From GRK-Wiki

• accepted for and presented at the 14th Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN'07), Universität Koblenz-Landau, Campus Koblenz, Germany

Author

• Dirk Fahland, Humboldt-Universität zu Berlin, Germany

Abstract

In this paper we present a pattern-based approach for synthesizing truly distributed Petri nets from a class of LTL specifications. The synthesis allows for the automatic, correct generation of humanly conceivable Petri nets, thus circumventing a manual construction of nets, or the use of Büchi automata which are not distributed and often less intuitive to understand.

Downloads

• article .pdf

BibTeX

@INPROCEEDINGS{fahland2007_awpn,
 author = {Fahland, Dirk},
 title = {Synthesizing Petri nets from LTL specifications - An engineering approach},
 booktitle = {Proceedings 14.Workshop Algorithmen und Werkzeuge
              für Petrinetze (AWPN), Arbeitsbericht aus dem Fach Informatik,
              Nr. 25/2007},
 editor = {Philippi, Stephan and Pinl, Alexander},
 month = {September},
 year = {2007},
 address = {Universität Koblenz-Landau, Germany},
 keywords = {Petri Nets, Temporal Logic},
 pages = {69--74}
}