Discrete Event Dynamic Systems

, Volume 23, Issue 4, pp 419–438 | Cite as

Shrinking of Time Petri nets

  • Didier Lime
  • Claude Martinez
  • Olivier H. Roux


The problem of the synthesis of time bounds enforcing good properties for reactive systems has been much studied in the literature. These works mainly rely on dioid algebra theory and require important restrictions on the structure of the model (notably by restricting to timed event graphs). In this paper, we address the problems of existence and synthesis of shrinkings of the bounds of the time intervals of a time Petri net, such that a given property is verified. We show that this problem is decidable for CTL properties on bounded time Petri nets. We then propose a symbolic algorithm based on the state class graph for a fragment of CTL. If the desired property “includes” k-boundedness, the proposed algorithm terminates even if the net is unbounded. A prototype has been implemented in our tool Romeo and the method is illustrated on a small case study from the literature.


Time Petri nets Time interval shrinking Model-checking State-class graph 


  1. Achour Z, Rezg N (2007) Time floating general mutual exclusion constraints. J Stud Inf Control 16(1):57–66Google Scholar
  2. Alur R, Henzinger TA, Vardi MY (1993) Parametric real-time reasoning. In: ACM symposium on theory of computing, pp 592–601Google Scholar
  3. Amari S, Demongodin I, Loiseau J (2005) Méthode formelle de commande sous contraintes de temps dans les dioides. Journal Européen des Systèmes Automatisés (Numéro spécial sur la Modélisation des Systèmes Réactifs, (MSR’05)) 39(1–3):319–334CrossRefGoogle Scholar
  4. André E, Chatain T, Encrenaz E, Fribourg L (2009) An inverse method for parametric timed automata. Int J Found Comput Sci 20(5):819–836MATHCrossRefGoogle Scholar
  5. Atto AM, Martinez C, Amari S (2011) Control of discrete event systems with respect to strict duration: supervision of an industrial manufacturing plant. Comput Inf Syst 61(4):1149–1159. doi: 10.1016/j.cie.2011.07.004 Google Scholar
  6. Bagnara R, Hill PM, Zaffanella E (2008) The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci Comput Program 72(1–2):3–21MathSciNetCrossRefGoogle Scholar
  7. Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time Petri nets. IEEE Trans Softw Eng 17(3):259–273MathSciNetCrossRefGoogle Scholar
  8. Berthomieu B, Vernadat F (2003) State class constructions for branching analysis of time Petri nets. In: TACAS 2003. Lecture notes in computer science, vol 2619, pp 442–457Google Scholar
  9. Berthomieu B, Lime D, Roux OH, Vernadat F (2007) Reachability problems and abstract state spaces for time Petri nets with stopwatches. Discrete Event Dyn Syst (Theory and Applications (DEDS)) 17(2):133–158MathSciNetMATHCrossRefGoogle Scholar
  10. Bloch C, Manier MA, Baptiste P, Varnier C (2010) Hoist scheduling problem. In: ISTE, pp 193–231. doi: 10.1002/9780470611050.ch8
  11. Bonhomme P, Aygalinc P, Calvez S (2001) Systèmes à contraintes de temps: validation, évaluation et contrôle. In: Modélisation des systèmes réactifs, MSR 01. Toulouse, FranceGoogle Scholar
  12. Boucheneb H, Gardey G, Roux OH (2009) TCTL model checking of time Petri nets. J Log Comput 19(6):1509–1540MathSciNetMATHCrossRefGoogle Scholar
  13. Boyer M, Roux OH (2008) On the compared expressiveness of arc, place and transition time Petri nets. Fundam Inform 88(3):225–249MathSciNetMATHGoogle Scholar
  14. Cassandras C, Lafortune S (1992) Introduction to discrete event systems. Kluwer AcademicGoogle Scholar
  15. Cook W, Hartmann M, Kannan R, McDiarmid C (1992) On integer points in polyhedra. Combinatorica 12(1):27–37MathSciNetMATHCrossRefGoogle Scholar
  16. Gardey G, Roux OF, Roux OH (2006) Safety control synthesis for time Petri nets. In: 8th international workshop on discrete event systems (WODES’06). IEEE Computer Society Press, Ann Arbor, pp 222–228CrossRefGoogle Scholar
  17. Giua A, DiCesare F, Silva M (1992) Generalized mutual exclusion constraints on nets with uncontrollable transitions. In: IEEE int. conf. on SMCGoogle Scholar
  18. Holloway LE, Krogh BH, Giua A (1997) A survey of Petri net methods for controlled discrete event systems. Discrete Event Dyn Syst 7(2):151–190MATHCrossRefGoogle Scholar
  19. Houssin L, Lahaye S, Boimond J (2007) Just in time control of constrained (max, +)-linear systems. Discrete Event Dyn Syst 17:159–178MathSciNetMATHCrossRefGoogle Scholar
  20. Hune T, Romijn J, Stoelinga M, Vaandrager FW (2001) Linear parametric model checking of timed automata. In: TACAS’01, LNCS, vol 2031. SpringerGoogle Scholar
  21. Katz RD (2007) Max-plus (a,b)-invariant spaces and control of timed discrete event systems. IEEE Trans Automat Contr 52:229–241CrossRefGoogle Scholar
  22. Kim J, Lee T (2003) Schedule stabilization and robust timing control for time-constrained cluster tools. In: IEEE international conference on robotics and automation. Taipei, Taiwan, pp 1039–1044Google Scholar
  23. Larsen KG, Pettersson P, Yi W (1995) Model-checking for real-time systems. In: Fundamentals of computation theory, pp 62–88Google Scholar
  24. Lee TE (2008) A review of scheduling theory and methods for semiconductor manufacturing cluster tools. In: Winter simulation conference, pp 2127–2135Google Scholar
  25. Li ZW, Zhou MC (2009) Deadlock resolution in automated manufacturing systems: a novel Petri net approach, 1st edn. SpringerGoogle Scholar
  26. Lime D, Roux OH, Seidner C, Traonouez LM (2009) Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski S, Philippou A (eds) 15th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2009). Lecture notes in computer science, vol 5505. Springer, York, pp 54–57CrossRefGoogle Scholar
  27. Manier MA, Bloch C (2003) A classification for hoist scheduling problems. Int J Flex Manuf Syst 15:37–55CrossRefGoogle Scholar
  28. Maza S, Castagna P (2005) A performance-based structural policy for conflict-free routing of bi-directional automated guided vehicles. Comput Ind 56(7). doi: 10.1016/j.compind.2005.03.003
  29. Merlin PM (1974) A study of the recoverability of computing systems. PhD thesis, Dep. of Information and Computer Science, Univ. of California, Irvine, CAGoogle Scholar
  30. Nemhauser GL, Wolsey LA (1988) Integer and combinatorial optimization. Wiley-Interscience, New YorkMATHGoogle Scholar
  31. Park J, Reveliotis SA, Bodner DA, McGinnis LF (2002) A distributed, event-driven control architecture for flexibly automated manufacturing systems. Int J Comput Integr Manuf 15:109–126CrossRefGoogle Scholar
  32. Schrijver A (1986) Theory of linear and integer programming. Wiley, New YorkMATHGoogle Scholar
  33. Spacek P, Manier M, Moudni A (1999) Control of an electroplating line in the max and min algebras. Int J Syst Sci 30(7):759–778MATHCrossRefGoogle Scholar
  34. Traonouez LM, Lime D, Roux OH (2009) Parametric model-checking of stopwatch Petri nets. J Univers Comput Sci 15(17):3273–3304MathSciNetMATHGoogle Scholar
  35. Virbitskaite I, Pokozy E (1999) Parametric behaviour analysis for Time Petri nets. In: PaCT’99. Springer, London, pp 134–140Google Scholar
  36. Wang F (1996) Parametric timing analysis for real-time systems. Inf Comput 130(2):131–150. doi: 10.1006/inco.1996.0086 MATHCrossRefGoogle Scholar
  37. Wu N, Chu C, Chu F, Zhou M (2008) A Petri net method for schedulability and scheduling problems in single-arm cluster tools with wafer residency time constraints. IEEE Trans Semicond Manuf 21(2):224–237CrossRefGoogle Scholar
  38. Wu N, Chu F, Chu C, Zhou M (2011) Petri net-based scheduling of single-arm cluster tools with reentrant atomic layer deposition processes. IEEE Trans Autom Sci Eng 8(1):42–55. doi: 10.1109/TASE.2010.2046736 CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2013

Authors and Affiliations

  • Didier Lime
    • 1
  • Claude Martinez
    • 2
  • Olivier H. Roux
    • 1
  1. 1.IRCCyN UMR CNRS 6597, LUNAM UniversitéÉcole Centrale de NantesNantes cedex 3France
  2. 2.IRCCyN UMR CNRS 6597, LUNAM UniversitéUniversité de NantesNantes cedex 3France

Personalised recommendations