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] 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
[42] Efficient encoding schemes for symbolic analysis of Petri nets
Pastor, E
Cortadella, J
DESIGN, AUTOMATION AND TEST IN EUROPE, PROCEEDINGS, 1998, : 790 - 795
[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] 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
[47] Verification of bounded Petri nets using integer programming
Khomenko, Victor
Koutny, Maciej
FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (02) : 143 - 176
[48] 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
[49] Verification of bounded Petri nets using integer programming
Victor Khomenko
Maciej Koutny
Formal Methods in System Design, 2007, 30 : 143 - 176
[50] Non-interference enforcement in bounded Petri nets
Basile, Francesco
De Tommasi, Gianmaria
Sterle, Claudio
2018 IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2018, : 4827 - 4832

← 1 2 3 4 5 →