Advertisement

Robustness of Time Petri Nets under Architectural Constraints

  • S. Akshay
  • Loïc Hélouët
  • Claude Jard
  • Didier Lime
  • Olivier H. Roux
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)

Abstract

This paper addresses robustness issues in Time Petri Nets (TPN) under constraints imposed by an external architecture. The main objective is to check whether a timed specification, given as a TPN behaves as expected when subject to additional time and scheduling constraints. These constraints are given by another TPN that constrains the specification via read arcs. Our robustness property says that the constrained net does not exhibit new timed or untimed behaviors. We show that this property is not always guaranteed but that checking for it is always decidable in 1-safe TPNs. We further show that checking if the set of untimed behaviors of the constrained and specification nets are the same is also decidable. Next we turn to the more powerful case of labeled 1-safe TPNs with silent transitions. We show that checking for the robustness property is undecidable even when restricted to 1-safe TPNs with injective labeling, and exhibit a sub-class of 1-safe TPNs (with silent transitions) for which robustness is guaranteed by construction. We demonstrate the practical utility of this sub-class with a case-study and prove that it already lies close to the frontiers of intractability.

Keywords

Supervisory Control Discrete Event System Empty Word Robustness Property Silent Transition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Akshay, S., Hélouët, L., Jard, C., Lime, D., Roux, O.H.: Robustness of time Petri nets under architectural constraints. Technical report (2012), http://people.rennes.inria.fr/Loic.Helouet/Papers/AHJLR12.pdf
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Berard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundam. Inform. 36(2-3), 145–182 (1998)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. Theoretical Computer Science 147(1-2), 117–136 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    Gardey, G., Roux, O.F., Roux, O.H.: Safety control synthesis for time Petri nets. In: 8th International Workshop on Discrete Event Systems (WODES 2006), pp. 222–228. IEEE Computer Society Press, Ann Arbor (2006)CrossRefGoogle Scholar
  8. 8.
    Giua, A., DiCesare, F., Silva, M.: Petri net supervisors for generalized mutual exclusion constraints. In: Proc. 12th IFAC World Congress, Sidney, Australia, pp. 267–270 (July 1993)Google Scholar
  9. 9.
    Holloway, L.E., Krogh, B.H.: Synthesis of feedback control logic for a class of controlled Petri nets. IEEE Trans. on Automatic Control 35(5), 514–523 (1990)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Lime, D., Roux, O.H.: Model checking of time Petri nets using the state class timed automaton. Journal of Discrete Events Dynamic Systems - Theory and Applications (DEDS) 16(2), 179–205 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Maler, O., Pnueli, A., Sifakis, J.: On the Synthesis of Discrete Controllers for Timed Systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  12. 12.
    Ramadge, P., Wonham, W.: The control of discrete event systems. Proceedings of the IEEE; Special issue on Dynamics of Discrete Event Systems 77(1), 81–98 (1989)Google Scholar
  13. 13.
    Uzam, M., Jones, A.H., Yucel, I.: Using a Petri-net-based approach for the real-time supervisory control of an experimental manufacturing system. Journal of Electrical Engineering and Computer Sciences 10(1), 85–110 (2002)Google Scholar
  14. 14.
    Valero, V., Frutos-Escrig, D., Cuartero, F.: On non-decidability of reachability for timed-arc Petri nets. In: Proc. 8th International Workshop on Petri Nets and Performance Models, PNPM 1999 (1999)Google Scholar
  15. 15.
    De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Formal Methods in System Design 33(1-3), 45–84 (2008)zbMATHCrossRefGoogle Scholar
  16. 16.
    Xu, D., He, X.H., Deng, Y.: Compositional schedulability analysis of real-time systems using time Petri nets. IEEE Transactions on Software Engineering 28(10), 984–996 (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • S. Akshay
    • 1
    • 2
  • Loïc Hélouët
    • 1
  • Claude Jard
    • 1
    • 2
  • Didier Lime
    • 3
  • Olivier H. Roux
    • 3
  1. 1.INRIA/IRISARennesFrance
  2. 2.ENS Cachan BretagneRennesFrance
  3. 3.École Centrale de Nantes, IRCCyN (CNRS UMR 6597)LUNAM UniversitéNantesFrance

Personalised recommendations