| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10225767 | Theoretical Computer Science | 2018 | 15 Pages |
Abstract
This work extends our previous work [4], [22] with the iteration operator. This new operator allows for representing more general networks and thus enhancing the former propositional logic for Petri nets. We provide an axiomatization and a new semantics, prove soundness and completeness with respect to its semantics and the EXPTIME-Hardness of its satisfiability problem, present a linear model checking algorithm and show that its satisfiability problem is in 2EXPTIME. In order to illustrate its usage, we also provide some examples.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Mario Benevides, Bruno Lopes, Edward Hermann Haeusler,