Towards reasoning about Petri nets: A Propositional Dynamic Logic based approach

被引：2

作者：

Benevides, Mario ^{[1
]}

Lopes, Bruno ^{[2
]}

Haeusler, Edward Hermann ^{[3
]}

机构：

[1] Univ Fed Rio de Janeiro, Programa Engn Sistemas & Comp, Rio De Janeiro, Brazil

[2] Univ Fed Fluminense, Inst Comp, Niteroi, RJ, Brazil

[3] Pontificia Univ Catolica Rio de Janeiro, Dept Informat, Rio De Janeiro, Brazil

来源：

THEORETICAL COMPUTER SCIENCE | 2018年 / 744卷

关键词：

Dynamic Logic; Petri nets; Modal Logic;

D O I：

10.1016/j.tcs.2018.01.007

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This work extends our previous work [4,22] with the iteration operator. This new operator allows for representing more general networks and thus enhancing the former propositional logic for Petri nets. We provide an axiomatization and a new semantics, prove soundness and completeness with respect to its semantics and the EXPTIME-Hardness of its satisfiability problem, present a linear model checking algorithm and show that its satisfiability problem is in 2EXPTIME. In order to illustrate its usage, we also provide some examples. (C) 2018 Elsevier B.V. All rights reserved.

引用

页码：22 / 36

页数：15

共 50 条

[1] Propositional dynamic logic for Petri nets
Lopes, Bruno
Benevides, Mario
Haeusler, Edward Hermann
[J]. LOGIC JOURNAL OF THE IGPL, 2014, 22 (05) : 721 - 736
[2] Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic Logic
Lopes, Bruno
Nalon, Claudia
Haeusler, Edward Hermann
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2021, 22 (02)
[3] Extending Propositional Dynamic Logic for Petri Nets
Lopes, Bruno
Benevides, Mario
Haeusler, Edward Hermann
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2014, 305 : 67 - 83
[4] Propositional Dynamic Logic for Petri Nets with Iteration
Benevides, Mario R. F.
Lopes, Bruno
Haeusler, Edward Hermann
[J]. THEORETICAL ASPECTS OF COMPUTING - ICTAC 2016, 2016, 9965 : 441 - 456
[5] THE UNDECIDABILITY OF PROPOSITIONAL TEMPORAL LOGIC FOR PETRI NETS
CHERKASOVA, LA
KOTOV, VE
[J]. COMPUTERS AND ARTIFICIAL INTELLIGENCE, 1987, 6 (02): : 123 - 130
[6] A Propositional Dynamic Logic Approach for Order of Magnitude Reasoning
Burrieza, A.
Munoz-Velasco, E.
Ojeda-Aciego, M.
[J]. ADVANCES IN ARTIFICIAL INTELLIGENCE - IBERAMIA 2008, PROCEEDINGS, 2008, 5290 : 11 - +
[7] Reductions of Petri nets and unfolding of propositional logic programs
Fribourg, L
Olsen, H
[J]. LOGIC PROGRAM SYNTHESIS AND TRANSFORMATION, 1997, 1207 : 187 - 203
[8] Temporal reasoning method of time Petri nets based on linear logic
Gao, Meimei
Wu, Zhiming
[J]. Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2000, 37 (12): : 1452 - 1456
[9] A Classical Propositional Logic for Reasoning About Reversible Logic Circuits
Axelsen, Holger Bock
Gluck, Robert
Kaarsgaard, Robin
[J]. LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, 2016, 9803 : 52 - 67
[10] An Approach for Repairing Process Models Based on Logic Petri Nets
Zhang, Xize
Du, Yuyue
Qi, Liang
Sun, Haichun
[J]. IEEE ACCESS, 2018, 6 : 29926 - 29939

← 1 2 3 4 5 →