Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

Authors Shaull Almagor, Orna Kupferman, Yaron Velner



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.9.pdf
  • Filesize: 491 kB
  • 15 pages

Document Identifiers

Author Details

Shaull Almagor
Orna Kupferman
Yaron Velner

Cite AsGet BibTex

Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.9

Abstract

In Boolean synthesis, we are given an LTL specification, and the goal is to construct a transducer that realizes it against an adversarial environment. Often, a specification contains both Boolean requirements that should be satisfied against an adversarial environment, and multi-valued components that refer to the quality of the satisfaction and whose expected cost we would like to minimize with respect to a probabilistic environment. In this work we study, for the first time, mean-payoff games in which the system aims at minimizing the expected cost against a probabilistic environment, while surely satisfying an omega-regular condition against an adversarial environment. We consider the case the omega-regular condition is given as a parity objective or by an LTL formula. We show that in general, optimal strategies need not exist, and moreover, the limit value cannot be approximated by finite-memory strategies. We thus focus on computing the limit-value, and give tight complexity bounds for synthesizing epsilon-optimal strategies for both finite-memory and infinite-memory strategies. We show that our game naturally arises in various contexts of synthesis with Boolean and multi-valued objectives. Beyond direct applications, in synthesis with costs and rewards to certain behaviors, it allows us to compute the minimal sensing cost of omega-regular specifications -- a measure of quality in which we look for a transducer that minimizes the expected number of signals that are read from the input.
Keywords
  • Stochastic and Quantitative Synthesis
  • Mean Payoff Games
  • Sensing.

Metrics

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

References

  1. S. Almagor, U. Boker, and O. Kupferman. Formalizing and reasoning about quality. Journal of the ACM, 63(3), 2016. Google Scholar
  2. S. Almagor, D. Kuperberg, and O. Kupferman. Regular sensing. In 34th FSTTCS, volume 29 of LIPIcs, pages 161-173, 2014. Google Scholar
  3. S. Almagor, D. Kuperberg, and O. Kupferman. The sensing cost of monitoring and synthesis. In 35th FSTTCS, volume 35 of LIPIcs, pages 380-393, 2015. Google Scholar
  4. Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing expected cost under hard boolean constraints, with applications to quantitative synthesis. CoRR, abs/1604.07064, 2016. URL: http://arxiv.org/abs/1604.07064.
  5. E. Arbel, O. Rokhlenko, and K. Yorav. Sat-based synthesis of clock gating functions using 3-valued abstraction. In FMCAD, pages 198-204, 2009. Google Scholar
  6. Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In 25th CONCUR, pages 266-280, 2014. Google Scholar
  7. 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
  8. K. Chatterjee and L. Doyen. Energy and mean-payoff parity markov decision processes. In 36th MFCS, pages 206-218, 2011. Google Scholar
  9. K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj. Perfect-information stochastic mean-payoff parity games. In 17th FOSSACS, pages 210-225, 2014. 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. L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, and M. Stoelinga. Model checking discounted temporal properties. Theoretical Computer Science, 345(1):139-170, 2005. Google Scholar
  14. M. Keating, D. Flynn, R. Aitken, A. Gibbons, and K. Shi. Low Power Methodology Manual. Springer, 2007. Google Scholar
  15. O. Kupferman and M.Y. Vardi. Synthesis with incomplete information. In Advances in Temporal Logic, pages 109-127. Kluwer Academic Publishers, 2000. Google Scholar
  16. A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45-60, 1981. Google Scholar
  17. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In 16th POPL, pages 179-190, 1989. Google Scholar
  18. M.L. Puterman. Markov decision processes: discrete stochastic dynamic programming. John Wiley &Sons, 2014. Google Scholar
  19. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. I&C, 115(1):1-37, 1994. 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