Life is Random, Time is Not: Markov Decision Processes with Window Objectives

Brihaye, Thomas; Delgrange, Florent; Oualhadj, Youssouf; Randour, Mickaël

doi:10.23638/LMCS-16(4:13)2020

Download

Article (Scientific journals)

Life is Random, Time is Not: Markov Decision Processes with Window Objectives

Brihaye, Thomas; Delgrange, Florent; Oualhadj, Youssouf et al.

2020 • In Logical Methods in Computer Science, 16 (4), p. 13:1-13:30

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/20.500.12907/11696

DOI
10.23638/LMCS-16(4:13)2020

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

1901.03571.pdf

Publisher postprint (523.32 kB)

Download

All documents in ORBi UMONS are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Research center :

CREMMI - Modélisation mathématique et informatique

Disciplines :

Computer science
Mathematics

Author, co-author :

Brihaye, Thomas ; Université de Mons > Faculté des Sciences > Service de Mathématiques effectives

Delgrange, Florent

Oualhadj, Youssouf

Randour, Mickaël ; Université de Mons > Faculté des Sciences > Service de Mathématiques effectives

Language :

English

Title :

Life is Random, Time is Not: Markov Decision Processes with Window Objectives

Publication date :

14 December 2020

Journal title :

Logical Methods in Computer Science

eISSN :

1860-5974

Publisher :

[Technischen Universitat Braunschweig], Braunschweig, Germany

Volume :

Issue :

Pages :

13:1-13:30

Peer reviewed :

Peer Reviewed verified by ORBi

Research unit :

S820 - Mathématiques effectives

Research institute :

R150 - Institut de Recherche sur les Systèmes Complexes

Name of the research project :

Synthèse de contrôleurs pour systèmes réactifs: synthèse quantitative dans des environnements stochastiques - Fédération Wallonie Bruxelles
3284 - CQ-Randour - ManySynth - Fédération Wallonie Bruxelles
3944 - MIS-Randour - ManySynth - Fédération Wallonie Bruxelles

Funders :

F.R.S.-FNRS - Fonds de la Recherche Scientifique

Available on ORBi UMONS :

since 18 December 2020

Statistics

Number of views

42 (3 by UMONS)

Number of downloads

74 (0 by UMONS)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

[ACD+ 17] Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, and Tobias Meggendor-fer. Value iteration for long-run average reward in Markov decision processes. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification-29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 201–221. Springer, 2017.
[AHM07] Parosh Aziz Abdulla, Noomene Ben Henda, and Richard Mayr. Decisive Markov chains. Logical Methods in Computer Science, 3(4), 2007.
[Bai15] Christel Baier. Reasoning about cost-utility constraints in probabilistic models. In Mikolaj Bojanczyk, Slawomir Lasota, and Igor Potapov, editors, Reachability Problems-9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings, volume 9328 of Lecture Notes in Computer Science, pages 1–6. Springer, 2015.
[BCFK17] Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci., 84:144–170, 2017.
[BDOR19] Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life is random, time is not: Markov decision processes with window objectives. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 26-31, 2019, Amsterdam, The Netherlands, volume 140 of LIPIcs, pages 4:1–4:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
[Bee80] Catriel Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst., 5(3):241–259, 1980.
[BFKN16] Tomás Brázdil, Vojtech Forejt, Antonín Kucera, and Petr Novotný. Stability in graphs and games. In Desharnais and Jagadeesan [DJ16], pages 10:1–10:14.
[BFRR17] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. Inf. Comput., 254:259–295, 2017.
[BGMR18] Patricia Bouyer, Mauricio González, Nicolas Markey, and Mickael Randour. Multi-weighted Markov decision processes with reachability objectives. In Andrea Orlandini and Martin Zimmer-mann, editors, Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018., volume 277 of EPTCS, pages 250–264, 2018.
[BGR19] Benjamin Bordais, Shibashis Guha, and Jean-François Raskin. Expected window mean-payoff. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 32:1–32:15. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2019.
[BHR16a] Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016., volume 226 of EPTCS, pages 135–148, 2016.
[BHR16b] Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. On the complexity of heteroge-neous multidimensional games. In Desharnais and Jagadeesan [DJ16], pages 11:1–11:15.
[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
[BKKW14] Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. Weight monitoring with linear temporal logic: complexity and decidability. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14-18, 2014, pages 11:1–11:10. ACM, 2014.
[Bra79] Gilles Brassard. A note on the complexity of cryptography (corresp.). IEEE Trans. Information Theory, 25(2):232–233, 1979.
[BRR17] Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold constraints with guarantees for parity objectives in Markov decision processes. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 121:1–121:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
[CDF+ 19] Wojciech Czerwinski, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdzinski, Ranko Lazic, and Pawel Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In Timothy M. Chan, editor, Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2019, San Diego, California, USA, January 6-9, 2019, pages 2333–2349. SIAM, 2019.
[CDRR15] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25–52, 2015.
[CH14] Krishnendu Chatterjee and Monika Henzinger. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. J. ACM, 61(3):15:1–15:40, 2014.
[CHH09] Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn. Finitary winning in omega-regular games. ACM Trans. Comput. Log., 11(1):1:1–1:27, 2009.
[CJH04] Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger. Quantitative stochastic parity games. In J. Ian Munro, editor, Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004, pages 121–130. SIAM, 2004.
[CJK+ 17] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 252–263. ACM, 2017.
[DJ16] Josée Desharnais and Radha Jagadeesan, editors. 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016.
[DJKV17] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification-29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 592–600. Springer, 2017.
[DJL18] Laure Daviaud, Marcin Jurdzinski, and Ranko Lazic. A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 325–334. ACM, 2018.
[FGO18] Nathanaël Fijalkow, Pawel Gawrychowski, and Pierre Ohlmann. The complexity of mean payoff games using universal graphs. CoRR, abs/1812.07072, 2018.
[FJ15] John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26–36, 2015.
[FV97] Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1997.
[GS97] Charles M. Grinstead and J. Laurie Snell. Introduction to probability. American Mathematical Society, 1997.
[GS09] Thomas Gawlitza and Helmut Seidl. Games through nested fixpoints. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26-July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 291–305. Springer, 2009.
[GTW02] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002.
[HJKQ18] Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann. Multi-cost bounded reachability in MDP. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems-24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pages 320–339. Springer, 2018.
[HK15] Christoph Haase and Stefan Kiefer. The odds of staying on budget. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming-42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 234–246. Springer, 2015.
[HPR18] Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Looking at mean payoff through foggy windows. Acta Inf., 55(8):627–647, 2018.
[Imm81] Neil Immerman. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci., 22(3):384–406, 1981.
[Jur98] Marcin Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119–124, 1998.
[Ran13] Mickael Randour. Automated synthesis of reliable and efficient systems through game theory: A case study. In Proc. of ECCS 2012, Springer Proceedings in Complexity XVII, pages 731–738. Springer, 2013.
[RPR18] Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending finite-memory determinacy by Boolean combination of winning conditions. In Sumit Ganguly and Paritosh K. Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 38:1–38:20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018.
[RRS15] Mickael Randour, Jean-François Raskin, and Ocan Sankur. Variations on the stochastic shortest path problem. In Deepak D’Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation-16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, volume 8931 of Lecture Notes in Computer Science, pages 1–18. Springer, 2015.
[RRS17] Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi-dimensional Markov decision processes. Formal Methods in System Design, 50(2-3):207–248, 2017.
[Tod91] Seinosuke Toda. PP is as hard as the polynomial-time hierarchy. SIAM J. Comput., 20(5):865–877, 1991.
[Tra06] Stephen D. Travers. The complexity of membership problems for circuits over sets of integers. Theor. Comput. Sci., 369(1-3):211–229, 2006.
[Var85] Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. of FOCS, pages 327–338. IEEE, 1985.