Robust reachability in timed automata and games: a game-based approach. (English) Zbl 1302.68153
Summary: Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing “robust” strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.
MSC:
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 91A80 | Applications of game theory |
References:
| [1] | Abdeddaïm, Yasmina; Asarin, Eugene; Maler, Oded, Scheduling with timed automata, Theoret. Comput. Sci., 354, 2, 272-300 (2006) · Zbl 1088.68023 |
| [2] | Abdulla, Parosh Aziz; Krčál, Pavel; Yi, Wang, Sampled universality of timed automata, (Proc. 10th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’07). Proc. 10th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’07), LNCS, vol. 4423 (2007), Springer), 2-16 · Zbl 1195.68052 |
| [3] | Abdulla, Parosh Aziz; Krčál, Pavel; Yi, Wang, Sampled semantics of timed automata, Log. Methods Comput. Sci., 6, 3, 14 (2010) · Zbl 1214.68195 |
| [4] | Alur, Rajeev; Dill, David L., A theory of timed automata, Theoret. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071 |
| [5] | Alur, Rajeev; Henzinger, Thomas A.; Vardi, Moshe Y., Parametric real-time reasoning, (Proc. 25th Annual ACM Symposium on Theory of Computing (STOC’93) (1993), ACM), 592-601 · Zbl 1310.68139 |
| [6] | Asarin, Eugene; Maler, Oded; Pnueli, Amir; Sifakis, Joseph, Controller synthesis for timed automata, (Proc. IFAC Symposium on System Structure and Control (1998), Elsevier Science), 469-474 |
| [7] | Bengtsson, Johan; Yi, Wang, Timed automata: semantics, algorithms and tools, (Proc. 4th Advanced Course on Petri Nets (ACPN’03). Proc. 4th Advanced Course on Petri Nets (ACPN’03), LNCS, vol. 3098 (2004), Springer), 87-124 · Zbl 1088.68119 |
| [8] | Bouyer, Patricia; Markey, Nicolas; Reynier, Pierre-Alain, Robust model-checking of timed automata, (Proc. 7th Latin American Symposium on Theoretical Informatics (LATIN’06). Proc. 7th Latin American Symposium on Theoretical Informatics (LATIN’06), LNCS, vol. 3887 (2006), Springer), 238-249 · Zbl 1145.68464 |
| [9] | Bouyer, Patricia; Markey, Nicolas; Reynier, Pierre-Alain, Robust analysis of timed automata via channel machines, (Proc. 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’08). Proc. 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’08), LNCS, vol. 4962 (2008), Springer), 157-171 · Zbl 1138.68431 |
| [10] | Bouyer, Patricia; Larsen, Kim G.; Markey, Nicolas; Sankur, Ocan; Thrane, Claus, Timed automata can always be made implementable, (Proc. 22nd International Conference on Concurrency Theory (CONCUR’11). Proc. 22nd International Conference on Concurrency Theory (CONCUR’11), LNCS, vol. 6901 (2011), Springer), 76-91 · Zbl 1343.68134 |
| [11] | Bouyer, Patricia; Markey, Nicolas; Sankur, Ocan, Robust model-checking of timed automata via pumping in channel machines, (Proc. 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11). Proc. 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11), LNCS, vol. 6919 (2011), Springer), 97-112 · Zbl 1348.68122 |
| [12] | Bouyer, Patricia; Markey, Nicolas; Sankur, Ocan, Robust reachability in timed automata: a game-based approach, (Proc. 39th International Colloquium on Automata, Languages and Programming (ICALP’12). Proc. 39th International Colloquium on Automata, Languages and Programming (ICALP’12), LNCS, vol. 7392 (2012), Springer), 128-140 · Zbl 1367.68161 |
| [13] | Cassez, Franck; Henzinger, Thomas A.; Raskin, Jean-François, A comparison of control problems for timed and hybrid systems, (Proc. 5th International Workshop on Hybrid Systems: Computation and Control (HSCC’02). Proc. 5th International Workshop on Hybrid Systems: Computation and Control (HSCC’02), LNCS, vol. 2289 (2002), Springer), 134-148 · Zbl 1044.93518 |
| [14] | Cassez, Franck; David, Alexandre; Fleury, Emmanuel; Larsen, Kim G.; Lime, Didier, Efficient on-the-fly algorithms for the analysis of timed games, (Proc. 16th International Conference on Concurrency Theory (CONCUR’05). Proc. 16th International Conference on Concurrency Theory (CONCUR’05), LNCS, vol. 3653 (2005), Springer), 66-80 · Zbl 1134.68382 |
| [15] | Chatterjee, Krishnendu; Henzinger, Thomas A.; Prabhu, Vinayak S., Timed parity games: complexity and robustness, Log. Methods Comput. Sci., 7, 4, 8 (2010) · Zbl 1237.68112 |
| [16] | Daws, Conrado; Kordy, Piotr, Symbolic robustness analysis of timed automata, (Proc. 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’06). Proc. 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’06), LNCS, vol. 4202 (2006)), 143-155 · Zbl 1141.68429 |
| [17] | De Wulf, Martin; Doyen, Laurent; Raskin, Jean-François, Almost ASAP semantics: from timed models to timed implementations, Form. Aspects Comput., 17, 3, 319-341 (2005) · Zbl 1101.68670 |
| [18] | De Wulf, Martin; Doyen, Laurent; Markey, Nicolas; Raskin, Jean-François, Robust safety of timed automata, Form. Methods Syst. Des., 33, 1-3, 45-84 (2008) · Zbl 1165.68392 |
| [19] | Fränzle, Martin, Analysis of hybrid systems: an ounce of realism can save an infinity of states, (Proc. 13th International Workshop on Computer Science Logic (CSL’99). Proc. 13th International Workshop on Computer Science Logic (CSL’99), LNCS, vol. 1683 (1999), Springer), 126-139 · Zbl 0944.68119 |
| [20] | Graham, Ronald L., Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math., 17, 2, 416-429 (1969) · Zbl 0188.23101 |
| [21] | Gupta, Vineet; Henzinger, Thomas A.; Jagadeesan, Radha, Robust timed automata, (Proc. International Workshop on Hybrid and Real-Time Systems (HART’97). Proc. International Workshop on Hybrid and Real-Time Systems (HART’97), LNCS, vol. 1201 (1997), Springer), 331-345 |
| [22] | Henzinger, Thomas A.; Raskin, Jean-François, Robust undecidability of timed and hybrid systems, (Proc. 3rd International Workshop on Hybrid Systems: Computation and Control (HSCC’00). Proc. 3rd International Workshop on Hybrid Systems: Computation and Control (HSCC’00), LNCS, vol. 1790 (2000), Springer), 145-159 · Zbl 0944.93018 |
| [23] | Henzinger, Thomas A.; Sifakis, Joseph, The embedded systems design challenge, (Proc. 14th International Symposium on Formal Methods (FM’06). Proc. 14th International Symposium on Formal Methods (FM’06), LNCS, vol. 4085 (2006), Springer), 1-15 |
| [24] | Herbreteau, Frédéric; Kini, Dileep; Srivathsan, B.; Walukiewicz, Igor, Using non-convex approximations for efficient analysis of timed automata, (Proc. 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’11). Proc. 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’11), LIPIcs, vol. 13 (2011), Leibniz-Zentrum für Informatik), 78-89 · Zbl 1246.68145 |
| [25] | Hune, Thomas; Romijn, Judi; Stoelinga, Mariëlle; Vaandrager Frits, W., Linear parametric model-checking of timed automata, (Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01). Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), LNCS, vol. 2031 (2001), Springer), 189-203 · Zbl 0978.68094 |
| [26] | Jaubert, Rémi; Reynier, Pierre-Alain, Quantitative robustness analysis of flat timed automata, (Proc. 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’11). Proc. 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’11), LNCS, vol. 6604 (2011), Springer), 229-244 · Zbl 1326.68185 |
| [27] | Jovanovic, Aleksandra; Faucou, Sébastien; Lime, Didier; Roux, Olivier Henri, Real-time control with parametric timed reachability games, (11th International Workshop on Discrete Event Systems (WODES’12) (2012)), 323-330 |
| [28] | Kopetz, Hermann, Real-Time Systems: Design Principles for Distributed Embedded Applications (2011), Springer · Zbl 1226.68001 |
| [29] | Larsen, Kim G.; Pettersson, Paul; Yi, Wang, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf., 1, 1-2, 134-152 (1997) · Zbl 1060.68577 |
| [30] | Larsen, Kim G.; Legay, Axel; Traonouez, Louis-Marie; Wasowski, Andrzej, Robust specification of real time components, (Proc. 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11). Proc. 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11), LNCS, vol. 6919 (2011), Springer), 129-144 · Zbl 1348.68143 |
| [31] | Markey, Nicolas, Robustness in real-time systems, (Proc. 6th IEEE International Symposium on Industrial Embedded Systems (SIES’11) (2011), IEEE Computer Society Press), 28-34 |
| [32] | Puri, Anuj, Dynamical properties of timed automata, Discrete Event Dyn. Syst., 10, 1-2, 87-113 (2000) · Zbl 0986.93042 |
| [33] | Reineke, Jan; Wachter, Björn; Thesing, Stephan; Wilhelm, Reinhard; Polian, Ilia; Eisinger, Jochen; Becker, Bernd, A definition and classification of timing anomalies, (Proc. 6th International Workshop on Worst-Case Execution Time Analysis (WCET’06) (2006)) |
| [34] | Sankur, Ocan, Untimed language preservation in timed systems, (Proc. 36th International Symposium on Mathematical Foundations of Computer Science (MFCS’11). Proc. 36th International Symposium on Mathematical Foundations of Computer Science (MFCS’11), LNCS, vol. 6907 (2011), Springer), 556-567 · Zbl 1343.68148 |
| [35] | Sankur, Ocan, Shrinktech: a tool for the robustness analysis of timed automata, (Proc. 25th International Conference on Computer Aided Verification (CAV’13). Proc. 25th International Conference on Computer Aided Verification (CAV’13), LNCS, vol. 8044 (2013), Springer), 1006-1012 |
| [36] | Sankur, Ocan; Bouyer, Patricia; Markey, Nicolas, Shrinking timed automata, (Proc. 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’11). Proc. 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’11), LIPIcs, vol. 13 (2011), Leibniz-Zentrum für Informatik), 375-386 · Zbl 1246.68159 |
| [37] | Sankur, Ocan; Bouyer, Patricia; Markey, Nicolas; Reynier, Pierre-Alain, Robust controller synthesis in timed automata, (Proc. 24th International Conference on Concurrency Theory (CONCUR’13). Proc. 24th International Conference on Concurrency Theory (CONCUR’13), LNCS, vol. 8052 (2013), Springer), 546-560 · Zbl 1390.68416 |
| [38] | Yovine, Sergio, Kronos: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf., 1, 1-2, 123-133 (1997) · Zbl 1060.68606 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
