Abstract
In this paper we focus on property-preserving preorders between timed game automata and their application to control of partially observable systems. We define timed weak alternating simulation as a preorder between timed game automata, which preserves controllability. We define the rules of building a symbolic turn-based two-player game such that the existence of a winning strategy is equivalent to the simulation being satisfied. We also propose an on-the-fly algorithm for solving this game. This simulation checking method can be applied to the case of non-alternating or strong simulations as well. We illustrate our algorithm by a case study and report on results.
This work has been supported by the EC FP7 under grant numbers INFSO-ICT-224249 (Multiform www.ict-multiform.eu) and ICT-214755 (Quasimodo www.quasimodo.aau.dk), and the VKR Center of Excellence MT-LAB (www.mtlab.dk).
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
Preview
Unable to display preview. Download preview PDF.
References
Abdeddaïm, Y., Asarin, E., Gallien, M., Ingrand, F., Lessire, C., Sighireanu, M.: Planning Robust Temporal Plans A Comparison Between CBTP and TGA Approaches. In: Proceedings of the International Conference on Automated Planning and Scheduling International Conference on Automated Planning and Scheduling (ICAPS 2007). AAAI Press, Menlo Park (2007)
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: FOCS, pp. 100–109 (1997)
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. In: SIGMETRICS Performance Evaluation Review (2005)
Bengtsson, J.E., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 2004, pp. 87–124. Springer, Heidelberg (2004)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
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)
Cerans, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1993)
Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification – theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993)
Chatain, T., David, A., Larsen, K.G.: Playing games with timed games. Research Report LSV-08-34, Laboratoire Spécification et Vérification, ENS Cachan, France, 15 pages (December 2008)
Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 192–206. Springer, Heidelberg (2007)
de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003)
Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for buchi automata. SIAM Journal on Computing 34, 1159–1175 (2001)
Jensen, H.E., Larsen, K.G., Skou, A.: Scaling up Uppaal automatic verification of real-time systems using compositionality and abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 19–30. Springer, Heidelberg (2000)
Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using uppaal tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 227–240. Springer, Heidelberg (2007)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Journal of Software Tools for Technology Transfer (STTT) 1(1-2), 134–152 (1997)
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)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)
Weise, C., Lenzkes, D.: Efficient scaling-invariant checking of timed bisimulation. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 177–188. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bulychev, P., Chatain, T., David, A., Larsen, K.G. (2009). Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation. In: Ouaknine, J., Vaandrager, F.W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2009. Lecture Notes in Computer Science, vol 5813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04368-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-04368-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04367-3
Online ISBN: 978-3-642-04368-0
eBook Packages: Computer ScienceComputer Science (R0)