Hanifa Boucheneb
Abstract
The main problem of verification techniques based on exploration of (reachable) state space is the state explosion problem. In timed models, abstract states reached by different interleavings of the same set of transitions are, in general, different and their union is not necessarily an abstract state. To attenuate this state explosion, it would be interesting to reduce the redundancy caused by the interleaving semantics by agglomerating all these abstract states whenever their union is an abstract state.
This article considers the time Petri net model and establishes some sufficient conditions that ensure that this union is an abstract state. In addition, it proposes a procedure to compute this union without computing beforehand intermediate abstract states. Finally, it shows how to use this result to improve the reachability analysis.
- Behrmann, G., Bouyer, P., Larsen, K. G., and Pelánek, R. 2006. Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Trans. 8, 3. Google Scholar
Digital Library
- Ben Salah, R., Bozga, M., and Maler, O. 2006. On interleaving in timed automata. In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR’06). Lecture Notes in Computer Science, vol. 4137, 465--476. Google ScholarDigital Library
- Bengtsson, J. 2002. Clocks, DBMs and states in timed systems. PhD thesis, Department of Information Technology, Uppsala University.Google Scholar
- Berthomieu, B. and Diaz, M. 1991. Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Engin. 17, 3. Google ScholarDigital Library
- Berthomieu, B. and Vernadat, F. 2003. State class constructions for branching analysis of time Petri nets. In Proceedings of the 9th International Conference onTools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2619. Google ScholarDigital Library
- Berthomieu, B., Peres, F., and Vernadat, F. 2007. Model-checking bounded prioriterized time petri nets. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA’07). Lecture Notes in Computer Science, vol. 4762. Google ScholarDigital Library
- Boucheneb, H. and Hadjidj, R. 2006. CTL* model checking for time Petri nets. J. Theor. Comput. Sci. 353, 1--3. Google ScholarDigital Library
- Boucheneb, H. and Rakkay, H. 2008. A more efficient time Petri net state space abstraction useful to model checking timed linear properties. In J. Fundamenta Informaticae 88, 4, 469--495. Google ScholarDigital Library
- Boucheneb, H. and Barkaoui, K. 2009a. Covering steps graphs of time Petri nets. In Proceedings of the 10th International Workshop on Verification of Infinite-State Systems. Electronic Notes in Theoretical Computer Science, vol. 239, 155--165. Google ScholarDigital Library
- Boucheneb, H. and Barkaoui, K. 2009b. On combining the ready sets with the covering steps methods. In Proceedings of the 3rd International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS’09), Electronic Workshops in Computing series, eWiC http://ewic.bcs.org/.Google Scholar
- Boucheneb, H., Gardey, G., and Roux, O. H. 2009. TCTL model checking of time Petri nets. J. Logic Comput. 19, 6, 1509--1540. Google ScholarDigital Library
- Fass, D. 2009. Clock Matrix Diagrams. Bachelors Thesis, Reactive Systems Group, Department of Computer Science, Universitat des Saarlandes.Google Scholar
- Gardey, G., Roux, O. H., and Roux, O. F. 2004. Using zone graph method for computing the state space of a time Petri net. In Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 2791. Springer.Google Scholar
- Hadjidj, R. and Boucheneb, H. 2008. Improving state class constructions for CTL* model checking of time Petri nets. Int. J. Softw. Tools Technol. Trans. 10, 2, 167--184. Google ScholarDigital Library
- Merlin, P. M. 1974. A study of the recoverability of computing systems. PhD thesis, University of California, Irvine, CA. Google ScholarDigital Library
- Murata, T. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4.Google ScholarCross Ref
- Penczek, W. and Pólrola, A. 2001. Abstraction and partial order reductions for checking branching properties of time Petri nets. In Proceedings of the 22nd International Conference on Applications and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 2075, Springer, 323--342. Google ScholarDigital Library
- Penczek, W. and Pólrola, A. 2004. Specification and model checking of temporal properties in time Petri nets and timed automata. In Proceedings of the 25th International Conference on Applications and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 3099. Springer.Google Scholar
- Pradubsuwun, D. Yoneda, T., and Myers, C. 2005. Partial order reduction for detecting safety and timing failures of timed circuits. IEICE Trans. Inf. Syst. E88-D, 7. Google ScholarDigital Library
- Ribet, P. O., Vernadat, F., and Berthomieu, B. 2002. On combining the persistent sets method with the covering steps graph method. In Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems. Lecture Notes in Computer Science. vol. 2529. Springer. Google ScholarDigital Library
- Yoneda, T. and Schlingloff, B. H. 1997. Efficient verification of parallel real-time systems. Formal Methods Syst. Des. 11, 2, 187--215. Google ScholarDigital Library
- Yoneda, T. and Ryuba, H. 1998. CTL model checking of Time Petri Nets using geometric regions. IEICE Trans. Inf. Syst. E99-D, 3, 1--10.Google Scholar
Index Terms
- Reducing Interleaving Semantics Redundancy in Reachability Analysis of Time Petri Nets
Recommendations
Reachability Analysis of P-time Petri Nets with Parametric Markings
ACSD '12: Proceedings of the 2012 12th International Conference on Application of Concurrency to System DesignThis paper deals with the verification of P-Time Petri nets with parametric markings. It investigates the verification of reach ability properties in the case of an upward-closed set of initial markings. We propose an efficient state space abstraction ...
Non Equivalence between Time Petri Nets and Time Stream Petri Nets
PNPM '99: Proceedings of the The 8th International Workshop on Petri Nets and Performance ModelsIt had been shown that Merlin's Time Petri Nets are a special case of Time Stream Petri Nets. In this paper, we show that it does not exist a time equivalence between both models. We extend first this result to the nonequivalence of Timed Automata and ...
Expressiveness of Petri Nets with Stopwatches. Dense-time Part
With this contribution, we aim to draw a comprehensive classification of Petri nets with stopwatches w.r.t. expressiveness and decidability issues. This topic is too ambitious to be summarized in a single paper. That is why we present our results in two ...
Comments