Skip to main content
SpringerLink
Log in

A State Class Construction for Computing the Intersection of Time Petri Nets Languages

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11750))

Abstract

We propose a new method for computing the language intersection of two Time Petri nets (TPN); that is the sequence of labels in timed traces common to the execution of two TPN. Our approach is based on a new product construction between nets and relies on the State Class construction, a widely used method for checking the behaviour of TPN. We prove that this new construct does not add additional expressive power, and yet that it can leads to very concise representation of the result. We have implemented our approach in a new tool, called Twina. We report on some experimental results obtained with this tool and show how to apply our approach on two interesting problems: first, to define an equivalent of the twin-plant diagnosability methods for TPN; then as a way to check timed properties without interfering with a system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We may assume that there is a countable set of all possible transitions (identifiers) and that different nets have distinct transitions.

References

  1. Abid, N., Dal Zilio, S., Le Botlan, D.: A formal framework to specify and verify real-time properties on critical systems. Int. J. Crit. Comput. Based Syst. (IJCCBS) 5(1/2) (2014). https://doi.org/10.1504/IJCCBS.2014.059593

    Article  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2) (1994). https://doi.org/10.1016/0304-3975(94)90010-8

    Article  MathSciNet  Google Scholar 

  3. Arnold, A.: Nivat’s processes and their synchronization. Theor. Comput. Sci. 281(1–2) (2002). https://doi.org/10.1016/S0304-3975(02)00006-3

    Article  MathSciNet  Google Scholar 

  4. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2) (2002). https://doi.org/10.1145/506147.506151

    Article  MathSciNet  Google Scholar 

  5. Basile, F., Cabasino, M.P., Seatzu, C.: Diagnosability analysis of labeled time Petri net systems. IEEE Trans. Autom. Control 62(3) (2017). https://doi.org/10.1109/TAC.2016.2588736

    Article  MathSciNet  Google Scholar 

  6. Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Software Engineering and Formal Methods (SEFM). IEEE (2006). https://doi.org/10.1109/SEFM.2006.27

  7. Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005). https://doi.org/10.1007/11603009_17

    Chapter  MATH  Google Scholar 

  8. Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Eng. 17(3) (1991). https://doi.org/10.1109/32.75415

    Article  MathSciNet  Google Scholar 

  9. Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Proceedings IFIP (1983)

    Google Scholar 

  10. Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time Petri nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 82–97. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_7

    Chapter  MATH  Google Scholar 

  11. Berthomieu, B., Peres, F., Vernadat, F.: Model checking bounded prioritized time Petri nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 523–532. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75596-8_37

    Chapter  Google Scholar 

  12. Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and time Petri nets. Int. J. Prod. Res. 42(14), 2741–2756 (2004)

    Article  Google Scholar 

  13. Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 442–457. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_33

    Chapter  MATH  Google Scholar 

  14. Bourdil, P.A., Berthomieu, B., Dal Zilio, S., Vernadat, F.: Symmetry reduction for time Petri net state classes. Sci. Comput. Program. 132(2) (2016). https://doi.org/10.1016/j.scico.2016.08.008

    Article  Google Scholar 

  15. Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: When are timed automata weakly timed bisimilar to time Petri nets? Theoret. Comput. Sci. 403(2–3) (2008). https://doi.org/10.1016/j.tcs.2008.03.030

    Article  MathSciNet  Google Scholar 

  16. Bérard, B., Gastin, P., Petit, A.: Intersection of regular signal-event (timed) languages. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 52–66. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_5

    Chapter  MATH  Google Scholar 

  17. Cabasino, M.P., Giua, A., Lafortune, S., Seatzu, C.: A new approach for diagnosability analysis of Petri nets using verifier nets. IEEE Trans. Autom. Control 57(12) (2012). https://doi.org/10.1109/TAC.2012.2200372

    Article  MathSciNet  Google Scholar 

  18. Cabasino, M.P., Giua, A., Seatzu, C.: Discrete event diagnosis using Petri nets. In: ICINCO-ICSO (2009)

    Google Scholar 

  19. Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. J. Syst. Softw. 79(10) (2006). https://doi.org/10.1016/j.jss.2005.12.021

    Article  Google Scholar 

  20. Cimatti, A., Pecheur, C., Cavada, R.: Formal verification of diagnosability via symbolic model checking. In: IJCAI (2003)

    Google Scholar 

  21. Dal Zilio, S.: TWINA: a realtime model-checker for analyzing Twin-TPN (2019). https://projects.laas.fr/twina/

  22. Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_41

    Chapter  Google Scholar 

  23. Gougam, H.E., Pencolé, Y., Subias, A.: Diagnosability analysis of patterns on bounded labeled prioritized Petri nets. Discrete Event Dyn. Syst. 27(1) (2017). https://doi.org/10.1007/s10626-016-0234-5

    Article  MathSciNet  Google Scholar 

  24. Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans. Autom. Control 46(8) (2001). https://doi.org/10.1109/9.940942

    Article  MathSciNet  Google Scholar 

  25. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM (JACM) 47(2) (2000). https://doi.org/10.1145/333979.333987

    Article  MathSciNet  Google Scholar 

  26. Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. thesis, Department of Information and Computer Science, University of California (1974)

    Google Scholar 

  27. Peres, F., Berthomieu, B., Vernadat, F.: On the composition of time Petri nets. Discrete Event Dyn. Syst. 21(3) (2011). https://doi.org/10.1007/s10626-011-0102-2

    Article  MathSciNet  Google Scholar 

  28. Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989). https://doi.org/10.1109/5.21072

    Article  Google Scholar 

  29. Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40(9), 1555–1575 (1995). https://doi.org/10.1109/9.412626

    Article  MathSciNet  MATH  Google Scholar 

  30. Toussaint, J., Simonot-Lion, F., Thomesse, J.P.: Time constraint verification methods based on time Petri nets. In: Workshop on Future Trends of Distributed Computing Systems. IEEE (1997). https://doi.org/10.1109/FTDCS.1997.644736

  31. Tripakis, S.: Fault diagnosis for timed automata. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT) (2002). https://doi.org/10.1007/3-540-45739-9_14

    Google Scholar 

  32. Wang, X., Mahulea, C., Silva, M.: Diagnosis of time Petri nets using fault diagnosis graph. IEEE Trans. Autom. Control 60(9) (2015). https://doi.org/10.1007/978-3-642-15297-9_12

    Google Scholar 

Download references

Acknowledgments

The authors are grateful to Thomas Hujsa and Pierre-Emmanuel Hladik for their valuable comments. We also want to thank Bernard Berthomieu, without whom none of this would have been possible; our work is a tribute to the versatility and the enduring qualities of the state class construction that he pioneered more than 30 years ago.

Author information

Authors and Affiliations

  1. LAAS-CNRS, Université de Toulouse, CNRS, INSA, Toulouse, France

    Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé & Audine Subias

Authors
  1. Éric Lubat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvano Dal Zilio
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Didier Le Botlan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yannick Pencolé
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Audine Subias
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Silvano Dal Zilio .

Editor information

Editors and Affiliations

  1. Université Paris 13, Villetaneuse, France

    Étienne André

  2. University of Twente, Enschede, The Netherlands

    Mariëlle Stoelinga

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lubat, É., Dal Zilio, S., Le Botlan, D., Pencolé, Y., Subias, A. (2019). A State Class Construction for Computing the Intersection of Time Petri Nets Languages. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29662-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29661-2

  • Online ISBN: 978-3-030-29662-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation