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
来源：
CONCUR 2012 - CONCURRENCY THEORY | 2012年 / 7454卷
基金：
英国工程与自然科学研究理事会;
关键词：
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 条
  • [21] The Pi+ calculus-an extension of the Pi calculus for expressing Petri nets
    Hao K.-G.
    Guo X.-Q.
    Li X.-N.
    Jisuanji Xuebao/Chinese Journal of Computers, 2011, 34 (02): : 193 - 203
  • [22] Digital hardware implementation of Petri net based specifications:: Direct translation from safe automation Petri nets to circuit elements
    Uzam, M
    Avci, M
    Yalçin, MK
    DESDES '1: PROCEEDINGS OF THE INTERNATIONAL WORKSHOP ON DISCRETE-EVENT SYSTEM DESIGN, 2001, : 25 - 33
  • [23] A polynomial algorithm to decide the liveness for a class of Petri nets
    Li, Zhiwu
    Liu, Ding
    Wang, Anrong
    PROCEEDINGS OF THE 2006 IEEE INTERNATIONAL CONFERENCE ON NETWORKING, SENSING AND CONTROL, 2006, : 254 - 259
  • [24] A Polynomial Algorithm for Observer Design with Interpreted Petri Nets
    Jimenez, Maria
    Ramirez Trevino, Antonio
    2012 WORLD AUTOMATION CONGRESS (WAC), 2012,
  • [25] A Process Calculus for Expressing Finite Place/Transition Petri Nets
    Gorrieri, Roberto
    Versari, Cristian
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (41): : 76 - 90
  • [26] Analysing Petri Nets in a Calculus of Context-aware Ambients
    Siewe, Francois
    Germanos, Vasileios
    Zeng, Wen
    2020 IEEE 44TH ANNUAL COMPUTERS, SOFTWARE, AND APPLICATIONS CONFERENCE (COMPSAC 2020), 2020, : 1647 - 1652
  • [27] On the Relationship between π-Calculus and Finite Place/Transition Petri Nets
    Meyer, Roland
    Gorrieri, Roberto
    CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS, 2009, 5710 : 463 - +
  • [28] Unified modeling and analysis based on Petri nets and Pi calculus
    Xu, Fei
    Zhang, Li
    TASE 2007: FIRST JOINT IEEE/IFIP SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, : 75 - +
  • [29] Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs
    Busi, Nadia
    Gorrieri, Roberto
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2009, 78 (03): : 138 - 162
  • [30] Power Grids' Dynamic Enlargement Calculus Using Petri Nets
    Munteanu, Radu
    Dub, Vasile
    ADVANCES IN ELECTRICAL AND COMPUTER ENGINEERING, 2011, 11 (02) : 73 - 78
12345