Towards reasoning about Petri nets: A Propositional Dynamic Logic based approach
| Autor: | Edward Hermann Haeusler, Bruno Lopes, Mario R. F. Benevides |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Soundness
Theoretical computer science General Computer Science Computer science 010102 general mathematics 0102 computer and information sciences Petri net Semantics Propositional calculus 01 natural sciences Theoretical Computer Science 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Dynamic logic (modal logic) 0101 mathematics Boolean satisfiability problem Dynamic logic (digital electronics) |
| Zdroj: | Theoretical Computer Science. 744:22-36 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/j.tcs.2018.01.007 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect