Skip to main content
Top

2018 | OriginalPaper | Chapter

What’s to Come is Still Unsure

Synthesizing Controllers Resilient to Delayed Interaction

Authors : Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, Naijun Zhan

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing or actuating the environment through physical devices nor data forwarding to and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to \(\omega \)-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm synthesizing a series of controllers handling increasing delays and reducing game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore shed some light on the practically relevant case of non-order-preserving delays, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay pioneered by Klein and Zimmermann.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
While player 1 could enforce a win with probability 1 in a probabilistic setting by just playing a random sequence, she cannot enforce a win in the qualitative setting where player 0 may just be lucky to draw the right guesses throughout.
 
2
Both the prototype implementation and the evaluation examples used in this section can be found at http://​lcs.​ios.​ac.​cn/​~chenms/​tools/​DGame.​tar.​bz2. We opted for an implementation in Mathematica due to its built-in primitives for visualization.
 
Literature
1.
go back to reference Balemi, S.: Communication delays in connections of input/output discrete event processes. CDC 1992, 3374–3379 (1992) Balemi, S.: Communication delays in connections of input/output discrete event processes. CDC 1992, 3374–3379 (1992)
4.
go back to reference Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT 2014, volume 157 of EPTCS, pp. 100–116 (2014)MathSciNetCrossRef Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT 2014, volume 157 of EPTCS, pp. 100–116 (2014)MathSciNetCrossRef
5.
go back to reference Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: Compositional algorithms for succinct safety games. SYNT 2015, 98–111 (2015) Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: Compositional algorithms for succinct safety games. SYNT 2015, 98–111 (2015)
6.
go back to reference Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)MathSciNetCrossRef Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)MathSciNetCrossRef
7.
go back to reference Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138(1), 295–311 (1969)MathSciNetCrossRef Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138(1), 295–311 (1969)MathSciNetCrossRef
9.
go back to reference Gale, D., Stewart, F.M.: Infinite games with perfect information. In: Kuhn, H.W., Tucker, A.W. (eds.) Contributions to the Theory of Games II, Annals of Mathematics Studies 28, pp. 245–266. Princeton University Press, 1953 Gale, D., Stewart, F.M.: Infinite games with perfect information. In: Kuhn, H.W., Tucker, A.W. (eds.) Contributions to the Theory of Games II, Annals of Mathematics Studies 28, pp. 245–266. Princeton University Press, 1953
11.
go back to reference Klein, F., Zimmermann, M.: What are strategies in delay games? Borel determinacy for games with lookahead. In: CSL 2015, volume 41 of Leibniz International Proceedings in Informatics, pp. 519–533 (2015) Klein, F., Zimmermann, M.: What are strategies in delay games? Borel determinacy for games with lookahead. In: CSL 2015, volume 41 of Leibniz International Proceedings in Informatics, pp. 519–533 (2015)
12.
go back to reference Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109–127. Springer, Berlin (2000) Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109–127. Springer, Berlin (2000)
14.
go back to reference Park, S., Cho, K.: Delay-robust supervisory control of discrete-event systems with bounded communication delays. IEEE Trans. Autom. Control 51(5), 911–915 (2006)MathSciNetCrossRef Park, S., Cho, K.: Delay-robust supervisory control of discrete-event systems with bounded communication delays. IEEE Trans. Autom. Control 51(5), 911–915 (2006)MathSciNetCrossRef
16.
go back to reference J. Raskin, K. Chatterjee, L. Doyen, and T. A. Henzinger. Algorithms for omega-regular games with imperfect information. Logical Methods Comput. Sci. 3(3) (2007) J. Raskin, K. Chatterjee, L. Doyen, and T. A. Henzinger. Algorithms for omega-regular games with imperfect information. Logical Methods Comput. Sci. 3(3) (2007)
17.
go back to reference Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)MathSciNetCrossRef Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)MathSciNetCrossRef
18.
go back to reference Somenzi, F.: Binary decision diagrams. In: Calculational System Design, Volume 173 of NATO Science Series F: Computer and Systems Sciences, pp. 303–366. IOS Press (1999) Somenzi, F.: Binary decision diagrams. In: Calculational System Design, Volume 173 of NATO Science Series F: Computer and Systems Sciences, pp. 303–366. IOS Press (1999)
20.
go back to reference Tripakis, S.: Decentralized control of discrete-event systems with bounded or unbounded delay communication. IEEE Trans. Autom. Control 49(9), 1489–1501 (2004)MathSciNetCrossRef Tripakis, S.: Decentralized control of discrete-event systems with bounded or unbounded delay communication. IEEE Trans. Autom. Control 49(9), 1489–1501 (2004)MathSciNetCrossRef
22.
go back to reference Zimmermann, M.: Finite-state strategies in delay games. In: GandALF 2017, Volume 256 of EPTCS, pp. 151–165 (2017)MathSciNetCrossRef Zimmermann, M.: Finite-state strategies in delay games. In: GandALF 2017, Volume 256 of EPTCS, pp. 151–165 (2017)MathSciNetCrossRef
Metadata
Title
What’s to Come is Still Unsure
Authors
Mingshuai Chen
Martin Fränzle
Yangjia Li
Peter N. Mosaad
Naijun Zhan
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_4

Premium Partner