Skip to main content
Top

2018 | OriginalPaper | Chapter

Round-Bounded Control of Parameterized Systems

Authors : Benedikt Bollig, Mathieu Lehaut, Nathalie Sznajder

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
2.
go back to reference Abdulla, P.A., Delzanno, G.: Parameterized verification. Int. J. Softw. Tools Technol. Transf. 18(5), 469–473 (2016)CrossRef Abdulla, P.A., Delzanno, G.: Parameterized verification. Int. J. Softw. Tools Technol. Transf. 18(5), 469–473 (2016)CrossRef
6.
go back to reference 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) 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)
8.
go back to reference Björklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4–5), 702–715 (2010)MathSciNetCrossRef Björklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4–5), 702–715 (2010)MathSciNetCrossRef
9.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
11.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
13.
go back to reference Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of FOCS 1991, pp. 368–377. IEEE Computer Society (1991) Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of FOCS 1991, pp. 368–377. IEEE Computer Society (1991)
14.
15.
go back to reference 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) 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)
16.
go back to reference Figueira, D., Praveen, M.: Playing with repetitions in data words using energy games. In: Proceedings of LICS 2018, pp. 404–413. ACM (2018) Figueira, D., Praveen, M.: Playing with repetitions in data words using energy games. In: Proceedings of LICS 2018, pp. 404–413. ACM (2018)
17.
go back to reference 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) 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)
18.
go back to reference Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014) Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014)
20.
go back to reference Kara, A.: Logics on data words: expressivity, satisfiability, model checking. Ph.D. thesis, Technical University of Dortmund (2016) Kara, A.: Logics on data words: expressivity, satisfiability, model checking. Ph.D. thesis, Technical University of Dortmund (2016)
21.
go back to reference Kozen, D.: Lower bounds for natural proof systems. In: Proceedings of SFCS 1977, pp. 254–266. IEEE Computer Society (1977) Kozen, D.: Lower bounds for natural proof systems. In: Proceedings of SFCS 1977, pp. 254–266. IEEE Computer Society (1977)
22.
go back to reference 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) 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)
25.
26.
28.
go back to reference Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)CrossRef Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)CrossRef
30.
go back to reference Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, MIT (1974) Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, MIT (1974)
33.
go back to reference Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998)MathSciNetCrossRef Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998)MathSciNetCrossRef
Metadata
Title
Round-Bounded Control of Parameterized Systems
Authors
Benedikt Bollig
Mathieu Lehaut
Nathalie Sznajder
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_22

Premium Partner