High-Quality Synthesis Against Stochastic Environments

Authors Shaull Almagor, Orna Kupferman



PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.28.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Shaull Almagor
Orna Kupferman

Cite AsGet BibTex

Shaull Almagor and Orna Kupferman. High-Quality Synthesis Against Stochastic Environments. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.28

Abstract

In the classical synthesis problem, we are given a linear temporal logic (LTL) formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies psi. One weakness of automated synthesis in practice is that it pays no attention to the quality of the synthesized system. Indeed, the classical setting is Boolean: a computation satisfies a specification or does not satisfy it. Accordingly, while the synthesized system is correct, there is no guarantee about its quality. In recent years, researchers have considered extensions of the classical Boolean setting to a quantitative one. The logic FLTL is a multi-valued logic that augments LTL with quality operators. The satisfaction value of an FLTL formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. Decision problems for LTL become search or optimization problems for FLTL. In particular, in the synthesis problem, the goal is to generate a transducer that satisfies the specification in the highest possible quality. Previous work considered the worst-case setting, where the goal is to maximize the quality of the computation with the minimal quality. We introduce and solve the stochastic setting, where the goal is to generate a transducer that maximizes the expected quality of a computation, subject to a given distribution of the input signals. Thus, rather than being hostile, the environment is assumed to be probabilistic, which corresponds to many realistic settings. We show that the problem is 2EXPTIME-complete, like classical LTL synthesis. The complexity stays 2EXPTIME also in two extensions we consider: one that maximizes the expected quality while guaranteeing that the minimal quality is, with probability 1, above a given threshold, and one that allows assumptions on the environment.
Keywords
  • Stochastic and Quantitative Synthesis
  • Markov Decision Process

Metrics

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

References

  1. S. Almagor, O. Kupferman, and Y. Velner. Minimizing expected cost under hard boolean constraints, with applications to quantitative synthesis. In 27th CONCUR, 2016. Google Scholar
  2. C. Baier, J. Klein, S. Klüppelholz, and S. Märcker. Computing conditional probabilities in markovian models efficiently. In 20th TACAS, pages 515-530, 2014. Google Scholar
  3. R. Bloem, K. Chatterjee, T. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In 21st CAV, volume 5643 of LNCS, pages 140-156, 2009. Google Scholar
  4. R. Bloem, R. Ehlers, and R. Könighofer. Cooperative reactive synthesis. In 13th ATVA, pages 394-410, 2015. Google Scholar
  5. V. Bruyère, E. Filiot, M. Randour, and J-F. Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In 31st STACS, volume 25 of LIPIcs, pages 199-213, 2014. Google Scholar
  6. K. Chatterjee and L. Doyen. Energy and mean-payoff parity markov decision processes. In 36th MFCS, pages 206-218, 2011. Google Scholar
  7. K. Chatterjee, T. Henzinger, and B. Jobstmann. Environment assumptions for synthesis. In 19th CONCUR, volume 5201 of LNCS, pages 147-161, 2008. Google Scholar
  8. K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Games with secure equilibria. In 19th LICS, pages 160-169, 2004. Google Scholar
  9. K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Quantitative stochastic parity games. In SODA 04, pages 121-130, 2004. Google Scholar
  10. K. Chatterjee, Z. Komárková, and J. Kretínský. Unifying two views on multiple mean-payoff objectives in markov decision processes. In 30th LICS, pages 244-256, 2015. Google Scholar
  11. A. Church. Logic, arithmetics, and automata. In Proc. Int. Congress of Mathematicians, 1962, pages 23-35. Institut Mittag-Leffler, 1963. Google Scholar
  12. L. Clemente and J-F. Raskin. Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives. In 30th LICS, pages 257-268, 2015. Google Scholar
  13. M. Faella, A. Legay, and M. Stoelinga. Model checking quantitative linear time logic. Electr. Notes Theor. Comput. Sci., 220(3):61-77, 2008. Google Scholar
  14. J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer, 1996. Google Scholar
  15. D. Fisman, O. Kupferman, and Y. Lustig. Rational synthesis. In 16th TACAS, volume 6015 of LNCS, pages 190-204, 2010. Google Scholar
  16. O. Kupferman, Y. Lustig, M.Y. Vardi, and M. Yannakakis. Temporal synthesis for bounded systems and environments. In 28th STACS, pages 615-626, 2011. Google Scholar
  17. M. Kwiatkowska and D. Parker. Automated verification and strategy synthesis for probabilistic systems. In 11th ATVA, volume 8172 of LNCS, pages 5-22, 2013. Google Scholar
  18. W. Li, L. Dworkin, and S. A. Seshia. Mining assumptions for synthesis. In 9th MEMOCODE, pages 43-50, 2011. Google Scholar
  19. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In 16th POPL, pages 179-190, 1989. Google Scholar
  20. U. Boker S. Almagor and and O. Kupferman. Formalizing and reasoning about quality. J. ACM, 63(3), 2016. Google Scholar
  21. S. Schewe and B. Finkbeiner. Bounded synthesis. In 5th ATVA, volume 4762 of LNCS, pages 474-488, 2007. Google Scholar