Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Symbolic unfolding of parametric stopwatch Petri nets

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We address the problem of unfolding safe parametric stopwatch time Petri nets (PSwPNs), i.e., safe time Petri nets (TPNs) possibly extended with time parameters and stopwatches. We extend the notion of branching process to account for the dates of the occurrences of events and thus define a symbolic unfolding for PSwPNs. In the case of TPNs we also propose a method based on our so-called time branching processes to compute a finite complete prefix of the symbolic unfolding. The originality of our work relies on a precise handling of direct conflicts between events, and the analysis of their effects on the constraints between the firing dates of those events.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

References

  1. Abdulla PA, Iyer SP, Nylen A (2000) Unfoldings of unbounded Petri nets. In: Proceedings of CAV. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 495–507

    Google Scholar 

  2. Aura T, Lilius J (2000) A causal semantics for time Petri nets. Theor Comput Sci 243(2):409–447

    Article  MathSciNet  MATH  Google Scholar 

  3. Baldan P, Busi N, Corradini A, Pinna GM (2000) Functorial concurrent semantics for Petri nets with read and inhibitor arcs. In: CONCUR. Lecture notes in computer science, vol 1877. Springer, Berlin, pp 442–457

    Google Scholar 

  4. Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time Petri nets. IEEE Trans Softw Eng 17(3):259–273

    Article  MathSciNet  Google Scholar 

  5. 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 17(2):133–158

    Article  MathSciNet  MATH  Google Scholar 

  6. Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. In: Mason REA (ed) Information processing: proceedings of the IFIP congress 1983. IFIP congress series, vol 9. Elsevier Science, Amsterdam, pp 41–46

    Google Scholar 

  7. Bouyer P, Haddad S, Reynier PA (2006) Timed unfoldings for networks of timed automata. In: Graf S, Zhang W (eds) Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA’06), Beijing, China. Lecture notes in computer science, vol 4218. Springer, Berlin, pp 292–306

    Chapter  Google Scholar 

  8. Cassez F, Chatain T, Jard C (2006) Symbolic unfoldings for networks of timed automata. In: Graf S, Zhang W (eds) Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA’06), Beijing, China. Lecture notes in computer science, vol 4218. Springer, Berlin, pp 307–321

    Chapter  Google Scholar 

  9. Chatain T, Jard C (2006) Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In: Proceedings of ICATPN. Lecture notes in computer science, vol 4024. Springer, Berlin, pp 125–145

    Google Scholar 

  10. Chatain T, Khomenko V (2007) On the well-foundedness of adequate orders used for construction of complete unfolding prefixes. Inf Process Lett 104(4):129–136

    Article  MathSciNet  MATH  Google Scholar 

  11. Dill D (1989) Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of workshop on computer aided verification methods for finite state systems, vol 407, pp 197–212

    Chapter  Google Scholar 

  12. Esparza J (1994) Model checking using net unfoldings. Sci Comput Program 23:151–195

    Article  MathSciNet  MATH  Google Scholar 

  13. Esparza J, Heljanko K (2008) Unfoldings, a partial-order approach to model checking. Monographs in theoretical computer science. Springer, Berlin

    MATH  Google Scholar 

  14. Esparza J, Römer S, Vogler W (2002) An improvement of McMillan’s unfolding algorithm. Form Methods Syst Des 20(3):285–310

    Article  MATH  Google Scholar 

  15. Fabre E, Benveniste A, Haar S, Jard C (2005) Distributed monitoring of concurrent and asynchronous systems. Discrete Event Dyn Syst 15(1):33–84

    Article  MathSciNet  MATH  Google Scholar 

  16. Gardey G, Roux OH, Roux OF (2006) State space computation and analysis of time Petri nets. Theory Pract Log Program 6(3):301–320. Special issue on specification analysis and verification of reactive systems

    Article  MathSciNet  MATH  Google Scholar 

  17. Grabiec B, Traonouez LM, Jard C, Lime D, Roux OH (2010) Diagnosis using unfoldings of parametric time Petri nets. In: Chatterjee K, Henzinger TA (eds) 8th international conference on formal modelling and analysis of timed systems (FORMATS 2010), Vienna, Austria. Lecture notes in computer science, vol 6246. Springer, Berlin, pp 137–151

    Chapter  Google Scholar 

  18. Henzinger T, Kopke P, Puri A, Varaiya P (1998) What’s decidable about hybrid automata? J Comput Syst Sci 57:94–124

    Article  MathSciNet  MATH  Google Scholar 

  19. Khomenko V, Koutny M (2003) Branching processes of high-level Petri nets. In: Proceedings of TACAS. Lecture notes in computer science, vol 2619. Springer, Berlin, pp 458–472

    Google Scholar 

  20. Lime D, Roux OH (2004) A translation-based method for the timed analysis of scheduling extended time Petri nets. In: 25th IEEE real-time systems symposium (RTSS 2004), Lisbon, Portugal. IEEE Computer Society Press, Los Alamitos, pp 187–196

    Chapter  Google Scholar 

  21. Lime D, Roux OH (2006) Model checking of time Petri nets using the state class timed automaton. Discrete Event Dyn Syst 16(2):179–205

    Article  MathSciNet  MATH  Google Scholar 

  22. Lime D, Roux OH (2009) Formal verification of real-time systems with preemptive scheduling. Real-Time Syst 41(2):118–151

    Article  MATH  Google Scholar 

  23. 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), York, United Kingdom. Lecture notes in computer science, vol 5505. Springer, Berlin, pp 54–57

    Chapter  Google Scholar 

  24. Margaria T, Steffen B (eds) (1996) An improvement of McMillan’s unfolding algorithm, Passau, Germany. Lecture notes in computer science, vol 1055. Springer, Berlin

    Google Scholar 

  25. McMillan KL (1992) Using unfolding to avoid the state space explosion problem in the verification of asynchronous circuits. In: Proceedings of computer aided verification (CAV’92). Lecture notes in computer science, vol 663. Springer, Berlin, pp 164–177

    Chapter  Google Scholar 

  26. Merlin PM (1974) A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California, Irvine, CA

  27. Traonouez LM, Grabiec B, Jard C, Lime D, Roux OH (2010) Symbolic unfolding of parametric stopwatch Petri nets. In: Bouajjani A, Chin WN (eds) 8th international symposium on automated technology for verification and analysis (ATVA 2010), Singapore. Lecture notes in computer science, vol 6252. Springer, Berlin, pp 291–305

    Chapter  Google Scholar 

  28. Traonouez LM, Lime D, Roux OH (2009) Parametric model-checking of stopwatch Petri nets. J Univers Comput Sci 15(17):3273–3304

    MathSciNet  MATH  Google Scholar 

  29. Vogler W, Semenov AL, Yakovlev A (1998) Unfolding and finite prefix for nets with read arcs. In: Sangiorgi D, de Simone R (eds) 9th international conference on concurrency theory (CONCUR’98), Nice, France. Lecture notes in computer science, vol 1466. Springer, Berlin, pp 501–516

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Nantes, LINA CNRS UMR 6241, Nantes, France

    Claude Jard

  2. École Centrale de Nantes, IRCCyN CNRS UMR 6597, Nantes, France

    Didier Lime & Olivier H. Roux

  3. INRIA, IRISA CNRS UMR 6074, Rennes, France

    Louis-Marie Traonouez

Authors
  1. Claude Jard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Didier Lime
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Olivier H. Roux
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Louis-Marie Traonouez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Didier Lime.

Additional information

This work has been partially funded by ANR project ImpRo (ANR-2010-BLAN-0317).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jard, C., Lime, D., Roux, O.H. et al. Symbolic unfolding of parametric stopwatch Petri nets. Form Methods Syst Des 43, 493–519 (2013). https://doi.org/10.1007/s10703-013-0188-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-013-0188-2

Keywords

Search

Navigation