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 条
  • [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] 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
  • [3] THE UNDECIDABILITY OF PROPOSITIONAL TEMPORAL LOGIC FOR PETRI NETS
    CHERKASOVA, LA
    KOTOV, VE
    [J]. COMPUTERS AND ARTIFICIAL INTELLIGENCE, 1987, 6 (02): : 123 - 130
  • [4] Towards reasoning about Petri nets: A Propositional Dynamic Logic based approach
    Benevides, Mario
    Lopes, Bruno
    Haeusler, Edward Hermann
    [J]. THEORETICAL COMPUTER SCIENCE, 2018, 744 : 22 - 36
  • [5] Reductions of Petri nets and unfolding of propositional logic programs
    Fribourg, L
    Olsen, H
    [J]. LOGIC PROGRAM SYNTHESIS AND TRANSFORMATION, 1997, 1207 : 187 - 203
  • [6] PETRI NETS IN LOGIC
    DOMENICI, A
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1990, 30 (1-5): : 193 - 198
  • [7] Constructing Petri Nets Model for Dynamic Description Logic Actions
    Ma, Bing-xian
    Xu, Ying-lei
    [J]. PROCEEDINGS OF THE FIRST INTERNATIONAL WORKSHOP ON EDUCATION TECHNOLOGY AND COMPUTER SCIENCE, VOL III, 2009, : 753 - +
  • [8] Expansion Nets: Proof-Nets for Propositional Classical Logic
    McKinley, Richard
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 535 - 549
  • [9] 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)
  • [10] PETRI NETS AS MODELS OF LINEAR LOGIC
    ENGBERG, U
    WINSKEL, G
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 431 : 147 - 161
12345