Extending Propositional Dynamic Logic for Petri Nets

被引：5

作者：

Lopes, Bruno ^{[1
]}

Benevides, Mario ^{[2
]}

Haeusler, Edward Hermann ^{[1
]}

机构：

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

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

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2014年 / 305卷

关键词：

Dynamic Logic; Petri Nets; Stochastic Petri Nets; program verification;

D O I：

10.1016/j.entcs.2014.06.006

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Propositional Dynamic Logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri Nets is a widely used formalism to specify and analyze concurrent programs with a very intuitive graphical representation. Petri-PDL is an extension of PDL, whose programs are Petri Nets, which combines the advantages of both formalisms using a compositional and structural approach to deal with Petri Nets. In this work we present an extension of Petri-PDL to deal with Stochastic Petri Nets, the DS3 logic. This system is an alternative to model performance evaluation in a compositional and structural approach. We discuss about its soundness, decidability and completeness regarding our semantics and present a proof of EXPTime-completeness of its SAT problem. A usage example is presented.

引用

页码：67 / 83

页数：17

共 50 条

[11] FROM PETRI NETS TO LINEAR LOGIC
MARTIOLIET, N
MESEGUER, J
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 389 : 313 - 340
[12] ON MODELS FOR PROPOSITIONAL DYNAMIC LOGIC
KNIJNENBURG, PMW
VANLEEUWEN, J
[J]. THEORETICAL COMPUTER SCIENCE, 1991, 91 (02) : 181 - 203
[13] PROPOSITIONAL DYNAMIC LOGIC OF FLOWCHARTS
HAREL, D
SHERMAN, R
[J]. INFORMATION AND CONTROL, 1985, 64 (1-3): : 119 - 135
[14] Inquisitive Propositional Dynamic Logic
Puncochar, Vit
Sedlar, Igor
[J]. JOURNAL OF LOGIC LANGUAGE AND INFORMATION, 2021, 30 (01) : 91 - 116
[15] Relevant propositional dynamic logic
Tedder, Andrew
Bilkova, Marta
[J]. SYNTHESE, 2022, 200 (03)
[16] Inquisitive Propositional Dynamic Logic
Vít Punčochář
Igor Sedlár
[J]. Journal of Logic, Language and Information, 2021, 30 : 91 - 116
[17] Relevant propositional dynamic logic
Andrew Tedder
Marta Bilková
[J]. Synthese, 200
[18] Extending the Modeling and Analysis Capabilities of Continuous Petri Nets by Flexible Nets
Julvez, Jorge
Oliver, Stephen G.
[J]. 2021 60TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2021, : 1750 - 1756
[19] PROPOSITIONAL DYNAMIC LOGIC OF FLOWCHARTS
HAREL, D
SHERMAN, R
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1983, 158 : 195 - 206
[20] Propositional dynamic logic as a logic of belief revision
van Eijck, Jan
Wang, Yanjing
[J]. LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, 2008, 5110 : 136 - 148

← 1 2 3 4 5 →