Skip to main content

What’s to Come is Still Unsure

Synthesizing Controllers Resilient to Delayed Interaction

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2018)

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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. 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. 3.

    Available at https://www.react.uni-saarland.de/tools/safetysynth/.

  4. 4.

    http://www.syntcomp.org/.

  5. 5.

    http://fmv.jku.at/aiger/.

  6. 6.

    http://www.verilog.com/.

  7. 7.

    http://www.clifford.at/yosys/.

References

  1. Balemi, S.: Communication delays in connections of input/output discrete event processes. CDC 1992, 3374–3379 (1992)

    Google Scholar 

  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_14

    Chapter  Google Scholar 

  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_1

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)

    Article  MathSciNet  Google Scholar 

  7. Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138(1), 295–311 (1969)

    Article  MathSciNet  Google Scholar 

  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. 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

    Google Scholar 

  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_36

    Chapter  Google Scholar 

  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. Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109–127. Springer, Berlin (2000)

    Google Scholar 

  13. McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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/BFb0035790

    Chapter  Google Scholar 

  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. Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)

    Article  MathSciNet  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  20. Tripakis, S.: Decentralized control of discrete-event systems with bounded or unbounded delay communication. IEEE Trans. Autom. Control 49(9), 1489–1501 (2004)

    Article  MathSciNet  Google Scholar 

  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_14

    Chapter  Google Scholar 

  22. Zimmermann, M.: Finite-state strategies in delay games. In: GandALF 2017, Volume 256 of EPTCS, pp. 151–165 (2017)

    Article  MathSciNet  Google Scholar 

Download references

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

Authors

Corresponding author

Correspondence to Mingshuai Chen .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics