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.
William Shakespeare, Twelfth Night/What You Will, Act 2, Scene 3.
The first and fifth authors are funded partly by NSFC under grant No. 61625206 and 61732001, by “973 Program" under grant No. 2014CB340701, and by the CAS/SAFEA International Partnership Program for Creative Research Teams. The second and fourth authors are supported by DFG under grant No. DFG RTG 1765 SCARE. The third author is funded by NSFC under grant No. 61502467 and by the US AFOSR via AOARD grant No. FA2386-17-1-4022.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 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.
- 3.
Available at https://www.react.uni-saarland.de/tools/safetysynth/.
- 4.
- 5.
- 6.
- 7.
References
Balemi, S.: Communication delays in connections of input/output discrete event processes. CDC 1992, 3374–3379 (1992)
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_14
Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1–20. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54013-4_1
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)
Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: Compositional algorithms for succinct safety games. SYNT 2015, 98–111 (2015)
Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138(1), 295–311 (1969)
Chen, M., Fränzle, M., Li, Y., Mosaad, P.N., Zhan, N.: What’s to come is still unsure: synthesizing controllers resilient to delayed interaction (full version). [Online]. http://lcs.ios.ac.cn/~chenms/papers/ATVA2018_FULL.pdf
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
Klein, F., Zimmermann, M.: How much lookahead is needed to win infinite games? In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 452–463. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_36
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)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109–127. Springer, Berlin (2000)
McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)
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)
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0035790
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)
Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)
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)
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). https://doi.org/10.1007/3-540-59042-0_57
Tripakis, S.: Decentralized control of discrete-event systems with bounded or unbounded delay communication. IEEE Trans. Autom. Control 49(9), 1489–1501 (2004)
De Wulf, M., Doyen, L., Raskin, J.-F.: A lattice theory for solving games of imperfect information. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 153–168. Springer, Heidelberg (2006). https://doi.org/10.1007/11730637_14
Zimmermann, M.: Finite-state strategies in delay games. In: GandALF 2017, Volume 256 of EPTCS, pp. 151–165 (2017)
Acknowledgements
The authors would like to thank Bernd Finkbeiner and Ralf Wimmer for insightful discussions on the AIGER format for synthesis and Leander Tentrup for extending his tool SafetySynth by state initialization, thus facilitating a comparison.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Chen, M., Fränzle, M., Li, Y., Mosaad, P.N., Zhan, N. (2018). What’s to Come is Still Unsure. In: Lahiri, S., Wang, C. (eds) Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science(), vol 11138. Springer, Cham. https://doi.org/10.1007/978-3-030-01090-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-01090-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-01089-8
Online ISBN: 978-3-030-01090-4
eBook Packages: Computer ScienceComputer Science (R0)