Advertisement

What’s to Come is Still Unsure

Synthesizing Controllers Resilient to Delayed Interaction
  • Mingshuai ChenEmail author
  • Martin Fränzle
  • Yangjia Li
  • Peter N. Mosaad
  • Naijun Zhan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

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.

Keywords

Safety games Control under delay Efficient algorithmic synthesis 

Notes

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.

References

  1. 1.
    Balemi, S.: Communication delays in connections of input/output discrete event processes. CDC 1992, 3374–3379 (1992)Google Scholar
  2. 2.
    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_14CrossRefGoogle Scholar
  3. 3.
    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_1CrossRefGoogle Scholar
  4. 4.
    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)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: Compositional algorithms for succinct safety games. SYNT 2015, 98–111 (2015)Google Scholar
  6. 6.
    Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138(1), 295–311 (1969)MathSciNetCrossRefGoogle Scholar
  8. 8.
    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
  9. 9.
    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, 1953Google Scholar
  10. 10.
    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_36CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109–127. Springer, Berlin (2000)Google Scholar
  13. 13.
    McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)MathSciNetCrossRefGoogle Scholar
  14. 14.
    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)MathSciNetCrossRefGoogle Scholar
  15. 15.
    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/BFb0035790CrossRefGoogle Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)MathSciNetCrossRefGoogle Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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_57CrossRefGoogle Scholar
  20. 20.
    Tripakis, S.: Decentralized control of discrete-event systems with bounded or unbounded delay communication. IEEE Trans. Autom. Control 49(9), 1489–1501 (2004)MathSciNetCrossRefGoogle Scholar
  21. 21.
    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_14CrossRefGoogle Scholar
  22. 22.
    Zimmermann, M.: Finite-state strategies in delay games. In: GandALF 2017, Volume 256 of EPTCS, pp. 151–165 (2017)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.State Key Lab. of Computer Science, Institute of SoftwareCAS, University of Chinese Academy of SciencesBeijingChina
  2. 2.Department of Computing ScienceCarl von Ossietzky Universität OldenburgOldenburgGermany
  3. 3.University of TartuTartuEstonia

Personalised recommendations