| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 422720 | Electronic Notes in Theoretical Computer Science | 2015 | 17 Pages |
Abstract
Petri Nets are a widely used formalism to deal with concurrent systems. Dynamic Logics (DL) are a family of modal logics where each modality corresponds to a program. This works presents a resolution-based method for Petri-PDL, a DL where programs are replaced by Petri Nets. We present a procedure to convert any Petri-PDL formula into a normal form, a set of resolution-based inference rules, examples of application of the method, and discuss soundness and completeness.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
