Document Open Access Logo

Synthesis in Distributed Environments

Authors Bernd Finkbeiner, Paul Gölz

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.28.pdf
  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Bernd Finkbeiner
Paul Gölz

Cite As Get BibTex

Bernd Finkbeiner and Paul Gölz. Synthesis in Distributed Environments. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 28:1-28:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.28

Abstract

Most approaches to the synthesis of reactive systems study the problem in terms of a two-player game with complete observation. In many applications, however, the system's environment consists of several distinct entities, and the system must actively communicate with these entities in order to obtain information available in the environment. In this paper, we model such environments as a team of players and keep track of the information known to each individual player. This allows us to synthesize programs that interact with a distributed environment and leverage multiple interacting sources of information. 
The synthesis problem in distributed environments corresponds to solving a special class of Petri games, i.e., multi-player games played over Petri nets, where the net has a distinguished token representing the system and an arbitrary number of tokens representing the environment. While, in general, even the decidability of Petri games is an open question, we show that the synthesis problem in distributed environments can be solved in polynomial time for nets with up to two environment tokens. For an arbitrary but fixed number of three or more environment tokens, the problem is NP-complete. If the number of environment tokens grows with the size of the net, the problem is EXPTIME-complete.

Subject Classification

Keywords
  • reactive synthesis
  • distributed information
  • causal memory
  • Petri nets

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Krzysztof R. Apt and Erich Grädel. Lectures in game theory for computer scientists. Cambridge University Press, 2011. Google Scholar
  2. Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett., 8(3):121-123, 1979. URL: http://dx.doi.org/10.1016/0020-0190(79)90002-4.
  3. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Acacia+, a tool for LTL synthesis. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 652-657. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31424-7_45.
  4. J. Richard Buchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: http://dx.doi.org/10.2307/1994916.
  5. Rüdiger Ehlers. Unbeast: Symbolic bounded synthesis. In Parosh Aziz Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6605 of Lecture Notes in Computer Science, pages 272-275. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19835-9_25.
  6. Javier Esparza. Model checking using net unfoldings. Sci. Comput. Program., 23(2-3):151-195, 1994. URL: http://dx.doi.org/10.1016/0167-6423(94)00019-0.
  7. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. Encodings of bounded synthesis. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, volume 10205 of Lecture Notes in Computer Science, pages 354-370, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54577-5_20.
  8. Bernd Finkbeiner. Bounded synthesis for petri games. In Roland Meyer, André Platzer, and Heike Wehrheim, editors, Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, volume 9360 of Lecture Notes in Computer Science, pages 223-237. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-23506-6_15.
  9. Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Symbolic vs. bounded synthesis for Petri games. In Dana Fisman and Swen Jacobs, editors, 6th Workshop on Synthesis (SYNT 2017). EPTCS, 2017. URL: https://www.react.uni-saarland.de/publications/FGHO17.pdf.
  10. Bernd Finkbeiner, Manuel Gieseking, and Ernst-Rüdiger Olderog. Adam: Causality-based synthesis of distributed systems. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 433-439. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21690-4_25.
  11. Bernd Finkbeiner and Paul Gölz. Synthesis in distributed environments. CoRR, abs/1710.05368, 2017. URL: http://arxiv.org/abs/1710.05368.
  12. Bernd Finkbeiner and Ernst-Rüdiger Olderog. Petri games: Synthesis of distributed systems with causal memory. Inf. Comput., 253:181-203, 2017. URL: http://dx.doi.org/10.1016/j.ic.2016.07.006.
  13. Bernd Finkbeiner and Sven Schewe. Semi-automatic distributed synthesis. In Doron A. Peled and Yih-Kuen Tsay, editors, Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 263-277. Springer, 2005. URL: http://dx.doi.org/10.1007/11562948_21.
  14. Paul Gastin, Benjamin Lerman, and Marc Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 275-286. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30538-5_23.
  15. Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker. The 3rd reactive synthesis competition (SYNTCOMP 2016): Benchmarks, participants & results. In Ruzica Piskac and Rayna Dimitrova, editors, Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016., volume 229 of EPTCS, pages 149-177, 2016. URL: http://dx.doi.org/10.4204/EPTCS.229.12.
  16. Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, and Roderick Bloem. Anzu: A tool for property synthesis. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 258-262. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73368-3_29.
  17. Anca Muscholl and Igor Walukiewicz. Distributed synthesis for acyclic architectures. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 639-651. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.639.
  18. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II, pages 746-757. IEEE Computer Society, 1990. URL: http://dx.doi.org/10.1109/FSCS.1990.89597.
  19. Stuart Russell and Peter Norvig. Artificial Intelligence - A Modern Approach. Pearson, 3rd edition, 2009. Google Scholar
  20. Larry J. Stockmeyer and Ashok K. Chandra. Provably difficult combinatorial games. SIAM J. Comput., 8(2):151-174, 1979. URL: http://dx.doi.org/10.1137/0208013.
  21. Wieslaw Zielonka. Notes on finite asynchronous automata. ITA, 21(2):99-135, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact