Probabilistic Robust Timed Games

  • Youssouf Oualhadj
  • Pierre-Alain Reynier
  • Ocan Sankur
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Solving games played on timed automata is a well-known problem and has led to tools and industrial case studies. In these games, the first player (Controller) chooses delays and actions and the second player (Perturbator) resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. These notions of robustness guarantee the implementability of synthesized controllers. We provide characterizations of the resulting games for Büchi conditions, and prove the EXPTIME-completeness of the corresponding decision problems.


Markov Decision Process Winning Strategy Stochastic Environment Controller Synthesis Industrial Case Study 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: SSC 1998, pp. 469–474. Elsevier Science (1998)Google Scholar
  3. 3.
    Basset, N., Asarin, E.: Thin and thick timed regular languages. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 113–128. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Beauquier, D.: On probabilistic timed automata. Theor. Comput. Sci. 292(1), 65–84 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)Google Scholar
  6. 6.
    Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: WCC 1983, pp. 41–46. North-Holland/IFIP (September 1983)Google Scholar
  7. 7.
    Bouyer, P., Markey, N., Reynier, P.-A.: Robust analysis of timed automata via channel machines. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 157–171. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  8. 8.
    Bouyer, P., Markey, N., Sankur, O.: Robust reachability in timed automata: A game-based approach. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 128–140. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 9.
    Bouyer, P., Markey, N., Sankur, O.: Robustness in timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 1–18. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Chatterjee, K., Henzinger, T.A., Prabhu, V.S.: Timed parity games: Complexity and robustness. Logical Methods in Computer Science 7(4) (2011)Google Scholar
  12. 12.
    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)CrossRefzbMATHGoogle Scholar
  13. 13.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) AVMFSS 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)Google Scholar
  14. 14.
    Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 122–136. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1–15. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Jensen, H.E.: Model checking probabilistic real time systems. In: Proc. 7th Nordic Workshop on Programming Theory, pp. 247–261. Citeseer (1996)Google Scholar
  17. 17.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  18. 18.
    Oualhadj, Y., Reynier, P.-A., Sankur, O.: Probabilistic Robust Timed Games. Technical report (June 2014),
  19. 19.
    Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Putterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, New York (1994)CrossRefGoogle Scholar
  21. 21.
    Sankur, O., Bouyer, P., Markey, N.: Shrinking timed automata. In: FSTTCS 2011. LIPIcs, vol. 13, pp. 375–386. Leibniz-Zentrum für Informatik (2011)Google Scholar
  22. 22.
    Sankur, O., Bouyer, P., Markey, N., Reynier, P.-A.: Robust controller synthesis in timed automata. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 546–560. Springer, Heidelberg (2013)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Youssouf Oualhadj
    • 1
  • Pierre-Alain Reynier
    • 2
  • Ocan Sankur
    • 3
  1. 1.Université de Mons (UMONS)Belgium
  2. 2.LIF, Université d’Aix-Marseille and CNRSFrance
  3. 3.Université Libre de BruxellesBelgium

Personalised recommendations