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
来源
基金
英国工程与自然科学研究理事会;
关键词
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 条
  • [21] Unfoldings of Bounded Hybrid Petri Nets
    Novosad, Petr
    Ceska, Milan
    COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2011, PT I, 2012, 6927 : 543 - 550
  • [22] Codiagnosability Analysis of Bounded Petri Nets
    Ran, Ning
    Su, Hongye
    Giua, Alessandro
    Seatzu, Carla
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2018, 63 (04) : 1192 - 1199
  • [23] Diagnosability analysis of bounded Petri nets
    Ran, Ning
    Hao, Jinyuan
    He, Zhou
    Seatzu, Carla
    2018 IEEE 23RD INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2018, : 1145 - 1148
  • [24] REDUCTION AND SYNTHESIS OF LIVE AND BOUNDED FREE-CHOICE PETRI NETS
    ESPARZA, J
    INFORMATION AND COMPUTATION, 1994, 114 (01) : 50 - 87
  • [25] Implementation of Algorithm of Petri Nets Distributed Synthesis into FPGA
    Bukowiec, Arkadiusz
    Tkacz, Jacek
    Gratkowski, Tomasz
    Gidlewicz, Tomasz
    INTERNATIONAL JOURNAL OF ELECTRONICS AND TELECOMMUNICATIONS, 2013, 59 (04) : 317 - 324
  • [26] An Efficient Algorithm for K-Diagnosability Analysis of Bounded and Unbounded Petri Nets
    Chouchane, A.
    Ghazel, M.
    IFAC PAPERSONLINE, 2024, 58 (01): : 162 - 167
  • [27] A symbolic reachability graph for coloured petri nets
    Chiola, G
    Dutheillet, C
    Franceschinis, G
    Haddad, S
    THEORETICAL COMPUTER SCIENCE, 1997, 176 (1-2) : 39 - 65
  • [28] Symbolic unfolding of parametric stopwatch Petri nets
    Claude Jard
    Didier Lime
    Olivier H. Roux
    Louis-Marie Traonouez
    Formal Methods in System Design, 2013, 43 : 493 - 519
  • [29] A Symbolic Model Checker for Petri Nets: pnmc
    Hamez, Alexandre
    TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY XI, 2016, 9930 : 297 - 306
  • [30] Symbolic Unfolding of Parametric Stopwatch Petri Nets
    Traonouez, Louis-Marie
    Grabiec, Bartosz
    Jard, Claude
    Lime, Didier
    Roux, Olivier H.
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2010, 6252 : 291 - +