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

被引：3

作者：

Nalon, Claudia ^{[1
]}

Lopes, Bruno ^{[2
]}

Dowek, Gilles ^{[3
]}

Haeusler, Edward Hermann ^{[2
]}

机构：

[1] Univ Brasilia, Dept Comp Sci, BR-70910900 Brasilia, DF, Brazil

[2] Pontificia Univ Catolica Rio de Janeiro, Dept Informat, BR-22453 Rio De Janeiro, Brazil

[3] Inst Natl Rech Informat & Automat, Deducteam, Le Chesnay, France

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2015年 / 312卷

关键词：

Dynamic logic; Petri Nets; Resolution; Deductive systems;

D O I：

10.1016/j.entcs.2015.04.008

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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 to convert any Petri-PDL formula into a normal form, a set of resolution-based inference rules, examples of application of the method, and discuss soundness and completeness.

引用

页码：125 / 141

页数：17

共 19 条

[1]

[Anonymous], 2014, LOGIC J IGPL

[2]

Bourcerie M, 2008, GLOB COOP ENG ED, P85

[3]

de Almeida E. S., 1999, PETRI NET NEWSLETTER, V57, P23

[4]

de Giacomo G., 1998, INFORM COMPUTATION, V160, P2000

[5] Monodic temporal resolution [J].

Degtyarev, Anatoli ;

Fisher, Michael ;

Konev, Boris .

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2006, 7 (01) :108-150

[6] Petri nets and software engineering [J].

Denaro, G ;

Pezzè, M .

LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 :439-466

[7]

Egly U., 1994, Logic Programming and Automated Reasoning. 5th International Conference, LPAR '94. Proceedings, P69

[8] PROPOSITIONAL DYNAMIC LOGIC OF REGULAR PROGRAMS [J].

FISCHER, MJ ;

LADNER, RE .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1979, 18 (02) :194-211

[9]

Goller S, 2006, LECT NOTES COMPUT SC, V4207, P349

[10]

Lange M, 2006, J APPL LOGIC, V4, P39, DOI DOI 10.1016/J.JAL.2005.08.002

← 1 2 →