Abstract
Reactive and hybrid systems are modeled by games where players make strategic decisions in a temporally discrete manner. The dynamics of players use dense or discrete time. In order to guarantee invariance and inevitability properties, the proponent moves are restricted by “winning guards”. The winning strategy determined by these guards does not exclude any initial state from which a winning strategy exists. Sets of such initial states constitute winning regions and are defined by fixed points. The iterates which yield winning regions are structured as unions of iterates which yield winning guards.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R.: The B-Book. Camdridge Univ. Press, Cambridge (1996)
Agrachev, A.A., Sachkov, Y.L.: Control Theory from the Geometric Viewpoint, Trieste. Lecture Notes, Intern. School Advanced Studies (2002)
Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Proc. 2nd Workshop Hybrid Systems. LNCS, vol. 999, pp. 1–20. Springer, Berlin (1995)
Asarin, E., Bournez, O., Dang, T., Maler, O., Pnueli, A.: Effective synthesis of switching controllers for linear systems. Proc. IEEE 88(7), 1011–1025 (2000)
Aubin, J.-P.: Viability Theory, Birkhaüser, Boston (1991)
Bardi, M., Capuzzo-Dolcetta, I.: Optimal Control and Viscosity Solutions of Hamilton-Jacobi-Bellman Equations, Birkhaüser, Boston (1997)
Bas̨ar, T., Olsder, G.J.: Dynamic Noncooperative Game Theory, Soc. Industr. and Appl. Math., Philadelphia (1998)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Berlin (1998)
Bayen, A.M., Crück, E., Tomlin, C.J.: Guaranteed overapproximations of unsafe sets for continuous and hybrid systems: solving the Hamilton-Jacobi equation using viability techniques. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 90–104. Springer, Heidelberg (2002)
Berstekas, D.P.: Dynamic Programming and Optimal Control. 2nd ed., Vol. I, 2000, and Vol. II, 2001. Athena Scientific, Belmont
Barbeau, M., Kabanza, F., St-Denis, R.: A method for the synthesis of controllers to handle safety, liveness, and real-time constraints. IEEE Trans. Automatic Control 43(11), 1543–1559 (1998)
Broy, M.: Abstractions from time. In: McIver, A., Morgan, C. (eds.) Programming Methodology, pp. 95–107. Springer, Berlin (2003)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions for finite-state operators. Trans. AMS 138, 259–311 (1969)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 25th Symp. Principles Programming Lang., pp. 12–25. ACM, New-York (2000)
Cousot, P.: Méthodes Itératives de Construction et d’Approximation de Points Fixes d’Opérateurs Monotones sur un Treillis, Analyse Sémantique des Programmes, Thèse de Doctorat Sci. Math., Univ. Sci. et Médicale de Grenoble (1978)
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)
Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proc. IEEE 88(7), 985–1010 (2000)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Harel, D.: And/or programs: a new approach to structured programming. ACM TOPLAS 2(1), 1–17 (1980)
Henzinger, T.A., Majumdar, R., Mang, F., Raskin, J.-F.: Abstract interpretation of game properties. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 220–239. Springer, Heidelberg (2000)
Heymann, M., Lin, F., Meyer, G.: Control of rate-bounded hybrid systems with liveness constraints. In: Colonius, F., et al. (eds.) Advances in Mathematical Systems Theory, pp. 151–168. Birkhaüser, Boston (2001)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Isaacs, R.: Differential Games. Wiley, New-York (1965); Republished: Dover, New-York (1999)
Lamport, L.: The temporal logic of actions. ACM Trans. Programming Languages and Systems 16(3), 872–923 (1994)
Lewin, J.: Differential Games. Springer, London (1994)
Lygeros, J., Johansson, K.H., Simić, S.N., Zhang, J., Sastry, S.S.: Dynamical properties of hybrid automata. IEEE Trans. Automatic Control 48(1), 2–18 (2003)
Moszkowski, B.: Compositional reasoning using interval temporal logic and Tempura. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 439–464. Springer, Heidelberg (1998)
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)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, London (1998)
Ramadge, P.J., Wonham, W.M.: The control of discrete-event systems. Proc. IEEE 77, 81–98 (1989)
Sintzoff, M.: Abstract verification of structured dynamical systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 126–137. Springer, Heidelberg (1996)
Trakhtenbrot, B.A., Barzdin, Ya.M.: Konechnye Avtomaty (Povedenie i Sintez), Nauka, Moscow (1970); Engl. transl. by D. Louvish, ed. by E. Shamir and L.H. Landweber: Finite Automata: Behaviour and Synthesis, North-Holland, Amsterdam (1973)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Tomlin, C.J., Lygeros, J., Sastry, S.S.: A game-theoretic approach to controller design for hybrid systems. Proc. IEEE 88(7), 949–970 (2000)
van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct concurrent programs. Acta Informatica 12, 1–31 (1979)
Vinter, R.: Optimal Control, Birkhaüser, Boston (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Sintzoff, M. (2004). Iterative Synthesis of Control Guards Ensuring Invariance and Inevitability in Discrete-Decision Games. In: Owe, O., Krogdahl, S., Lyche, T. (eds) From Object-Orientation to Formal Methods. Lecture Notes in Computer Science, vol 2635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39993-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-39993-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21366-6
Online ISBN: 978-3-540-39993-3
eBook Packages: Springer Book Archive