A Polynomial Translation of π-Calculus (FCP) to Safe Petri Nets

被引:0
|
作者
Meyer, Roland [1 ]
Khomenko, Victor [2 ]
Huechting, Reiner [1 ]
机构
[1] Univ Kaiserslautern, D-67663 Kaiserslautern, Germany
[2] Newcastle Univ, Newcastle, NSW, Australia
来源
基金
英国工程与自然科学研究理事会;
关键词
finite control process; pi-calculus; Petri net; model checking; VERIFICATION;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We develop a polynomial translation from finite control processes (an important fragment of pi-calculus) to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural (there is a close correspondence between the control flow of the original specification and the resulting Petri net), enjoys a bisimulation result, and it is suitable for practical model checking.
引用
收藏
页码:440 / 455
页数:16
相关论文
共 50 条
  • [41] A Polynomial Algorithm for Computing Elementary Siphons in a Class of Petri Nets
    Liu, Huixia
    Xing, Keyi
    Wang, Feng
    Han, Libin
    Sun, Xiaojing
    ASIAN JOURNAL OF CONTROL, 2012, 14 (04) : 1141 - 1149
  • [42] A polynomial complexity algorithm to decide the liveness for a class of Petri nets
    Li, ZW
    Liu, D
    2005 INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION (ICCA), VOLS 1 AND 2, 2005, : 1175 - 1180
  • [43] Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic Logic
    Lopes, Bruno
    Nalon, Claudia
    Haeusler, Edward Hermann
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2021, 22 (02)
  • [44] A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics
    Nalon, Claudia
    Lopes, Bruno
    Dowek, Gilles
    Haeusler, Edward Hermann
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2015, 312 : 125 - 141
  • [45] DFL: A dataflow language based on Petri nets and nested relational calculus
    Hidders, Jan
    Kwasnikowska, Natalia
    Sroka, Jacek
    Tyszkiewicz, Jerzy
    Van den Bussche, Jan
    INFORMATION SYSTEMS, 2008, 33 (03) : 261 - 284
  • [46] Collaboration business processes modeling based on Petri nets and Pi calculus
    Xu, Fei
    Zhang, Li
    IMECS 2007: INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, VOLS I AND II, 2007, : 412 - +
  • [47] Parameterized Complexity Results for 1-safe Petri Nets
    Praveen, M.
    Lodaya, Kamal
    CONCUR 2011: CONCURRENCY THEORY, 2011, 6901 : 358 - 372
  • [48] Transforming Dynamic Condition Response Graphs to Safe Petri Nets
    Cosma, Vlad Paul
    Hildebrandt, Thomas T.
    Slaats, Tijs
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2023, 2023, 13929 : 417 - 439
  • [49] Reduction of constraints for controller synthesis based on safe Petri Nets
    Dideban, Abbas
    Alla, Hassane
    AUTOMATICA, 2008, 44 (07) : 1697 - 1706
  • [50] Determination of minimal sets of control places for safe Petri nets
    Dideban, A.
    Alla, H.
    2007 AMERICAN CONTROL CONFERENCE, VOLS 1-13, 2007, : 455 - 460