Round-Bounded Control of Parameterized Systems

  • Benedikt BolligEmail author
  • Mathieu Lehaut
  • Nathalie Sznajder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)


We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.


  1. 1.
    Abdulla, P.A., Bouajjani, A., d’Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1–14. Springer, Heidelberg (2003). Scholar
  2. 2.
    Abdulla, P.A., Delzanno, G.: Parameterized verification. Int. J. Softw. Tools Technol. Transf. 18(5), 469–473 (2016)CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 106–120. Springer, Heidelberg (2013). Scholar
  4. 4.
    Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262–281. Springer, Heidelberg (2014). Scholar
  5. 5.
    Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Parity games on bounded phase multi-pushdown systems. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 272–287. Springer, Cham (2017). Scholar
  6. 6.
    Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4) (2011)Google Scholar
  7. 7.
    Bérard, B., Haddad, S., Sassolas, M., Sznajder, N.: Concurrent games on VASS with inhibition. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 39–52. Springer, Heidelberg (2012). Scholar
  8. 8.
    Björklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4–5), 702–715 (2010)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27 (2011)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Brázdil, T., Jančar, P., Kučera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478–489. Springer, Heidelberg (2010). Scholar
  11. 11.
    Brütsch, B., Thomas, W.: Playing games in the Baire space. In: Proceedings Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd International Workshop on Synthesis of Complex Parameters, Volume 220 of EPTCS, pp. 13–25 (2016)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 220–231. Springer, Heidelberg (2014). Scholar
  13. 13.
    Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of FOCS 1991, pp. 368–377. IEEE Computer Society (1991)Google Scholar
  14. 14.
    Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification. In: STACS 2014, Volume 25 of Leibniz International Proceedings in Informatics, pp. 1–10. Leibniz-Zentrum für Informatik (2014)Google Scholar
  16. 16.
    Figueira, D., Praveen, M.: Playing with repetitions in data words using energy games. In: Proceedings of LICS 2018, pp. 404–413. ACM (2018)Google Scholar
  17. 17.
    Hopcroft, J.E., Motwani, R., Rotwani, Ullman, J.D.: Introduction to Automata Theory, Languages and Computability, 2nd edn. Addison-Wesley Longman Publishing Company Inc., (2000)Google Scholar
  18. 18.
    Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014)Google Scholar
  19. 19.
    Jančar, P.: On reachability-related games on vector addition systems with states. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 50–62. Springer, Cham (2015). Scholar
  20. 20.
    Kara, A.: Logics on data words: expressivity, satisfiability, model checking. Ph.D. thesis, Technical University of Dortmund (2016)Google Scholar
  21. 21.
    Kozen, D.: Lower bounds for natural proof systems. In: Proceedings of SFCS 1977, pp. 254–266. IEEE Computer Society (1977)Google Scholar
  22. 22.
    La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007, pp. 161–170. IEEE Computer Society Press (2007)Google Scholar
  23. 23.
    La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299–314. Springer, Heidelberg (2008). Scholar
  24. 24.
    La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 629–644. Springer, Heidelberg (2010). Scholar
  25. 25.
    La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. Technical Report 2142/15410, University of Illinois (2010). Available at
  26. 26.
    Lange, M., Stirling, C.: Model checking games for branching time logics. J. Log. Comput. 12(4), 623–639 (2002)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). Scholar
  28. 28.
    Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)CrossRefGoogle Scholar
  29. 29.
    Seth, A.: Games on multi-stack pushdown systems. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 395–408. Springer, Heidelberg (2008). Scholar
  30. 30.
    Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, MIT (1974)Google Scholar
  31. 31.
    Thomas, Wolfgang: Languages, automata, and logic. In: Rozenberg, Grzegorz, Salomaa, Arto (eds.) Handbook of Formal Languages, pp. 389–455. Springer, Heidelberg (1997). Scholar
  32. 32.
    Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Benedikt Bollig
    • 1
    Email author
  • Mathieu Lehaut
    • 2
  • Nathalie Sznajder
    • 2
  1. 1.CNRS, LSV & ENS Paris-SaclayUniversité Paris-SaclayCachanFrance
  2. 2.Sorbonne Université, CNRS, LIP6ParisFrance

Personalised recommendations