Resilience of Timed Systems

Authors S. Akshay , Blaise Genest , Loïc Hélouët , S. Krishna , Sparsa Roychowdhury



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.33.pdf
  • Filesize: 0.84 MB
  • 22 pages

Document Identifiers

Author Details

S. Akshay
  • IIT Bombay, Mumbai, India
Blaise Genest
  • Univ. Rennes, CNRS, IRISA, Rennes, France
Loïc Hélouët
  • Univ. Rennes, INRIA, IRISA, Rennes, France
S. Krishna
  • IIT Bombay, Mumbai, India
Sparsa Roychowdhury
  • IIT Bombay, Mumbai, India

Cite As Get BibTex

S. Akshay, Blaise Genest, Loïc Hélouët, S. Krishna, and Sparsa Roychowdhury. Resilience of Timed Systems. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 33:1-33:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSTTCS.2021.33

Abstract

This paper addresses reliability of timed systems in the setting of resilience, that considers the behaviors of a system when unspecified timing errors such as missed deadlines occur. Given a fault model that allows transitions to fire later than allowed by their guard, a system is universally resilient (or self-resilient) if after a fault, it always returns to a timed behavior of the non-faulty system. It is existentially resilient if after a fault, there exists a way to return to a timed behavior of the non-faulty system, that is, if there exists a controller which can guide the system back to a normal behavior. We show that universal resilience of timed automata is undecidable, while existential resilience is decidable, in EXPSPACE. To obtain better complexity bounds and decidability of universal resilience, we consider untimed resilience, as well as subclasses of timed automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Timed automata
  • Fault tolerance
  • Integer-resets
  • Resilience

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. S. Akshay, B. Bollig, P. Gastin, M. Mukund, and K. Narayan Kumar. Distributed timed automata with independently evolving clocks. Fundam. Informaticae, 130(4):377-407, 2014. Google Scholar
  2. R. Alur and D.L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. Google Scholar
  3. R. Alur, L. Fix, and T.A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci., 211(1-2):253-273, 1999. Google Scholar
  4. C. Baier, N. Bertrand, P. Bouyer, and T. Brihaye. When are timed automata determinizable? In Proc. of ICALP'09, volume 5556 of LNCS, pages 43-54, 2009. Google Scholar
  5. Roderick Bloem, Peter Gjøl Jensen, Bettina Könighofer, Kim Guldstrand Larsen, Florian Lorber, and Alexander Palmisano. It’s time to play safe: Shield synthesis for timed systems. CoRR, abs/2006.16688, 2020. URL: http://arxiv.org/abs/2006.16688.
  6. P. Bouyer, F. Chevalier, and D. D'Souza. Fault diagnosis using timed automata. In Proc. of FOSSACS 2005, pages 219-233, 2005. Google Scholar
  7. P. Bouyer, N. Markey, and O. Sankur. Robust model-checking of timed automata via pumping in channel machines. In Proc. of FORMATS 2011, volume 6919 of LNCS, pages 97-112, 2011. Google Scholar
  8. P. Bouyer, N. Markey, and O. Sankur. Robustness in timed automata. In International Workshop on Reachability Problems, volume 8169 of LNCS, pages 1-18, 2013. Google Scholar
  9. R. Brenguier, S. Göller, and O. Sankur. A comparison of succinctly represented finite-state systems. In Proc. of CONCUR 2012, volume 7454 of LNCS, pages 147-161. Springer, 2012. Google Scholar
  10. M. De Wulf, L. Doyen, N. Markey, and J-F Raskin. Robust safety of timed automata. Formal Methods Syst. Des., 33(1-3):45-84, 2008. Google Scholar
  11. V. Diekert, P. Gastin, and A. Petit. Removing epsilon-transitions in timed automata. In Proceedings of the 14th Annual Symposium on Theoretical Aspects of Computer Science, STACS '97, pages 583-594, Berlin, Heidelberg, 1997. Springer-Verlag. Google Scholar
  12. Catalin Dima. Dynamical properties of timed automata revisited. In Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, volume 4763 of Lecture Notes in Computer Science, pages 130-146. Springer, 2007. Google Scholar
  13. D. D'Souza, M. Gopinathan, S. Ramesh, and P. Sampath. Conflict-tolerant real-time features. In Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), pages 274-283. IEEE Computer Society, 2008. Google Scholar
  14. Rüdiger Ehlers and Ufuk Topcu. Resilience to intermittent assumption violations in reactive synthesis. In Martin Fränzle and John Lygeros, editors, 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, Berlin, Germany, April 15-17, 2014, pages 203-212. ACM, 2014. Google Scholar
  15. V. Gupta, T.A. Henzinger, and R. Jagadeesan. Robust timed automata. In Proc. Of HART'97, Hybrid and Real-Time Systems, volume 1201 of LNCS, pages 331-345, 1997. Google Scholar
  16. A. Puri. Dynamical properties of timed automata. In DEDS, 10(1-2):87-113, 2000. Google Scholar
  17. Matthieu Renard, Yliès Falcone, Antoine Rollet, Thierry Jéron, and Hervé Marchand. Optimal enforcement of (timed) properties with uncontrollable events. Math. Struct. Comput. Sci., 29(1):169-214, 2019. Google Scholar
  18. P. V. Suman, P.K. Pandya, S.N. Krishna, and L. Manasa. Timed automata with integer resets: Language inclusion and expressiveness. In Proc. of FORMATS'08, volume 5215 of LNCS, pages 78-92, 2008. Google Scholar
  19. M. Swaminathan, M. Fränzle, and J-P. Katoen. The surprising robustness of (closed) timed automata against clock-drift. In Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273 of IFIP, pages 537-553. Springer, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail