[en] High-level Petri nets make models more concise and read-
able as compared to low-level Petri nets. However, usual verification
techniques such as state space analysis remain an open challenge for
both because of state space explosion. The contribution of this paper is
to propose an approach for property based reduction of the state space
of Algebraic Petri nets (a variant of high-level Petri nets). To achieve
the objective, we propose a slicing algorithm for Algebraic Petri nets
(APNSlicing). The proposed algorithm can alleviate state space even for
certain strongly connected nets. By construction, it is guaranteed that
the state space of sliced net is at most as big as the original net. We
exemplify our technique through the running case study of car crash
management system.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
KHAN, Yasir Imtiaz ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
risoldi, matteo; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Langue du document :
Anglais
Titre :
Optimizing algebraic petri net model checking by slicing
Date de publication/diffusion :
2013
Nom de la manifestation :
International Workshop on Modeling and Business Environments (ModBE’13)
Date de la manifestation :
June 24, 2013
Manifestation à portée :
International
Titre de l'ouvrage principal :
International Workshop on Modeling and Business Environments (ModBE’13) in Milano, Italy, June 24, 2013.
D. Buchs, S. Hostettler, A. Marechal, A. Linard, and M. Risoldi. Alpina: A symbolic model checker. Springer Berlin Heidelberg, pages 287-296, 2010.
J. R. Burch, E. Clarke, K. L. McMillan, D. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e, pages 428-439, 1990.
J. Chang and D. J. Richardson. Static and dynamic specification slicing. In In Proceedings of the Fourth Irvine Software Symposium, 1994.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8:244-263, 1986.
S. Hostettler, A. Marechal, A. Linard, M. Risoldi, and D. Buchs. High-level petri net model checking with alpina. Fundamenta Informaticae, 113(3-4):229-264, Aug. 2011.
K. Jensen. Coloured petri nets. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Central Models and Their Properties, volume 254 of Lecture Notes in Computer Science, pages 248-299. Springer Berlin Heidelberg, 1987.
Y. I. Khan. A formal approach for engineering resilient car crash management system. Technical Report TR-LASSY-12-05, University of Luxembourg, 2012.
L. Lamport. What good is temporal logic. Information processing, 83:657-668, 1983.
W. J. Lee, H. N. Kim, S. D. Cha, and Y. R. Kwon. A slicing-based approach to enhance petri net reachability analysis. Journal of Research Practices and Information Technology, 32:131-143, 2000.
M. Llorens, J. Oliver, J. Silva, S. Tamarit, and G. Vidal. Dynamic slicing techniques for petri nets. Electron. Notes Theor. Comput. Sci., 223:153-165, Dec. 2008.
A. Rakow. Slicing petri nets with an application to workflow verification. In Proceedings of the 34th conference on Current trends in theory and practice of computer science, SOFSEM'08, pages 436-447, Berlin, Heidelberg, 2008. Springer - Verlag.
A. Rakow. Slicing and Reduction Techniques for Model Checking Petri Nets. PhD thesis, University of Oldenburg, 2011.
A. Rakow. Safety slicing petri nets. In S. Haddad and L. Pomello, editors, Application and Theory of Petri Nets, volume 7347 of Lecture Notes in Computer Science, pages 268-287. Springer Berlin Heidelberg, 2012.
W. Reisig. Petri nets and algebraic specifications. Theor. Comput. Sci., 80(1):1-34, 1991.
K. Schmidt. T-invariants of algebraic petri nets. Informatik-Bericht, 1994.
A. Valmari. The state explosion problem. In Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, pages 429-528, London, UK, UK, 1998. Springer-Verlag.
M. Weiser. Program slicing. In Proceedings of the 5th international conference on Software engineering, ICSE '81, pages 439-449, Piscataway, NJ, USA, 1981. IEEE Press.
