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

共 34 条

[21]

Kract M., 1995, Journal of Logic, Language and Information, V4, P41, DOI 10.1007/BF01048404

[22] Propositional dynamic logic with recursive programs [J].

Loeding, Christof ;

Lutz, Carsten ;

Serre, Olivier .

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2007, 73 (1-2) :51-69

[23] Reasoning about Multi-Agent Systems Using Stochastic Petri Nets [J].

Lopes, Bruno ;

Benevides, Mario ;

Haeusler, Edward Hermann .

TRENDS IN PRACTICAL APPLICATIONS OF AGENTS, MULTI-AGENT SYSTEMS AND SUSTAINABILITY: THE PAAMS COLLECTION, 2015, 372 :75-86

[24] Extending Propositional Dynamic Logic for Petri Nets [J].

Lopes, Bruno ;

Benevides, Mario ;

Haeusler, Edward Hermann .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2014, 305 :67-83

[25] Propositional dynamic logic for Petri nets [J].

Lopes, Bruno ;

Benevides, Mario ;

Haeusler, Edward Hermann .

LOGIC JOURNAL OF THE IGPL, 2014, 22 (05) :721-736

[26]

Meyer J.-J. C., 1988, Notre Dame Journal of Formal Logic, V29, P109, DOI 10.1305/ndjfl/1093637776

[27]

Mirkowska G., 1981, Annales Societatis Mathematicae Polonae, Series IV: Fundamenta Informaticae, V4, P675

[28] COMMUNICATION IN CONCURRENT DYNAMIC LOGIC [J].

PELEG, D .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1987, 35 (01) :23-58

[29] CONCURRENT DYNAMIC LOGIC [J].

PELEG, D .

JOURNAL OF THE ACM, 1987, 34 (02) :450-479

[30]

Petkov A., 1987, PROPOSITIONAL DYNAMI

← 1 2 3 4 →