A More Efficient Time Petri Net State Space Abstraction Useful to Model Checking Timed Linear Properties

• Autorzy: Bouchene H. , Rakkay H.
• Języki publikacji: EN

Abstrakty

EN

We consider here time Petri nets (TPN model). We first propose an abstraction to its generally infinite state space which preserves linear properties of the TPN model. Comparing with TPN abstractions proposed in the literature, our abstraction produces graphs which are both smaller and faster to compute. In addition, our characterization of agglomerated states allows a significant gain in space. Afterwards, we show how to apply Yoneda's partial order reduction technique to construct directly reduced graphs useful to verify LTL_x properties of the model. Using our approach, both time and space complexities are reduced. Finally, we propose a time extension for Büchi automata which is useful to model checking timed linear properties of the model, using the abstraction proposed here.

Słowa kluczowe

EN

Time Petri Net; State class graph; state explosion problem; partial order techniques; independent transitions; timed linear properties; Interval timed Büchi automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 4
• Strony: 469--495
• Opis fizyczny: bibliogr. 21 poz., tab., wykr.

Twórcy

autor

Bouchene H.

autor

Rakkay H.

• Department of Computer Engineering, Ecole Polytechnique de Montréal P.O. Box 6079, Station Centre-ville, Montréal, Québec,Canada, H3C 3A7,

Bibliografia

• [1] Bengtsson, J.: Clocks, DBMs and States in Timed Systems, PhD thesis, Dept. of Information Technology, Uppsala University, 2002.
• [2] B. Berthomieu, F. Vernadat, State class constructions for branching analysis of time Petri nets, volume 2619 of LNCS, 2003.
• [3] B. Berthomieu, M. Diaz, Modeling and verification of time dependent systems using time Petri nets, IEEE Transactions on Software Engineering, vol 17, no 3, 1991.
• [4] H. Boucheneb, R. Hadjidj, CTL* model checking for time Petri nets, Journal of Theoretical Computer Science TCS, vol. 353/1-3, pages 208-227, 2006.
• [5] H. Boucheneb, J. Mullins, Analyse des réseaux de Petri temporels: Calcul des classes en O(n2) et des temps de chemin en O(m × n), Technique et Science Informatiques, vol. 22, no. 4, 2003.
• [6] H. Boucheneb, G. Berthelot, Toward a simplified building of time Petri nets reachability graph, In Proc. of Petri Nets Performance Models PNPM'93, pages 46-55, Toulouse, France, IEEE computer society press, 1993.
• [7] C. Daws, R. Gerth, B. Knaack and R. Kuiper, Partial-order reduction techniques for real-time model checking, Formal Aspects of Computing, (10), pages 469-482, Springer, 1998.
• [8] S. Edelkamp, S. Leue, and A. Lluch-Lafuente, Partial-order reduction and trail improvement in directed model checking,International Journal of Software Tools Technology Transfer (2004)6, pages 277301, Springer-Verlag, November 2004.
• [9] Guillaume Gardey, O. H. Roux, and O. F. Roux, State space computation and analysis of time Petri nets, Theory and Practice of Logic Programming (TPLP), Special Issue on Specification Analysis and Verification of Reactive Systems, 6(3):301-320, 2006.
• [10] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, volume 1032 of LNCS, Springer-Verlag, 1996.
• [11] V. Khomenko, M. Koutny, Towards an Efficient Algorithm for Unfolding Petri Nets, In Proc. Concur'2001. Springer, LNCS 2154 (2001): 366-380.
• [12] D. Lime, O.(H.) Roux, Model checking of time Petri nets using the state class timed automaton, Journal of Discrete Events Dynamic Systems - Theory and Applications (DEDS), 16(2):179-205, 2006.
• [13] D. Peled and T. Wilke, Stutter invariant temporal properties are expressible without the next-time operator. Information Processing Letters, 63(5), 1997.
• [14] W. Penczek and A. Pólrola, Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata, In Proc. of ICATPN, volume 3099 of LNCS, pages 37-76, Springer-Verlag, 2004.
• [15] E. G. Mercer, C. J. Myers, and T. Yoneda, Improved POSET timing analysis in timed Petri nets., In Proc. of the 10thWorkshop on Synthesis And System Integration of Mixed Technologies, pages 127-134, 2001.
• [16] W. Penczek, A. Pólrola, Abstraction and partial order reductions for checking branching properties of time Petri nets, In Proc. of ICATPN, volume 2075 of LNCS , pages 323-342, 2001.
• [17] S. Tripakis, S. Yovine, Analysis of Timed Systems using Time-abstracting Bisimulations, Formal Methods in System Design, Vol.18(1), pp 25-68, Kluwer Academic Publishers, 2001
• [18] D. Pradubsuwun, T.Yoneda, C. Myers, Partial order reduction for detecting safety and timing failures of timed circuits, IEICE Trans. Inf. & Syst., vol. E88-D, no. 7, July 2005.
• [19] T.G. Rokicki, Representing and Modeling Digital Circuits, PhD Thesis, Standford University, 1993.
• [20] A. Valmari, A stubborn attack on state explosion, volume 531 of LNCS, Springer-Verlag, 1990.
• [21] T.Yoneda, B.H.Schlingloff, Efficient Verification of Parallel Real-Time Systems, Formal Methods in System Design, Kluwer Academic Publishers, vol. 11, no. 2, pp.187-215, August 1997.