A calculus for automatic verification of Petri nets based on resolution and dynamic logics

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

zbMATH Keywords

Petri netsdynamic logicresolutiondeductive systems

Mathematics Subject Classification ID

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