Paper Info
Title
Towards Reasoning in Dynamic Logics with Rewriting Logic: The Petri-PDL Case.
Abstract
Safety is a desired property in software to ensure that no unforeseen scenarios will be achieved and in concurrent systems the variety of scenarios increase with complexity. Dynamic Logics (DL) present a large body of techniques to reason about and certify systems. Modelling and assessing concurrent systems with a formal semantics leads to the possibility of proving that they comply with their specification. Petri nets fulfill these requirements as a formal modelling language comprising a wide body of tools and an intuitive graphical interpretation. Petri-PDL puts together DL with Petri nets, providing a theoretical background to reason about Petri nets, inheriting their properties with all the techniques available for DL. This work presents a prototype implementation, in the Rewriting Logic language Maude, of a bounded model checker for Petri-PDL. The Petri-PDL model checker is formally designed following the representation of Kripke models as rewrite theories defined for the Linear Temporal Logic model checker available in the Maude system.
Year
Venue
Field
2015
SBMF
Kripke structure,T-norm fuzzy logics,Petri net,Programming language,Computer science,Substructural logic,Linear temporal logic,Theoretical computer science,Rewriting,Non-monotonic logic,Classical logic
DocType
Citations 
PageRank 
Conference
2
0.38
References 
Authors
3
2
Name
Order
Citations
PageRank
Christiano Braga118017.38
Bruno Lopes2144.40