Document Open Access Logo

Synthesis from Weighted Specifications with Partial Domains over Finite Words

Authors Emmanuel Filiot, Christof Löding, Sarah Winter

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.46.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Emmanuel Filiot
  • Université libre de Bruxelles, Belgium
Christof Löding
  • RWTH Aachen University, Germany
Sarah Winter
  • Université libre de Bruxelles, Belgium

Funding

  • Filiot, Emmanuel: This work is partially supported by the MIS project F451019F (F.R.S.-FNRS). Emmanuel Filiot is a research associate at F.R.S.-FNRS.

Cite AsGet BibTex

Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from Weighted Specifications with Partial Domains over Finite Words. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.46

Abstract

In this paper, we investigate the synthesis problem of terminating reactive systems from quantitative specifications. Such systems are modeled as finite transducers whose executions are represented as finite words in (I × O)^*, where I, O are finite sets of input and output symbols, respectively. A weighted specification S assigns a rational value (or -∞) to words in (I × O)^*, and we consider three kinds of objectives for synthesis, namely threshold objectives where the system’s executions are required to be above some given threshold, best-value and approximate objectives where the system is required to perform as best as it can by providing output symbols that yield the best value and ε-best value respectively w.r.t. S. We establish a landscape of decidability results for these three objectives and weighted specifications with partial domain over finite words given by deterministic weighted automata equipped with sum, discounted-sum and average measures. The resulting objectives are not regular in general and we develop an infinite game framework to solve the corresponding synthesis problems, namely the class of (weighted) critical prefix games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Transducers
  • Theory of computation → Quantitative automata
Keywords
  • synthesis
  • weighted games
  • weighted automata on finite words

Metrics

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

References

  1. Shaull Almagor and Orna Kupferman. Good-enough synthesis. In International Conference on Computer Aided Verification, pages 541-563. Springer, 2020. Google Scholar
  2. Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, and Yaron Velner. Quantitative assume guarantee synthesis. In International Conference on Computer Aided Verification, pages 353-374. Springer, 2017. Google Scholar
  3. Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Trans. Algorithms, 6(2):28:1-28:36, 2010. Google Scholar
  4. Daniel Andersson. An improved algorithm for discounted payoff games. In ESSLLI Student Session, pages 91-98, 2006. Google Scholar
  5. Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In International Conference on Computer Aided Verification, pages 140-156. Springer, 2009. Google Scholar
  6. Roderick Bloem, Rüdiger Ehlers, and Robert Könighofer. Cooperative reactive synthesis. In Bernd Finkbeiner, Geguang Pu, and Lijun Zhang, editors, Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, volume 9364 of Lecture Notes in Computer Science, pages 394-410. Springer, 2015. Google Scholar
  7. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. J. Comput. Syst. Sci., 78(3):911-938, 2012. URL: https://doi.org/10.1016/j.jcss.2011.08.007.
  8. Udi Boker and Thomas A. Henzinger. Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  9. Udi Boker, Thomas A. Henzinger, and Jan Otop. The target discounted-sum problem. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 750-761. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.74.
  10. Patricia Bouyer, Uli Fahrenberg, Kim G Larsen, and Nicolas Markey. Timed automata with observers under energy constraints. In Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, pages 61-70, 2010. Google Scholar
  11. Tomáš Brázdil, Petr Jančar, and Antonín Kučera. Reachability games on extended vector addition systems with states. In International Colloquium on Automata, Languages, and Programming, pages 478-489. Springer, 2010. Google Scholar
  12. Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-zero sum games for reactive synthesis. In Language and Automata Theory and Applications, pages 3-23. Springer, 2016. Google Scholar
  13. Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. Acta Informatica, 54(1):41-83, 2017. URL: https://doi.org/10.1007/s00236-016-0273-2.
  14. J Richard Büchi and Lawrence H Landweber. Solving sequential conditions finite-state strategies. Trans. Ameri. Math. Soc., 138:295-311, 1969. Google Scholar
  15. Edward Chang, Zohar Manna, and Amir Pnueli. The safety-progress classification. In Logic and Algebra of Specification, pages 143-202. Springer, 1993. Google Scholar
  16. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theoretical Computer Science, 458, 2012. Google Scholar
  17. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49-60, 2012. URL: https://doi.org/10.1016/j.tcs.2012.07.038.
  18. Krishnendu Chatterjee and Thomas A. Henzinger. Assume-guarantee synthesis. In Orna Grumberg and Michael Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science, pages 261-275. Springer, 2007. Google Scholar
  19. A Church. Applications of recursive arithmetic to the problem of circuit synthesis-summaries of talks. Institute for Symbolic Logic, Cornell University, 1957. Google Scholar
  20. Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. Handbook of model checking, volume 10. Springer, 2018. Google Scholar
  21. Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The complexity of rational synthesis. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  22. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk. Energy and mean-payoff games with imperfect information. In International Workshop on Computer Science Logic, pages 260-274. Springer, 2010. Google Scholar
  23. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of weighted automata. Springer Science & Business Media, 2009. Google Scholar
  24. Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8(2):109-113, 1979. Google Scholar
  25. Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. Quantitative languages defined by functional automata. In CONCUR, volume 7454 of Lecture Notes in Computer Science, pages 132-146. Springer, 2012. Google Scholar
  26. Emmanuel Filiot, Ismaël Jecker, Nathan Lhote, Guillermo A. Pérez, and Jean-François Raskin. On delay and regret determinization of max-plus automata. In LICS, pages 1-12. IEEE Computer Society, 2017. Google Scholar
  27. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design, 39(3):261-296, 2011. Google Scholar
  28. Axel Haddad and Benjamin Monmege. Why value iteration runs in pseudo-polynomial time for discounted-payoff games. Technical note, Université libre de Bruxelles, 2015. Google Scholar
  29. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing regret in discounted-sum games. In CSL, volume 62 of LIPIcs, pages 30:1-30:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  30. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intell., 78(1):3-20, 2016. Google Scholar
  31. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. Safraless compositional synthesis. In Computer Aided Verification, 18th International Conference, CAV 2006, volume 4144 of Lecture Notes in Computer Science, pages 31-44. Springer, 2006. Google Scholar
  32. Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, and Moshe Y. Vardi. Sat-based explicit ltlf satisfiability checking. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 2946-2953. AAAI Press, 2019. Google Scholar
  33. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic ltlf synthesis. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 1362-1369. ijcai.org, 2017. Google Scholar
  34. Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1-2):343-359, 1996. 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 Imprint Privacy Contact