|
Title:
|
Petri net analysis using boolean manipulation
|
|
Author:
|
Pastor Llorens, Enric; Roig Mansilla, Oriol; Cortadella, Jordi; Badia Sala, Rosa Maria
|
|
Other authors:
|
Universitat Politècnica de Catalunya. Departament d'Arquitectura de Computadors; Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. CAP - Grup de Computació d'Altes Prestacions; Universitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals |
|
Abstract:
|
This paper presents a novel analysis approach for bounded Petri nets. The net behavior is modeled by boolean functions, thus reducing reasoning about Petri nets to boolean calculation. The state explosion problem is managed by using Binary Decision Diagrams (BDDs), which are capable to represent large sets of markings in small data structures. The ability of Petri nets to model systems, the flexibility and generality of boolean algebras, and the efficient implementation of BDDs, provide a general environment to handle a large variety of problems. Examples are presented that show how all the reachable states (1018) of a Petri net can be efficiently calculated and represented with a small BDD (103 nodes). Properties requiring an exhaustive analysis of the state space can be verified in polynomial time in the size of the BDD. |
|
Abstract:
|
Peer Reviewed |
|
Subject(s):
|
-Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
-Petri nets
-Computational complexity
-Boolean function
-Boolean algebra
-Binary decision diagram
-Strongly connect component
-Firing sequence
-Petri, Xarxes de
-Complexitat computacional |
|
Rights:
|
|
|
Document type:
|
Article - Submitted version
Book Part |
|
Published by:
|
Springer
|
|
Share:
|
|
