A calculus for automatic verification of Petri nets based on resolution and dynamic logics
From MaRDI portal
Publication:530854
DOI10.1016/j.entcs.2015.04.008zbMath1342.68237OpenAlexW2009555631WikidataQ113317806 ScholiaQ113317806MaRDI QIDQ530854
Bruno D. Lopes, Gilles Dowek, Cláudia Nalon, Edward Hermann Haeusler
Publication date: 1 August 2016
Full work available at URL: https://doi.org/10.1016/j.entcs.2015.04.008
Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Extending propositional dynamic logic for Petri nets
- Propositional dynamic logic of regular programs
- Combining deduction and model checking into tableaux and algorithms for converse-PDL.
- Model checking propositional dynamic logic with all extras
- Anti-prenexing and Prenexing for Modal Logics
- Infinite State Model-Checking of Propositional Dynamic Logics
- Monodic temporal resolution
- A Machine-Oriented Logic Based on the Resolution Principle
- Lectures on Concurrency and Petri Nets