Skip to main content
SpringerLink
Log in

Round-Bounded Control of Parameterized Systems

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

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

Partly supported by ANR FREDDA (ANR-17-CE40-0013).

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

Access this chapter

Log in via an institution
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

References

  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_1

    Google Scholar 

  2. Abdulla, P.A., Delzanno, G.: Parameterized verification. Int. J. Softw. Tools Technol. Transf. 18(5), 469–473 (2016)

    Article  Google Scholar 

  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_9

    Chapter  Google Scholar 

  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_15

    Chapter  MATH  Google Scholar 

  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_21

    Chapter  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  8. Björklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4–5), 702–715 (2010)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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_40

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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_19

    Chapter  Google Scholar 

  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. Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)

    Article  MathSciNet  Google Scholar 

  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. 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. 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. Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014)

    Google Scholar 

  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_6

    Chapter  MATH  Google Scholar 

  20. Kara, A.: Logics on data words: expressivity, satisfiability, model checking. Ph.D. thesis, Technical University of Dortmund (2016)

    Google Scholar 

  21. Kozen, D.: Lower bounds for natural proof systems. In: Proceedings of SFCS 1977, pp. 254–266. IEEE Computer Society (1977)

    Google Scholar 

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

    Chapter  MATH  Google Scholar 

  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_54

    Chapter  Google Scholar 

  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. Lange, M., Stirling, C.: Model checking games for branching time logics. J. Log. Comput. 12(4), 623–639 (2002)

    Article  MathSciNet  Google Scholar 

  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_7

    Chapter  MATH  Google Scholar 

  28. Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)

    Article  Google Scholar 

  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_27

    Chapter  Google Scholar 

  30. Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, MIT (1974)

    Google Scholar 

  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_7

    Chapter  Google Scholar 

  32. Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001)

    Article  MathSciNet  Google Scholar 

  33. Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, LSV & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France

    Benedikt Bollig

  2. Sorbonne Université, CNRS, LIP6, 75005, Paris, France

    Mathieu Lehaut & Nathalie Sznajder

Authors
  1. Benedikt Bollig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mathieu Lehaut
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nathalie Sznajder
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Benedikt Bollig .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Shuvendu K. Lahiri

  2. University of Southern California, Los Angeles, CA, USA

    Chao Wang

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

Bollig, B., Lehaut, M., Sznajder, N. (2018). Round-Bounded Control of Parameterized Systems. 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_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01090-4_22

  • 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

Search

Navigation