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

Nalon, Cláudia; Lopes, Bruno; Dowek, Gilles; Hermann Hæusler, Edward

doi:10.1016/j.entcs.2015.04.008

Public

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

Published in Electronic Notes in Theoretical Computer Science • Apr 1, 2015

Authors:

Cláudia Nalon

Bruno Lopes

Gilles Dowek

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 t...

Subject

Soundness

Petri net

Computer science

Finding related papers...

Discussions

(0)

No comments yet

Be the first to share your thoughts!