Top

Published in:

2019 | OriginalPaper | Chapter

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

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

Published in: Formal Modeling and Analysis of Timed Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Mixed-Time Signal Temporal Logic

next chapter Stability and Performance Bounds in Cyclic Networks Using Network Calculus

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

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.059593CrossRef

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-8MathSciNetCrossRef

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

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

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.2588736MathSciNetCrossRef

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

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_17CrossRefMATH

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.75415MathSciNetCrossRef

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

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_7CrossRefMATH

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_37CrossRef

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)CrossRef

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_33CrossRefMATH

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.008CrossRef

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.030MathSciNetCrossRef

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_5CrossRefMATH

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.2200372MathSciNetCrossRef

18.

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

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.021CrossRef

20.

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

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_41CrossRef

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-5MathSciNetCrossRef

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.940942MathSciNetCrossRef

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.333987MathSciNetCrossRef

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)

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-2MathSciNetCrossRef

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.21072CrossRef

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.412626MathSciNetCrossRefMATH

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

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

Title: A State Class Construction for Computing the Intersection of Time Petri Nets Languages
Authors: Éric Lubat
Silvano Dal Zilio
Didier Le Botlan
Yannick Pencolé
Audine Subias
Publisher: Springer International Publishing
Book: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-030-29661-2

Electronic ISBN: 978-3-030-29662-9

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-29662-9_5

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner