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 条
  • [31] Symbolic unfolding of parametric stopwatch Petri nets
    Jard, Claude
    Lime, Didier
    Roux, Olivier H.
    Traonouez, Louis-Marie
    FORMAL METHODS IN SYSTEM DESIGN, 2013, 43 (03) : 493 - 519
  • [32] Decomposition theorems for bounded persistent Petri nets
    Best, Eike
    Darondeau, Philippe
    APPLICATIONS AND THEORY OF PETRI NETS, 2008, 5062 : 33 - +
  • [33] Causality in Bounded Petri Nets is MSO Definable
    Oliveira, Mateus de Oliveira
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, 2016, 9803 : 200 - 214
  • [34] Representing bounded Petri nets by process calculi
    Dong, Zhen-Hua
    Dong, Xiao-Ju
    Shanghai Jiaotong Daxue Xuebao/Journal of Shanghai Jiaotong University, 2011, 45 (07): : 980 - 984
  • [35] BOUNDED SELF-STABILIZING PETRI NETS
    CHERKASOVA, L
    HOWELL, RR
    ROSIER, LE
    ACTA INFORMATICA, 1995, 32 (03) : 189 - 207
  • [36] Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
    Arias, Jaime
    Bae, Kyungmin
    Olarte, Carlos
    Olveczky, Peter Csaba
    Petrucci, Laure
    Romming, Fredrik
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2023, 2023, 13929 : 369 - 392
  • [37] Symbolic model checking of dual transition Petri nets
    Varea, M
    Al-Hashimi, BM
    Cortés, LA
    Eles, P
    Peng, Z
    CODES 2002: PROCEEDINGS OF THE TENTH INTERNATIONAL SYMPOSIUM ON HARDWARE/SOFTWARE CODESIGN, 2002, : 43 - 48
  • [38] Factorization Properties of Symbolic Unfoldings of Colored Petri Nets
    Chatain, Thomas
    Fabre, Eric
    APPLICATIONS AND THEORY OF PETRI NETS, PROCEEDINGS, 2010, 6128 : 165 - +
  • [39] SYMBOLIC EXECUTION OF CONCURRENT SYSTEMS USING PETRI NETS
    GHEZZI, C
    MANDRIOLI, D
    MORASCA, S
    PEZZE, M
    COMPUTER LANGUAGES, 1989, 14 (04): : 263 - 281
  • [40] Symbolic Reachability Analysis of Integer Timed Petri Nets
    Wan, Min
    Ciardo, Gianfranco
    SOFSEM 2009-THEORY AND PRACTICE OF COMPUTER SCIENCE, PROCEEDINGS, 2009, 5404 : 595 - 608
12345