Stubborn Sets for Time Petri Nets

Abstract

The main limitation of the verification approaches based on state enumeration is the state explosion problem. The partial order reduction techniques aim at attenuating this problem by reducing the number of transitions to be fired from each state while preserving properties of interest. Among the reduction techniques proposed in the literature, this article considers the stubborn set method of Petri nets and investigates its extension to time Petri nets. It establishes some useful sufficient conditions for stubborn sets, which preserve deadlocks and k-boundedness of places.

References

1. W. Belluomini and C. J. Myers. 2000. Timed state space exploration using POSETs. IEEE Transactions on Computer-Aided Design of Integrated Circuits 19, 5 (2000), 501--520.
2. J. Bengtsson. 2002. Clocks, DBMs and States in Timed Systems. Ph.D. thesis, Dept. of Information Technology, Uppsala University.
3. J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi. 1998. Partial order reductions for timed systems. In 9th International Conference on Concurrency Theory (CONCUR’98). Lecture Notes in Computer Science, Vol. 1466. Springer, Berlin, 485--500.
4. B. Bérard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux. 2013. The expressive power of time Petri nets. Theoretical Computer Science 474 (2013), 1--20.
5. B. Berthomieu and M. Diaz. 1991. Modeling and verification of time dependent systems using time petri nets. IEEE Transactions on Software Engineering 17, 3 (1991), 259--273.
6. B. Berthomieu and F. Vernadat. 2003. State class constructions for branching analysis of time Petri nets. In 9th International Conference of Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 2619. Springer, 442--457.
7. H. Boucheneb and K. Barkaoui. 2013. Reducing interleaving semantics redundancy in reachability analysis of time Petri nets. ACM Transactions on Embedded Computing Systems 12, 1 (2013), 259--273.
8. H. Boucheneb, G. Gardey, and O. H. Roux. 2009. TCTL model checking of time Petri nets. Logic and Computation 19, 6 (2009), 1509--1540.
9. H. Boucheneb and R. Hadjidj. 2006. CTL* model checking for time Petri nets. Theoretical Computer Science 353, 1--3 (2006), 208227.
10. H. Boucheneb, D. Lime, and O. H. Roux. 2013. On multi-enabledness in time Petri nets. In 34th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN’13). Lecture Notes in Computer Science, Vol. 7927. Springer, 130--149.
11. H. Boucheneb and H. Rakkay. 2008. A more efficient time Petri net state space abstraction useful to model checking timed linear properties. Fundamenta Informaticae 88, 4 (2008), 469--495.
12. M. Boyer and M. Diaz. 2001. Multiple-enabledness of transitions in time petri nets. In 9th IEEE International Workshop on Petri Nets and Performance Models. IEEE Computer Society, 219--228.
13. T. Chatain and C. Jard. 2006. Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency (ICATPN’06). Lecture Notes in Computer Science, Vol. 4024. Springer, 125--145.
14. T. Chatain and C. Jard. 2013. Back in time petri net. In 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’13). Lecture Notes in Computer Science, Vol. 8053. Springer, 91--105.
15. D. Delfieu, M. Sogbohossou, L. M. Traonouez, and S. Revol. 2007. Parameterized study of a time Petri net. In Cybernetics and Information Technologies, Systems and Applications: CITSA. 89--90.
16. G. M. Delgadillo and S. P. Llano. 2006. Scheduling application using Petri nets: A case study: Intergráficas s.a. In 9th International Conference on Production Research. 1--6.
17. P. Godefroid. 1996. An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, Vol. 1032. Springer-Verlag, New York.
18. J. Hakansson and P. Pettersson. 2007. Partial order reduction for verification of real-time components. In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’07). Lecture Notes in Computer Science. Springer, 211--226.
19. J. Lilius. 1998. Efficient state space search for time Petri nets. In MFCSÕ98 Workshop on Concurrency Algorithms and Tools. Electronic Notes of Theoretical Science, Vol. 8. Elsevier Science B.V, Brno, Czech Republic, 113--133.
20. D. Lugiez, P. Niebert, and S. Zennou. 2005. A partial order semantics approach to the clock explosion problem of timed automata. Theoretical Computer Science 345, 1 (2005), 27--59.
21. E. G. Mercer, C. J. Myers, and T. Yoneda. 2001. Improved POSET timing analysis in timed Petri nets. In International Workshop on Synthesis and System Integration of Mixed Technologies. 1--6.
22. M. Minea. 1999. Partial order reduction for model checking of timed automata. In 10th International Conference on Concurrency Theory (CONCUR’99). Lecture Notes in Computer Science, Vol. 1664. Springer, Berlin, 431--446.
23. D. Peled. 1993. All from one, one for all: On model checking using representatives. In Computer Aided Verification, Costas Courcoubetis (Ed.). Lecture Notes in Computer Science, Vol. 697. Springer, Berlin, 409--423.
24. D. Peled and T. Wilke. 1997. Stutter invariant temporal properties are expressible without the next-time operator. Information Processing Letters 63, 5 (1997), 243--246.
25. D. Pradubsuwun, T. Yoneda, and C. Myers. 2005. Partial order reduction for detecting safety and timing failures of timed circuits. IEICE - Transactions on Information and Systems. E99-D(7) (2005), 1646--1661.
26. R. Ben Salah, M. Bozga, and O. Maler. 2006. On interleaving in timed automata. In 17th International Conference on Concurrency Theory (CONCUR’06). Lecture Notes in Computer Science, Vol. 4137. Springer, 465--476.
27. A. Semenov and A. Yakovlev. 1996. Verification of asynchronous circuits using time petri net unfolding. In 33rd Annual Conference on Design Automation (DAC’96). 59--62.
28. M. Sogbohossou and D. Delfeu. 2008. Temporal reduction in time petri net. In 3rd International Workshop on Design and Test (IDT’08). IEEE, 260--265.
29. A. Valmari. 1992. A stubborn attack on state explosion. Formal Methods in System Design 1, 4 (1992), 297--322.
30. A. Valmari. 1998. The State Explosion Problem. Lecture Notes in Computer Science, Vol. 1491. Springer, Berlin, 429--528 pages.
31. A. Valmari and H. Hansen. 2010. Can stubborn set be optimal. In 31st International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets’10). Lecture Notes in Computer Science, Vol. 6128. Springer, Berlin, 43--62.
32. T. Yoneda and H. Ryuba. 1998. CTL model checking of time petri nets using geometric regions. IEICE - Transactions on Information and Systems. E99-D(3) (1998), 297--306.
33. T. Yoneda and B. H. Schlingloff. 1997. Efficient verification of parallel real-time systems. Formal Methods in System Design 11, 2 (1997), 187--215.
34. T. Yoneda, A. Shibayama, B. H. Schlingloff, and E. M. Clarke. 1993. Efficient verification of parallel real-time systems. In Computer Aided Verification, Costas Courcoubetis (Ed.). Lecture Notes in Computer Science, Vol. 697. Springer, Berlin, 321--332.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification