A symbolic algorithm for the synthesis of bounded Petri nets

被引：0
|
作者：
Carmona, J. [1 ]
Cortadella, J. [1 ]
Kishinevsky, M. [2 ]
Kondratyev, A. [3 ]
Lavagno, L. [4 ]
Yakovlev, A. [5 ]
机构：
[1] Univ Politecn Cataluna, E-08028 Barcelona, Spain
[2] Intel Corp, Santa Clara, CA 95051 USA
[3] Cadence Berkeley Lab, Berkeley, CA 94704 USA
[4] Politecnico Torino, Turin, Italy
[5] Univ Newcastle, Callaghan, NSW 2308, Australia
来源：
APPLICATIONS AND THEORY OF PETRI NETS | 2008年 / 5062卷
基金：
英国工程与自然科学研究理事会;
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents an algorithm for the synthesis of bounded Petri nets from transition systems. A bounded Petri net is always provided in case it exists. Otherwise, the events are split into several transitions to guarantee the synthesis of a Petri net with bisimilar behavior. The algorithm uses symbolic representations of multisets of states to efficiently generate all the minimal regions. The algorithm has been implemented in a tool. Experimental results show a significant net reduction when compared with approaches for the synthesis of safe Petri nets.
引用
收藏
页码：92 / +
页数：2
相关论文
共 50 条
  • [41] Efficient encoding schemes for symbolic analysis of Petri nets
    Pastor, E
    Cortadella, J
    DESIGN, AUTOMATION AND TEST IN EUROPE, PROCEEDINGS, 1998, : 790 - 795
  • [42] Symbolic reachability analysis of Petri nets using ZBDDs
    Li, Feng-Ying
    Gu, Tian-Long
    Xu, Zhou-Bo
    Jisuanji Xuebao/Chinese Journal of Computers, 2009, 32 (12): : 2420 - 2428
  • [43] Symbolic Bounded Synthesis
    Ehlers, Ruediger
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 365 - 379
  • [44] Symbolic bounded synthesis
    Rüdiger Ehlers
    Formal Methods in System Design, 2012, 40 : 232 - 262
  • [45] Symbolic bounded synthesis
    Ehlers, Ruediger
    FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (02) : 232 - 262
  • [46] Verification of bounded Petri nets using integer programming
    Khomenko, Victor
    Koutny, Maciej
    FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (02) : 143 - 176
  • [47] Prognosability Analysis and Enforcement of Bounded Labeled Petri Nets
    Ran, Ning
    Hao, Jinyuan
    Seatzu, Carla
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2022, 67 (10) : 5541 - 5547
  • [48] State feedback based deadlock-free supervisor synthesis for bounded Petri nets
    Ru, Y
    Wu, WM
    Su, HY
    Chu, J
    2004 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN & CYBERNETICS, VOLS 1-7, 2004, : 1666 - 1671
  • [49] Verification of bounded Petri nets using integer programming
    Victor Khomenko
    Maciej Koutny
    Formal Methods in System Design, 2007, 30 : 143 - 176
  • [50] An Improved Approach to Test Diagnosability of Bounded Petri Nets
    Ran, Ning
    Su, Hongye
    Wang, Shouguang
    IEEE-CAA JOURNAL OF AUTOMATICA SINICA, 2017, 4 (02) : 297 - 303
12345