Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

akshay:hal-00879818

S. Akshay, L. Hélouet, C. Jard, D. Lime, O-H. Roux. Robustness of Time Petri Nets under architectural constraints. In Formal Modeling and Analysis of Timed Systems, Marcin Jurdzinski, Dejan Nickovic (eds.), LNCS, Volume 7595, Pages 11-26, Warwik, United Kingdom, September 2013.

Download [help]

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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, specified 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 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.}

Contact

Loic Hélouet http://people.irisa.fr/Loic.Helouet/

BibTex Reference

@InProceedings{akshay:hal-00879818,
   Author = {Akshay, S. and Hélouet, L. and Jard, C. and Lime, D. and Roux, O-H.},
   Title = {{Robustness of Time Petri Nets under architectural constraints}},
   BookTitle = {{Formal Modeling and Analysis of Timed Systems}},
   editor = {Jurdzinski, Marcin and Nickovic, Dejan},
   Volume = {7595},
   Pages = {11--26},
   Series = {LNCS},
   Publisher = {Springer},
   Address = {Warwik, United Kingdom},
   Month = {September},
   Year = {2013}
}

EndNote Reference [help]

Get EndNote Reference (.ref)