Nicolas Markey

TIME Conference 2022 Conference Paper

Logical Forms of Chronicles

• Thomas Guyet
• Nicolas Markey

A chronicle is a temporal model introduced by Dousson et al. for situation recognition. In short, a chronicle consists of a set of events and a set of real-valued temporal constraints on the delays between pairs of events. This work investigates the relationship between chronicles and classical temporal-model formalisms, namely TPTL and MTL. More specifically, we answer the following question: is it possible to find an equivalent formula in such formalisms for any chronicle? This question arises from the observation that a single chronicle captures complex temporal behaviours, without imposing a particular order of the events in time. For our purpose, we introduce the subclass of linear chronicles, which set the order of occurrence of the events to be recognized in a temporal sequence. Our first result is that any chronicle can be expressed as a disjunction of linear chronicles. Our second result is that any linear chronicle has an equivalent TPTL formula. Using existing expressiveness results between TPTL and MTL, we show that some chronicles have no equivalent in MTL. This confirms that the model of chronicle has interesting properties for situation recognition.

ECAI Conference 2020 Conference Paper

Reasoning About Quality and Fuzziness of Strategic Behaviours

• Patricia Bouyer
• Orna Kupferman
• Nicolas Markey
• Bastien Maubert
• Aniello Murano
• Giuseppe Perelli

GandALF Workshop 2019 Workshop Paper

Reachability Games with Relaxed Energy Constraints

• Loïc Hélouët
• Nicolas Markey
• Ritam Raha

We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i. e. , for infinite runs). We then consider two kinds of relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, in the sense that it allows receiving more energy when the upper bound is already reached, but the extra energy will not be stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations. We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in co-NP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players.

IJCAI Conference 2019 Conference Paper

Reasoning about Quality and Fuzziness of Strategic Behaviours

• Patricia Bouyer
• Orna Kupferman
• Nicolas Markey
• Bastien Maubert
• Aniello Murano
• Giuseppe Perelli

We introduce and study SL[F], a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0, 1], reflecting ``how much'' or ``how well'' the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for ourlogic, based on a quantitative extension of Quantified CTL*.

TCS Journal 2018 Journal Article

Compositional synthesis of state-dependent switching control

• Adrien Le Coënt
• Laurent Fribourg
• Nicolas Markey
• Florian De Vuyst
• Ludovic Chamoin

We present a correct-by-design method of state-dependent control synthesis for sampled switching systems. Given a target region R of the state space, our method builds a capture set S and a control that steers any element of S into R. The method works by iterated backward reachability from R. The method is also used to synthesize a recurrence control that makes any state of R return to R infinitely often. We explain how the synthesis method can be performed in a compositional manner, and apply it to the synthesis of a compositional control of a concrete floor-heating system with 11 rooms and up to 2 11 = 2048 switching modes.

GandALF Workshop 2018 Workshop Paper

Multi-weighted Markov Decision Processes with Reachability Objectives

• Patricia Bouyer
• Mauricio González
• Nicolas Markey
• Mickael Randour

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.

MFCS Conference 2017 Conference Paper

Temporal Logics for Multi-Agent Systems (Invited Talk)

• Nicolas Markey

This is an overview of an invited talk delivered during the 42nd International Conference on Mathematical Foundations of Computer Science (MFCS 2017).

Highlights Conference 2016 Conference Abstract

Average-energy games

• Joint work with Patricia Bouyer
• Nicolas Markey
• Kim G. Larsen
• Simon Laursen

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements. This talk is based on joint work with Patricia Bouyer, Nicolas Markey, Kim G. Larsen and Simon Laursen, published in GandALF 2015 [1]. An extended version can be found on arXiv [2]. [1] P. Bouyer, N. Markey, M. Randour, K. G. Larsen, and S. Laursen. Average-energy games. In Proc. of GandALF, EPTCS 193, pages 1–15, 2015. [2] P. Bouyer, N. Markey, M. Randour, K. G. Larsen, and S. Laursen. Average-energy games (full version). CoRR, abs/1512. 08106, 2015.

GandALF Workshop 2016 Workshop Paper

Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games

• Patricia Bouyer
• Nicolas Markey
• Daniel Stan

We study the existence of mixed-strategy equilibria in concurrent games played on graphs. While existence is guaranteed with safety objectives for each player, Nash equilibria need not exist when players are given arbitrary terminal-reward objectives, and their existence is undecidable with qualitative reachability objectives (and only three players). However, these results rely on the fact that the players can enforce infinite plays while trying to improve their payoffs. In this paper, we introduce a relaxed notion of equilibria, where deviations are imprecise. We prove that contrary to Nash equilibria, such (stationary) equilibria always exist, and we develop a PSPACE algorithm to compute one.

GandALF Workshop 2015 Workshop Paper

ATLsc with partial observation

• François Laroussinie
• Nicolas Markey
• Arnaud Sangnier

Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expressive logics such as ATLsc.

GandALF Workshop 2015 Workshop Paper

Average-energy games

• Patricia Bouyer
• Nicolas Markey
• Mickael Randour
• Kim G. Larsen
• Simon Laursen

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP inter coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.

TCS Journal 2015 Journal Article

Robust reachability in timed automata and games: A game-based approach

• Patricia Bouyer
• Nicolas Markey
• Ocan Sankur

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing “robust” strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.

Highlights Conference 2013 Conference Abstract

Satisfiability of ATL with strategy contexts

• Francois Laroussinie
• Nicolas Markey

ATLsc is a powerful formalism for reasoning about multi-agent systems; it is a natural variant of the semantics of the logic ATL, as defined by Alur, Henzinger and Kupferman. Using a translation into QCTL (CTL extended with quantification over atomic propositions), we prove that ATLsc satisfiability is decidable when satisfiability is restricted to turn-based games, or when the set of moves allowed to the players in advance. On the other hand, when strategy quantification is restricted to memoryless strategies, satisfiability is undecidable in all considered cases.

GandALF Workshop 2013 Workshop Paper

Satisfiability of ATL with strategy contexts

• François Laroussinie
• Nicolas Markey

Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts, while Strategy Logic has first-order quantification over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable. We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to turn-based games. We prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we prove that restricting strategy quantification to memoryless strategies brings back undecidability.

TIME Conference 2008 Conference Paper

Good Friends are Hard to Find!

• Thomas Brihaye
• Nicolas Markey
• Mohamed Ghannem
• Lionel Rieg

We focus on the problem of finding (the size of) a minimal winning coalition in a multi-player game. We prove that deciding whether there is a winning coalition of size at most k is HP-complete, while deciding whether k is the optimal size is DP -complete. We also study different variants of our original problem: the function problem, where the aim is to effectively compute the coalition; more succinct encoding of the game; and richer families of winning objectives.

TCS Journal 2006 Journal Article

Model checking restricted sets of timed paths

• Nicolas Markey
• Jean-François Raskin

In this paper, we study the complexity of model-checking formulas of four important real-time logics ( TPTL, MTL, MITL, and TCTL ) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph. Several results are quite negative: TPTL and MTL remain undecidable along region- and zone-paths. On the other hand, we obtained PTIME algorithms for model-checking TCTL along a region path, and for MTL along a single timed path.