ManySynth | Mickael Randour

Project highlights

FNRS Incentive Grant for Scientific Research.
Project leader: Mickael Randour.
Duration: January 2018 to December 2019. Budget ~250.000 euros.

Project summary

We live in the days of ubiquitous computing: we are surrounded by reactive (computer) systems that continuously interact with their environment through user input, sensors, etc. Their correctness is often critical, either for safety reasons (e.g., ABS for cars) or due to constraints of mass production (e.g., smartphones). Unfortunately, their development is difficult and prone to errors. Formal verification and synthesis have proved to be success stories of computer science, aiming at the automated construction of provably-safe system controllers. Many techniques take roots in the game- theoretic framework, modeling the interaction between the system and its environment as a competitive game.

One crucial change over the last decade is the evolution from Boolean to quantitative specifications, giving birth to models describing performance of systems. However, prevalent frameworks only permit to consider a single quantitative (or qualitative) aspect at a time: they do not take into account their interplay and the resulting trade-offs. Such trade-offs may occur between different resources (e.g., decreasing response time requires additional computing power and energy consumption) but also between different behavioral models (e.g., average-case vs. worst-case performance). Those interactions are at the core of practical scenarios and require the developers to decide how to balance the different aspects. Hence, there is an absolute need for frameworks and tools capable of modeling interplays for the synthesis approach to be effective in practice. I coin the term “many-sided models” for such rich models in opposition to single-sided ones, which only allow to reason about a unique aspect of reactive systems.

The goal of ManySynth is to allow next-generation synthesis by establishing formal foundations, algorithms, and tools to support the paradigm shift from single-sided qualitative and quantitative models to many-sided ones, developing fundamental advances in this direction.

Publications supported by the project: 17 (2 best paper awards)

Peer-reviewed journals

Inf. Comput.
Decisiveness of stochastic systems and its application to hybrid models

Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove

Information and Computation, 2022

