Skip to main content
SpringerLink
Log in

On the composition of time Petri nets

  • Published:
Discrete Event Dynamic Systems Aims and scope Submit manuscript

Abstract

Complex systems are often designed and built from smaller pieces, called components. Components are open sub-systems meant to be combined (or composed) to form other components or closed systems. It is well known that Petri nets allow such a component based modeling, relying on parallel composition and transition synchronization. However, synchronizing transitions that carry temporal constraints does not yield a compositional method for assembling components, a highly desirable property. The paper addresses this particular problem: how to build complex systems in a compositional manner from components specified by Time Petri nets (TPN). A first solution is proposed, adequate for a particular subclass of Time Petri nets but significantly increasing the complexity of components. Then an improved solution is developed, relying on an extension of Time Petri nets with two relations added on transitions. This latter solution requires a much simpler transformation of nets, does not significantly increase their complexity, and is applicable to a larger class of TPN.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17

Similar content being viewed by others

Notes

  1. For conciseness, ( ∀ x = (y,...,z))(P) stands for \((\forall (x,y,\dots,z))(x = (y,\dots,z) \Rightarrow P)\).

References

  • Bérard B, Cassez F, Haddad S, Roux OH, Lime D (2005a) Comparison of the expressiveness of timed automata and time Petri nets. In: Formal modeling and analysis of timed systems (FORMATS). LNCS 3829, pp 211–225

  • Bérard B, Cassez F, Haddad S, Roux OH, Lime D (2005b) When are timed automata weakly timed bisimilar to time Petri nets? In: 25th conference on foundations of software technology and theoretical computer science. LNCS 3821. Springer, pp 261–272

  • Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. IFIP Congr Ser 9:41–46

    Google Scholar 

  • Berthomieu B, Vernadat F (2003) State class constructions for branching analysis of time Petri nets. In: Proc. tools and algorithms for the construction and analysis of systems. LNCS 2619. Springer

  • Berthomieu B, Ribet P-O, Vernadat F (2003) L’outil Tina—construction d’espaces d’etats abstraits pour les réseaux de Petri et réseaux temporels. In: Proc. Modélisation des Systèmes Réactifs, Metz, France

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

    Article  MATH  Google Scholar 

  • Berthomieu B, Peres F, Vernadat F (2006) Bridging the gap between timed automata and bounded time Petri nets. In: 4th int. conf. on formal modelling and analysis of timed systems (FORMATS). LNCS 4202. Springer

  • Boyer M, Roux O (2007) Comparison of the expressiveness of arc, place and transition time Petri nets. In: Kleijn J, Yakovlev A (eds) Petri nets and other models of concurrency—ICATPN 2007. Lecture notes in computer science, vol 4546. Springer Berlin/Heidelberg, pp 63–82

    Chapter  Google Scholar 

  • Bouyer P, Haddad S, Reynier P-A (2006) Extended timed automata and time Petri nets. In: Proc. of 6th international conference on application of concurrency to system design (ACSD’06), Turku, Finland. IEEE Computer Society Press

  • Browne MC, Clarke EM, Grümberg O (1988) Characterizing finite Kripke structures in propositional temporal logics. TCS 59:115–131

    Article  MATH  Google Scholar 

  • Bucci G, Vicario E (1995) Compositional validation of time-critical systems using communicating time Petri nets. IEEE Trans Softw Eng 21(12):969–992

    Article  Google Scholar 

  • Cassez F, Roux OH (2006) Structural translation from time Petri nets to timed automata. J Syst Softw 29(1):1456–1468

    Article  Google Scholar 

  • Gardey G, Lime D, Magnin M, Roux OH (2005) Roméo: a tool for analyzing time Petri nets. In: 17th international conference on computer aided verification, CAV’05. LNCS 3576. Springer

  • Gössler G, Sifakis J (2003) Composition for components-based modeling. In: Formal methods for components and objects. LNCS 2852. Springer, pp 443–466

  • Hack M (1976) Petri net languages. Technical Report 159. MIT, Cambridge, MA

  • Larsen KG, Pettersson P, Yi WY (1995) Model-checking for real-time systems. In: Fundamentals of computation theory. LNCS 965, pp 62–88

  • Merlin PM, Farber DJ (1976) Recoverability of communication protocols: implications of a theoretical study. IEEE Trans Commun 24(9):1036–1043

    Article  MATH  MathSciNet  Google Scholar 

  • Peres F (2010) Réseaux de Petri temporels à inhibitions/permissions—application à la modélisation de systèmes de tâches temps réel. Thèse de l’Université de Toulouse, Janvier

  • Peres F, Berthomieu B, Vernadat F (2009) Composer les réseaux de Petri temporels. Journal Europeen des Systemes Automatises 43(7–9):1001–1015. http://hal.archives-ouvertes.fr/hal-00438377/fr/

    Article  Google Scholar 

  • Sifakis J, Yovine S (1996) Compositional specification of timed systems. In: 13th annual symp. on theoretical aspects of computer science (STACS). LNCS 1046, Springer, pp 347–359

  • van Glabbeek R (1990) The linear time—branching time spectrum. In: Baeten J, Klop J (eds) CONCUR ’90 theories of concurrency: unification and extension. Lecture notes in computer science, vol 458. Springer Berlin/Heidelberg

    Google Scholar 

  • Wang Y (1990) Real-time behaviour of asynchronous agents. In: Baeten J, Klop J (eds) CONCUR ’90 theories of concurrency: unification and extension. Lecture notes in computer science, vol 458. Springer Berlin/Heidelberg, pp 502–520

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Lille Nord de France, 59000, Lille, France

    Florent Peres

  2. IFSTTAR, ESTAS, 59650, Villeneuve d’Ascq, France

    Florent Peres

  3. CNRS; LAAS, 7 avenue du colonel Roche, 31077, Toulouse, France

    Bernard Berthomieu & François Vernadat

  4. Université de Toulouse; UPS, INSA, INP, INSAE; LAAS, 31077, Toulouse, France

    Bernard Berthomieu & François Vernadat

Authors
  1. Florent Peres
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernard Berthomieu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. François Vernadat
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florent Peres.

Additional information

Florent Peres is on leave from LAAS-CNRS.

Rights and permissions

Reprints and permissions

About this article

Cite this article

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

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10626-011-0102-2

Keywords

Search

Navigation