Efficient reachability analysis of bounded Petri nets using constraint programming

作者: T. Bourdeaud'huy , P. Yim , S. Hanafi

DOI: 10.1109/ICSMC.2004.1399939

关键词: Constraint programmingReachability problemBounded functionStochastic Petri netReachabilityAlgorithmPetri netProcess architectureComputer scienceGraph (abstract data type)

摘要: In this paper, we consider the Petri net (PNs) reachability problem, which consists of finding transition firing sequences leading to a given target marking. We focus on bounded nets for develop correct and complete algorithm using logical abstraction technique proposed by Benasser Yim. define that PN sequential depth parameter, corresponds maximal number transitions fire in order reach any marking graph.

参考文章(11)
Kurt Lautenbach, Linear Algebraic Techniques for Place/Transition Nets Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986-Part I. pp. 142- 167 ,(1986) , 10.1007/BFB0046839
Peter Huber, Arne M. Jensen, Leif O. Jepsen, Kurt Jensen, Towards reachability trees for high-level Petri nets applications and theory of petri nets. pp. 215- 233 ,(1985) , 10.1007/3-540-15204-0_13
Doo Yong Lee, F. DiCesare, Scheduling flexible manufacturing systems using Petri nets and heuristic search international conference on robotics and automation. ,vol. 10, pp. 123- 132 ,(1994) , 10.1109/70.282537
Robert M. Keller, Formal verification of parallel programs Communications of The ACM. ,vol. 19, pp. 371- 384 ,(1976) , 10.1145/360248.360251
T. Murata, Petri nets: Properties, analysis and applications Proceedings of the IEEE. ,vol. 77, pp. 541- 580 ,(1989) , 10.1109/5.24143
Jean-Claude Fernandez, Laurent Mounier, Claude Jard, Thierry J�ron, On-the-fly verification of finite transition systems computer aided verification. ,vol. 1, pp. 251- 273 ,(1992) , 10.1007/BF00121127
Antti Valmari, Stubborn sets for reduced state space generation applications and theory of petri nets. pp. 491- 515 ,(1991) , 10.1007/3-540-53863-1_36
J. Gunnarsson, Symbolic tools for verification of large scale DEDS systems man and cybernetics. ,vol. 1, pp. 722- 727 ,(1998) , 10.1109/ICSMC.1998.725499
Markus Lindqvist, Parameterized reachability trees for predicate/transition nets applications and theory of petri nets. pp. 1- 120 ,(1991) , 10.1007/3-540-56689-9_49
G. Memmi, G. Roucairol, Linear Algebra in Net Theory Proceedings of the Advanced Course on General Net Theory of Processes and Systems: Net Theory and Applications. pp. 213- 223 ,(1979) , 10.1007/3-540-10001-6_24