Abs arXiv Bib

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
@article{DBLP:journals/iandc/BouyerBRRV22, author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`{e}}re, C{\'{e}}dric and Vandenhove, Pierre}, title = {Decisiveness of stochastic systems and its application to hybrid models}, journal = {Information and Computation}, volume = {289}, number = {Part}, pages = {104861}, year = {2022}, url = {https://doi.org/10.1016/j.ic.2021.104861}, doi = {10.1016/J.IC.2021.104861}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iandc/BouyerBRRV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
LMCS
Games Where You Can Play Optimally with Arena-Independent Finite Memory

Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

Logical Methods in Computer Science, 2022

Abs arXiv Bib

For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory – finite or infinite – is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).
@article{DBLP:journals/lmcs/BouyerRORV22, author = {Bouyer, Patricia and Roux, Stéphane Le and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory}, journal = {Logical Methods in Computer Science}, volume = {18}, number = {1}, year = {2022}, url = {https://doi.org/10.46298/lmcs-18(1:11)2022}, doi = {10.46298/LMCS-18(1:11)2022}, timestamp = {Tue, 31 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/lmcs/BouyerRORV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
LMCS
Life is Random, Time is Not: Markov Decision Processes with Window Objectives

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

Logical Methods in Computer Science, 2020

Abs arXiv Bib

The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.
@article{DBLP:journals/lmcs/BrihayeDOR20, author = {Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael}, title = {Life is Random, Time is Not: Markov Decision Processes with Window Objectives}, journal = {Logical Methods in Computer Science}, volume = {16}, number = {4}, year = {2020}, url = {https://lmcs.episciences.org/6975}, timestamp = {Wed, 16 Dec 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/lmcs/BrihayeDOR20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

International peer-reviewed conferences

FSTTCS
The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India , 2022

Invited paper Abs Bib PDF

Keynote lecture at FSTTCS’22.

Two-player turn-based zero-sum games on (finite or infinite) graphs are a central framework in theoretical computer science - notably as a tool for controller synthesis, but also due to their connection with logic and automata theory. A crucial challenge in the field is to understand how complex strategies need to be to play optimally, given a type of game and a winning objective. In this invited contribution, we give a tour of recent advances aiming to characterize games where finite-memory strategies suffice (i.e., using a limited amount of information about the past). We mostly focus on so-called chromatic memory, which is limited to using colors - the basic building blocks of objectives - seen along a play to update itself. Chromatic memory has the advantage of being usable in different game graphs, and the corresponding class of strategies turns out to be of great interest to both the practical and the theoretical sides
@inproceedings{DBLP:conf/fsttcs/BouyerRV22, author = {Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre}, editor = {Dawar, Anuj and Guruswami, Venkatesan}, title = {The True Colors of Memory: {A} Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)}, booktitle = {42nd {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2022, December 18-20, 2022, {IIT} Madras, Chennai, India}, series = {LIPIcs}, volume = {250}, pages = {3:1--3:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2022.3}, doi = {10.4230/LIPICS.FSTTCS.2022.3}, timestamp = {Tue, 21 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/fsttcs/BouyerRV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
GandALF
Decisiveness of Stochastic Systems and its Application to Hybrid Models

Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove

In Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020 , 2020

Abs arXiv Bib

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
@inproceedings{DBLP:journals/corr/abs-2001-04347, author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`{e}}re, C{\'{e}}dric and Vandenhove, Pierre}, editor = {Raskin, Jean{-}Fran{\c{c}}ois and Bresolin, Davide}, title = {Decisiveness of Stochastic Systems and its Application to Hybrid Models}, booktitle = {Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020}, series = {{EPTCS}}, volume = {326}, pages = {149--165}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.326.10}, doi = {10.4204/EPTCS.326.10}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2001-04347.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Arena-Independent Finite-Memory Determinacy in Stochastic Games

Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference , 2021

Abs arXiv Bib

We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games to stochastic ones.
@inproceedings{DBLP:conf/concur/BouyerORV21, author = {Bouyer, Patricia and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, editor = {Haddad, Serge and Varacca, Daniele}, title = {Arena-Independent Finite-Memory Determinacy in Stochastic Games}, booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021, August 24-27, 2021, Virtual Conference}, series = {LIPIcs}, volume = {203}, pages = {26:1--26:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.26}, doi = {10.4230/LIPICS.CONCUR.2021.26}, timestamp = {Sun, 12 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/concur/BouyerORV21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

James C. A. Main, Mickael Randour, and Jeremy Sproston

In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference , 2021

Abs arXiv Bib

The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs. It has since proved useful in a variety of settings, including parity objectives in games and both mean-payoff and parity objectives in Markov decision processes. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.
@inproceedings{DBLP:conf/concur/MainRS21, author = {Main, James C. A. and Randour, Mickael and Sproston, Jeremy}, editor = {Haddad, Serge and Varacca, Daniele}, title = {Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives}, booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021, August 24-27, 2021, Virtual Conference}, series = {LIPIcs}, volume = {203}, pages = {25:1--25:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.25}, doi = {10.4230/LIPICS.CONCUR.2021.25}, timestamp = {Fri, 13 Aug 2021 16:29:32 +0200}, biburl = {https://dblp.org/rec/conf/concur/MainRS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Games Where You Can Play Optimally with Arena-Independent Finite Memory

Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference) , 2020

Abs arXiv Bib

For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory – finite or infinite – is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).
@inproceedings{DBLP:conf/concur/Bouyer0ORV20, author = {Bouyer, Patricia and Roux, St{\'{e}}phane Le and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, editor = {Konnov, Igor and Kov{\'{a}}cs, Laura}, title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory}, booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)}, series = {LIPIcs}, volume = {171}, pages = {24:1--24:22}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2020}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.24}, doi = {10.4230/LIPICS.CONCUR.2020.24}, timestamp = {Mon, 21 Dec 2020 13:23:22 +0100}, biburl = {https://dblp.org/rec/conf/concur/Bouyer0ORV20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
TACAS
Simple Strategies in Multi-Objective MDPs

Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, and Mickael Randour

In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I , 2020

Abs arXiv Bib

We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining the Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case can be reduced to the stationary one by a product construction. Experimental results using Storm and Gurobi show the feasibility of our algorithms.
@inproceedings{DBLP:conf/tacas/DelgrangeKQR20, author = {Delgrange, Florent and Katoen, Joost{-}Pieter and Quatmann, Tim and Randour, Mickael}, editor = {Biere, Armin and Parker, David}, title = {Simple Strategies in Multi-Objective MDPs}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, {TACAS} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {12078}, pages = {346--364}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-45190-5\_19}, doi = {10.1007/978-3-030-45190-5\_19}, timestamp = {Fri, 14 May 2021 08:34:17 +0200}, biburl = {https://dblp.org/rec/conf/tacas/DelgrangeKQR20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

CAV

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization

Frantisek Blahoudek, Alexandre Duret-Lutz, and Jan Strejcek

In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II , 2020

Bib

@inproceedings{DBLP:conf/cav/BlahoudekDS20,
  author = {Blahoudek, Frantisek and Duret{-}Lutz, Alexandre and Strejcek, Jan},
  editor = {Lahiri, Shuvendu K. and Wang, Chao},
  title = {Seminator 2 Can Complement Generalized B{\"{u}}chi Automata via
                    Improved Semi-determinization},
  booktitle = {Computer Aided Verification - 32nd International Conference, {CAV}
                    2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
  series = {Lecture Notes in Computer Science},
  volume = {12225},
  pages = {15--27},
  publisher = {Springer},
  year = {2020},
  url = {https://doi.org/10.1007/978-3-030-53291-8\_2},
  doi = {10.1007/978-3-030-53291-8\_2},
  timestamp = {Wed, 16 Mar 2022 23:55:02 +0100},
  biburl = {https://dblp.org/rec/conf/cav/BlahoudekDS20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

ICTAC

LTL to Smaller Self-Loop Alternating Automata and Back

Frantisek Blahoudek, Juraj Major, and Jan Strejcek

In Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings , 2019

Best paper arXiv Bib

Best paper award at ICTAC 2019.

@inproceedings{DBLP:conf/ictac/BlahoudekMS19,
  author = {Blahoudek, Frantisek and Major, Juraj and Strejcek, Jan},
  editor = {Hierons, Robert M. and Mosbah, Mohamed},
  title = {{LTL} to Smaller Self-Loop Alternating Automata and Back},
  booktitle = {Theoretical Aspects of Computing - {ICTAC} 2019 - 16th International
                    Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {11884},
  pages = {152--171},
  publisher = {Springer},
  year = {2019},
  url = {https://doi.org/10.1007/978-3-030-32505-3\_10},
  doi = {10.1007/978-3-030-32505-3\_10},
  timestamp = {Tue, 11 Oct 2022 14:59:07 +0200},
  biburl = {https://dblp.org/rec/conf/ictac/BlahoudekMS19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

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

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands , 2019

Best paper Abs arXiv Bib

Best paper award at CONCUR 2019.

The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.
@inproceedings{DBLP:conf/concur/BrihayeDOR19, author = {Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael}, editor = {Fokkink, Wan J. and van Glabbeek, Rob}, title = {Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}, booktitle = {30th International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30, 2019, Amsterdam, the Netherlands}, series = {LIPIcs}, volume = {140}, pages = {8:1--8:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.8}, doi = {10.4230/LIPICS.CONCUR.2019.8}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/concur/BrihayeDOR19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
CONCUR
Energy Mean-Payoff Games

Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin

In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands , 2019

Abs arXiv Bib

In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.
@inproceedings{DBLP:conf/concur/BruyereHRR19, author = {Bruy{\`{e}}re, V{\'{e}}ronique and Hautem, Quentin and Randour, Mickael and Raskin, Jean{-}Fran{\c{c}}ois}, editor = {Fokkink, Wan J. and van Glabbeek, Rob}, title = {Energy Mean-Payoff Games}, booktitle = {30th International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30, 2019, Amsterdam, the Netherlands}, series = {LIPIcs}, volume = {140}, pages = {21:1--21:17}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.21}, doi = {10.4230/LIPICS.CONCUR.2019.21}, timestamp = {Fri, 30 Aug 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/concur/BruyereHRR19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

ATVA

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata

Juraj Major, Frantisek Blahoudek, Jan Strejcek, Miriama Sasaráková, and Tatiana Zboncáková

In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings , 2019

Bib

@inproceedings{DBLP:conf/atva/MajorBSSZ19,
  author = {Major, Juraj and Blahoudek, Frantisek and Strejcek, Jan and Sasar{\'{a}}kov{\'{a}}, Miriama and Zbonc{\'{a}}kov{\'{a}}, Tatiana},
  editor = {Chen, Yu{-}Fang and Cheng, Chih{-}Hong and Esparza, Javier},
  title = {ltl3tela: {LTL} to Small Deterministic or Nondeterministic Emerson-Lei
                    Automata},
  booktitle = {Automated Technology for Verification and Analysis - 17th International
                    Symposium, {ATVA} 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {11781},
  pages = {357--365},
  publisher = {Springer},
  year = {2019},
  url = {https://doi.org/10.1007/978-3-030-31784-3\_21},
  doi = {10.1007/978-3-030-31784-3\_21},
  timestamp = {Mon, 03 Jan 2022 17:11:32 +0100},
  biburl = {https://dblp.org/rec/conf/atva/MajorBSSZ19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

ATVA

Generic Emptiness Check for Fun and Profit

Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejcek

In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings , 2019

Bib

@inproceedings{DBLP:conf/atva/BaierBD00S19,
  author = {Baier, Christel and Blahoudek, Frantisek and Duret{-}Lutz, Alexandre and Klein, Joachim and M{\"{u}}ller, David and Strejcek, Jan},
  editor = {Chen, Yu{-}Fang and Cheng, Chih{-}Hong and Esparza, Javier},
  title = {Generic Emptiness Check for Fun and Profit},
  booktitle = {Automated Technology for Verification and Analysis - 17th International
                    Symposium, {ATVA} 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {11781},
  pages = {445--461},
  publisher = {Springer},
  year = {2019},
  url = {https://doi.org/10.1007/978-3-030-31784-3\_26},
  doi = {10.1007/978-3-030-31784-3\_26},
  timestamp = {Mon, 03 Jan 2022 17:11:32 +0100},
  biburl = {https://dblp.org/rec/conf/atva/BaierBD00S19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

FSTTCS
Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions

Stéphane Le Roux, Arno Pauly, and Mickael Randour

In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India , 2018

Abs arXiv Bib

We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.
@inproceedings{DBLP:conf/fsttcs/0001PR18, author = {Roux, St{\'{e}}phane Le and Pauly, Arno and Randour, Mickael}, editor = {Ganguly, Sumit and Pandya, Paritosh K.}, title = {Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions}, booktitle = {38th {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2018, December 11-13, 2018, Ahmedabad, India}, series = {LIPIcs}, volume = {122}, pages = {38:1--38:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2018}, url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2018.38}, doi = {10.4230/LIPICS.FSTTCS.2018.38}, timestamp = {Tue, 11 Feb 2020 15:52:14 +0100}, biburl = {https://dblp.org/rec/conf/fsttcs/0001PR18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
GandALF
Multi-weighted Markov Decision Processes with Reachability Objectives

Patricia Bouyer, Mauricio González, Nicolas Markey, and Mickael Randour

In Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018 , 2018

Abs arXiv Bib

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.
@inproceedings{DBLP:journals/corr/abs-1809-03107, author = {Bouyer, Patricia and Gonz{\'{a}}lez, Mauricio and Markey, Nicolas and Randour, Mickael}, editor = {Orlandini, Andrea and Zimmermann, Martin}, title = {Multi-weighted Markov Decision Processes with Reachability Objectives}, booktitle = {Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbr{\"{u}}cken, Germany, 26-28th September 2018}, series = {{EPTCS}}, volume = {277}, pages = {250--264}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.277.18}, doi = {10.4204/EPTCS.277.18}, timestamp = {Wed, 07 Dec 2022 23:00:49 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1809-03107.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }