Document Open Access Logo

Strategy Synthesis for Global Window PCTL

Authors Benjamin Bordais, Damien Busatto-Gaston , Shibashis Guha , Jean-François Raskin

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.115.pdf
  • Filesize: 1.16 MB
  • 20 pages

Document Identifiers

Author Details

Benjamin Bordais
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, 91190 Gif-sur-Yvette, France
Damien Busatto-Gaston
  • Université libre de Bruxelles, Brussels, Belgium
Shibashis Guha
  • Tata Institute of Fundamental Research, Mumbai, India
Jean-François Raskin
  • Université libre de Bruxelles, Brussels, Belgium

Funding

This work is partially supported by the ARC project Non-Zero Sum Game Graphs: Applications to Reactive Synthesis and Beyond (Fédération Wallonie-Bruxelles), the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS & FWO), the COST Action 16228 GAMENET (European Cooperation in Science and Technology), by the PDR project Subgame perfection in graph games (F.R.S.- FNRS), and the DST-SERB SRG/2021/000466 "Zero-sum and Nonzero-sum Games for Controller Synthesis of Reactive Systems" project.

Cite AsGet BibTex

Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin. Strategy Synthesis for Global Window PCTL. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.115

Abstract

Given a Markov decision process (MDP) M and a formula Φ, the strategy synthesis problem asks if there exists a strategy σ s.t. the resulting Markov chain M[σ] satisfies Φ. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Stochastic processes
Keywords
  • Markov decision processes
  • synthesis
  • PCTL

Metrics

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

Related Versions

References

  1. E. Ábrahám, E. Bartocci, B. Bonakdarpour, and O. Dobe. Probabilistic hyperproperties with nondeterminism. In ATVA, pages 518-534. Springer, 2020. Google Scholar
  2. E. Ábrahám and B. Bonakdarpour. Hyperpctl: A temporal logic for probabilistic hyperproperties. In QEST, pages 20-35. Springer, 2018. Google Scholar
  3. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. J. ACM, 41(1):181-204, 1994. Google Scholar
  4. R. Andriushchenko, M. Ceska, S. Junges, and J-P Katoen. Inductive synthesis for probabilistic programs reaches new horizons. In TACAS, Part I, pages 191-209. Springer, 2021. Google Scholar
  5. C. Baier, M. Größer, M. Leucker, B. Bollig, and F. Ciesinski. Controller synthesis for probabilistic systems. In Exploring New Frontiers of Theoretical Informatics, pages 493-506. Springer US, 2004. Google Scholar
  6. C. Baier and J-P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  7. T. Brázdil, V. Forejt, J. Kretínský, and A. Kucera. The satisfiability problem for probabilistic CTL. In LICS, pages 391-402. IEEE Computer Society, 2008. Google Scholar
  8. John Canny. Some algebraic and geometric computations in pspace. In STOC, pages 460-467, 1988. Google Scholar
  9. S. Chakraborty and J-P Katoen. On the satisfiability of some simple probabilistic logics. In LICS, pages 56-65. Association for Computing Machinery, 2016. Google Scholar
  10. M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sánchez. Temporal logics for hyperproperties. In POST, pages 265-284. Springer, 2014. Google Scholar
  11. R. Dimitrova, B. Finkbeiner, and H. Torfah. Probabilistic hyperproperties of markov decision processes. In ATVA, pages 484-500. Springer, 2020. Google Scholar
  12. N. Fijalkow and F. Horn. The surprizing complexity of reachability games. CoRR, abs/1010.2420, 2010. URL: http://arxiv.org/abs/1010.2420.
  13. J. W. Gray III. Toward a mathematical foundation for information flow security. J. Comput. Secur., 1(3-4):255-294, 1992. Google Scholar
  14. Jan Kretínský and Alexej Rotar. The satisfiability problem for unbounded fragments of probabilistic CTL. In CONCUR, pages 32:1-32:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  15. A. Kucera, V. Forejt, V. Brozek, and T. Brazdil. Stochastic games with branching-time winning objectives. In LICS, pages 349-358. IEEE Computer Society, 2006. Google Scholar
  16. A. Kučera and O. Stražovský. On the controller synthesis for finite-state markov decision processes. In FSTTCS, pages 541-552. Springer Berlin Heidelberg, 2005. Google Scholar
  17. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  18. J. Renegar. On the computational complexity and geometry of the first-order theory of the reals. part iii: Quantifier elimination. Journal of Symbolic Computation, 13(3):329-352, 1992. 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