Abstract
We consider the synthesis problem on timed automata with Büchi objectives, where delay choices made by a controller are subjected to small perturbations. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we generalize to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes the existing characterization of winning cycles in the absence of punctual guards. We show that the problem remains within \(\textsf{PSPACE}\) despite the presence of punctual guards.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Including self-loops \(v\rightarrow v\) for every vertex v.
- 2.
On automata with 3 clocks, some corner partitions may induce slices described by linear equations of the shape \(x+y-z=w\).
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proceedings of IFAC Symposium on System Structure and Control, pp. 469–474. Elsevier (1998)
Barbot, B., Busatto-Gaston, D., Dima, C., Oualhadj, Y.: Controller synthesis in timed Büchi automata: robustness and punctual guards. CoRR abs/2404.18584 (2024). https://doi.org/10.48550/ARXIV.2404.18584
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). https://doi.org/10.1007/978-3-642-24310-3_9
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). https://doi.org/10.1007/978-3-540-27755-2_3
Busatto-Gaston, D., Monmege, B., Reynier, P.-A., Sankur, O.: Robust controller synthesis in timed Büchi automata: a symbolic approach. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 572–590. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_33
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). https://doi.org/10.1007/11539452_9
Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 331–345. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0014736
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). https://doi.org/10.1007/3-540-59042-0_76
Oualhadj, Y., Reynier, P.-A., Sankur, O.: Probabilistic robust timed games. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 203–217. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_15
Puri, A.: Dynamical properties of timed automata. Discret. Event Dyn. Syst. 10(1–2), 87–113 (2000). https://doi.org/10.1023/A:1008387132377
Rodríguez-Navas, G., Proenza, J.: Using timed automata for modeling distributed systems with clocks: challenges and solutions. IEEE Trans. Softw. Eng. 39(6), 857–868 (2013). https://doi.org/10.1109/TSE.2012.73
Sankur, O.: Robustness in timed automata: analysis, synthesis, implementation. (Robustesse dans les automates temporisés: analyse, synthèse, implémentation). Ph.D. thesis, École normale supérieure de Cachan, Paris, France (2013). https://tel.archives-ouvertes.fr/tel-00910333
Sankur, O., Bouyer, P., Markey, N.: Shrinking timed automata. Inf. Comput. 234, 107–132 (2014). https://doi.org/10.1016/J.IC.2014.01.002
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. LNCS, vol. 8052, pp. 546–560. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40184-8_38
Stainer, A.: Frequencies in forgetful timed automata. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 236–251. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33365-1_17
De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robustness and implementability of timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 118–133. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_10
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Barbot, B., Busatto-Gaston, D., Dima, C., Oualhadj, Y. (2024). Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards. In: Hillston, J., Soudjani, S., Waga, M. (eds) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. QEST+FORMATS 2024. Lecture Notes in Computer Science, vol 14996. Springer, Cham. https://doi.org/10.1007/978-3-031-68416-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-031-68416-6_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-68415-9
Online ISBN: 978-3-031-68416-6
eBook Packages: Computer ScienceComputer Science (R0)