Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic Logic

2021 ◽  
Vol 22 (2) ◽  
pp. 1-22
Author(s):  
Bruno Lopes ◽  
Cláudia Nalon ◽  
Edward Hermann Haeusler
Keyword(s):  
Normal Form ◽  
Petri Nets ◽  
Dynamic Logic ◽  
Concurrent Systems ◽  
Modal Logics ◽  
Inference Rules ◽  
Logical Language ◽  
Dynamic Logics

Petri Nets are a widely used formalism to deal with concurrent systems. Dynamic Logics (DLs) are a family of modal logics where each modality corresponds to a program. Petri-PDL is a logical language that combines these two approaches: it is a dynamic logic where programs are replaced by Petri Nets. In this work we present a clausal resolution-based calculus for Petri-PDL. Given a Petri-PDL formula, we show how to obtain its translation into a normal form to which a set of resolution-based inference rules are applied. We show that the resulting calculus is sound, complete, and terminating. Some examples of the application of the method are also given.

Algebraic properties of processes for Local Action Systems

2002 ◽  
Vol 12 (4) ◽  
pp. 423-448
Author(s):  
NICO VERLINDEN ◽  
DIRK JANSSENS
Keyword(s):  
Petri Nets ◽  
Formal Semantics ◽  
Dynamic Structure ◽  
Concurrent Systems ◽  
Local Action ◽  
Graph Rewriting ◽  
Action Systems ◽  
Algebraic Properties ◽  
Dynamic Structures

Graph rewriting has been used extensively to model the behaviour of concurrent systems and to provide a formal semantics for them. In this paper, we investigate processes for Local Action Systems (LAS); LAS generalize several types of graph rewriting based on node replacement and embedding. An important difference between processes for Local Action Systems and the process notions that have been introduced for other systems, for example, Petri nets, is the presence of a component describing the embedding mechanism. The aim of the paper is to develop a methodology for dealing with this embedding mechanism: we introduce a suitable representation (a dynamic structure) for it, and then investigate the algebraic properties of this representation. This leads to a simple characterization of the configurations of a process and to a number of equational laws for dynamic structures. We illustrate the use of these laws by providing an equational proof of one of the basic results for LAS processes, namely that the construction yielding the result graph of a process behaves well with respect to the sequential composition of processes.

scholarly journals A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics

2015 ◽  
Vol 312 ◽  
pp. 125-141 ◽  
Author(s):  
Cláudia Nalon ◽  
Bruno Lopes ◽  
Gilles Dowek ◽  
Edward Hermann Haeusler
Keyword(s):  
Petri Nets ◽  
Automatic Verification ◽  
Dynamic Logics

scholarly journals INSTANTIAL NEIGHBOURHOOD LOGIC

2016 ◽  
Vol 10 (1) ◽  
pp. 116-144 ◽  
Author(s):  
JOHAN VAN BENTHEM ◽  
NICK BEZHANISHVILI ◽  
SEBASTIAN ENQVIST ◽  
JUNHUA YU
Keyword(s):  
Fine Structure ◽  
Normal Form ◽  
Axiom System ◽  
Topological Spaces ◽  
Relational Semantics ◽  
Basic Model ◽  
Semantic Tableaux ◽  
Dynamic Logics ◽  
A Current

AbstractThis paper explores a new language of neighbourhood structures where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. The resulting system of ‘instantial neighbourhood logic’ INL has a nontrivial mix of features from relational semantics and from neighbourhood semantics. We explore some basic model-theoretic behavior, including a matching notion of bisimulation, and give a complete axiom system for which we prove completeness by a new normal form technique. In addition, we relate INL to other modal logics by means of translations, and determine its precise SAT complexity. Finally, we discuss proof-theoretic fine-structure of INL in terms of semantic tableaux and some expressive fine-structure in terms of fragments, while discussing concrete illustrations of the instantial neighborhood language in topological spaces, in games with powers for players construed in a new way, as well as in dynamic logics of acquiring or deleting evidence. We conclude with some coalgebraic perspectives on what is achieved in this paper. Many of these final themes suggest follow-up work of independent interest.

Sign in / Sign up

Export Citation Format

Share Document