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

被引：0

作者：

Lopes, Bruno ^{[1
]}

Nalon, Claudia ^{[2
]}

Haeusler, Edward Hermann ^{[3
]}

机构：

[1] Univ Fed Fluminense, Inst Comp, Rua Gal Milton Tavares Souza S-N, BR-24210346 Niteroi, RJ, Brazil

[2] Univ Brasilia, Dept Ciencia Comp, Campus Univ Asa Norte,POB 4466, BR-70910090 Brasilia, DF, Brazil

[3] Pontificia Univ Catolica Rio de Janeiro, Dept Informat, Rua Marques de Sao Vicente 225, BR-22451900 Rio De Janeiro, RJ, Brazil

来源：

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC | 2021年 / 22卷 / 02期

关键词：

Modal logic; Petri nets; resolution; MODEL CHECKING;

D O I：

10.1145/3441655

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页数：22

共 35 条

[1]

Amparore Elvio Gilberto, 2014, Application and Theory of Petri Nets and Concurrency. 35th International Conference, PETRI NETS 2014. Proceedings: LNCS 8489, P354, DOI 10.1007/978-3-319-07734-5_19

[2] Deterministic and stochastic Petri net for urban traffic systems [J].