Advertisement

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)

Abstract

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.

References

  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).  https://doi.org/10.1007/978-3-540-45220-1_1Google 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).  https://doi.org/10.1007/978-3-642-40184-8_9CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-54013-4_15CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-59647-1_21CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-32940-1_5CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-14162-1_40CrossRefGoogle 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).  https://doi.org/10.1007/978-3-662-44522-8_19CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-24537-9_6CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-540-78800-3_21CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-14295-6_54CrossRefGoogle 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 http://hdl.handle.net/2142/15410
  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).  https://doi.org/10.1007/978-3-540-31980-1_7CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-540-92687-0_27CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-59126-6_7CrossRefGoogle 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