Abstract
A controller for a discrete game with ω-regular objectives requires attention if, intuitively, it requires measuring the state and switching from the current control action. Minimum attention controllers are preferable in modern shared implementations of cyber-physical systems because they produce the least burden on system resources such as processor time or communication bandwidth. We give algorithms to compute minimum attention controllers for ω-regular objectives in imperfect information discrete two-player games. We show a polynomial-time reduction from minimum attention controller synthesis to synthesis of controllers for mean-payoff parity objectives in games of incomplete information. This gives an optimal EXPTIME-complete synthesis algorithm. We show that the minimum attention controller problem is decidable for infinite state systems with finite bisimulation quotients. In particular, the problem is decidable for timed and rectangular automata.
This research was funded in part by the US National Science Foundation grants CCF-0546170, CNS-0702881, DARPA grant HR0011-09-1-0037, Austrian Science Fund (FWF) NFN Grant S11407-N23 (RiSE), and a Microsoft faculty fellowship.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–236 (1994)
Anta, A., Tabuada, P.: On the minimum attention and anytime attention problems for nonlinear systems. In: CDC 2010. IEEE, Los Alamitos (2010)
Brockett, R.W.: Minimum attention control. In: CDC 1997. IEEE, Los Alamitos (1997)
Brockett, R.W.: Minimizing attention in a motion control context. In: CDC 2003. IEEE, Los Alamitos (2003)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the AMS 138, 295–311 (1969)
Cassez, F., Tripakis, S.: Fault diagnosis with static and dynamic observers. Fundam. Inform. 88(4), 497–540 (2008)
Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.F.: Algorithms for omega-regular games with imperfect information. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 287–302. Springer, Heidelberg (2006)
Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Mean-payoff parity games. In: LICS 2005, pp. 178–187. IEEE, Los Alamitos (2005)
Chatterjee, K., Majumdar, R., Henzinger, T.A.: Controller synthesis with budget constraints. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 72–86. Springer, Heidelberg (2008)
Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35. Institut Mittag-Leffler (1962)
Degorre, A., Doyen, L., Gentilini, R., Raskin, J.-F., Toruńczyk, S.: Energy and mean-payoff games with imperfect information. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 260–274. Springer, Heidelberg (2010)
Emerson, E.A., Jutla, C.: Tree automata, mu-calculus and determinacy. In: FOCS 1991, pp. 368–377. IEEE, Los Alamitos (1991)
Girard, A.: Synthesis using approximately bisimilar abstractions: state-feedback controllers for safety specifications. In: HSCC, pp. 111–120. ACM, New York (2010)
Girard, A., Julius, A.A., Pappas, G.J.: Approximate simulation relations for hybrid systems. Discrete Event Dynamic Systems 18(2), 163–179 (2008)
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: STOC 1982, pp. 60–65. ACM, New York (1982)
Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theoretical Computer Science 221, 369–392 (1999)
Jobstmann, B.: Applications and Optimizations for LTL Synthesis. PhD thesis, Graz University of Technology (March 2007)
Kechris, A.: Classical Descriptive Set Theory. Springer, Heidelberg (1995)
Kloetzer, M., Belta, C.: A fully automated framework for control of linear systems from temporal logic specifications. IEEE Transactions on Automatic Control 53(1), 287–297 (2008)
Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal logic-based reactive mission and motion planning. IEEE Transactions on Robotics 25(6), 1370–1381 (2009)
Kupferman, O., Vardi, M.Y.: μ-calculus synthesis. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 497–507. Springer, Heidelberg (2000)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete informatio. In: Advances in Temporal Logic, pp. 109–127. Kluwer Academic Publishers, Dordrecht (2000)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS 2005: Foundations of Computer Science, pp. 531–540 (2005)
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)
Martin, D.A.: Borel determinacy. Annals of Mathematics 102(2), 363–371 (1975)
Mazo, M., Davitian, A., Tabuada, P.: Pessoa: A tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 566–569. Springer, Heidelberg (2010)
Montestruque, L., Antsaklis, P.: On the model-based control of networked systems. Automatica 39(10), 1837–1843 (2003)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57 (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989, pp. 179–190. ACM, New York (1989)
Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508–2516 (2008)
Rabin, M.O.: Automata on Infinite Objects and Church’s Problem. Conference Series in Mathematics, vol. 13. American Mathematical Society, Providence (1969)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. IEEE Transactions on Control Theory 77, 81–98 (1989)
Reif, J.H.: The complexity of two-player games of incomplete information. Journal of Computer and System Sciences 29, 274–301 (1984)
Safra, S.: On the complexity of ω-automata. In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science, pp. 319–327. IEEE Computer Society Press, Los Alamitos (1988)
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages. Beyond Words. ch.7, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
Thorsley, D., Teneketzis, D.: Active acquisition of information for diagnosis and supervisory control of discrete event systems. Discrete Event Dynamic Systems 17, 531–583 (2007)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Zwick, U., Paterson, M.S.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158, 343–359 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Majumdar, R. (2011). Minimum Attention Controller Synthesis for Omega-Regular Objectives. In: Fahrenberg, U., Tripakis, S. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2011. Lecture Notes in Computer Science, vol 6919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24310-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-24310-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24309-7
Online ISBN: 978-3-642-24310-3
eBook Packages: Computer ScienceComputer Science (R0)