2023 | |
---|---|

[BKM+23] | Patricia Bouyer,
Orna Kupferman,
Nicolas Markey,
Bastien Maubert,
Aniello Murano, and
Giuseppe Perelli.
Reasoning about Quality and Fuzziness of Strategic
Behaviours.
ACM Transactions on Computational Logic.
ACM Press, 2023. To appear.
- Abstract
Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In the first class, SL (Strategy Logic) is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is LTL[F], which extends LTL with quality operators. In this work we introduce and study SL[F], which enables the specification of quantitative strategic behaviors. 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, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for SL[F], based on a quantitative extension of Quantified CTL*. Our algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems' behavior
@article{tocl2023-BKMMMP, author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe}, title = {Reasoning about Quality and Fuzziness of Strategic Behaviours}, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, year = {2023}, note = {To~appear}, abstract = {Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In~the first class, SL~(Strategy~Logic)~is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is \(\textsf{LTL}[\mathcal{F}]\), which extends \textsf{LTL} with quality operators. \par In~this work we introduce and study \(\textsf{SL}[\mathcal{F}]\), which enables the specification of quantitative strategic behaviors. The satisfaction value of an \(\textsf{SL}[\mathcal{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 \(\textsf{SL}[\mathcal{F}]\) in quantitative reasoning about multi-agent systems, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for \(\textsf{SL}[\mathcal{F}]\), based on a quantitative extension of Quantified~\(\textsf{CTL}^*\). Our~algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems' behavior}, } |

2022 | |

[HMR22] | Loïc Hélouët,
Nicolas Markey, and
Ritam Raha.
Reachability games with relaxed energy constraints.
Information and Computation 285 (Part B).
Elsevier, May 2022.
- Abstract
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 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, i.e., when the upper bound is reached, the extra energy is not 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 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. We then address the problem of existence of bounds for a given arena. We show that with reachability objectives, existence can be a simpler problem than the game itself, and conversely that with infinite games, existence can be harder.
@article{icomp2022-HMR, author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and Raha, Ritam}, title = {Reachability games with relaxed energy constraints}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {285~(Part~B)}, year = {2022}, month = may, doi = {10.1016/j.ic.2021.104806}, abstract = {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 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, i.e., when the upper bound is reached, the extra energy is not 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. \par 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 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. We then address the problem of existence of bounds for a given arena. We show that with reachability objectives, existence can be a simpler problem than the game itself, and conversely that with infinite games, existence can be harder.}, } |

[BMS+22] | Nathalie Bertrand,
Nicolas Markey,
Suman Sadhukhan, and
Ocan Sankur.
Semilinear Representations for Series-Parallel
Atomic Congestion Games.
In FSTTCS'22,
Leibniz International Proceedings in Informatics 250, pages 32:1-32:20. Leibniz-Zentrum für Informatik, December 2022.
- Abstract
We consider atomic congestion games on series-parallel networks, and study the structure of the sets of Nash equilibria and social local optima on a given network when the number of players varies. We establish that these sets are definable in Presburger arithmetic and that they admit semilinear representations whose all period vectors have a common direction. As an application, we prove that the prices of anarchy and stability converge to 1 as the number of players goes to infinity, and show how to exploit these semilinear representations to compute these ratios precisely for a given network and number of players.
@inproceedings{fsttcs2022-BMSS, author = {Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan}, title = {Semilinear Representations for Series-Parallel Atomic Congestion Games}, editor = {Dawar, Anuj and Guruswami, Venkatesan}, booktitle = {{P}roceedings of the 42nd {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'22)}, acronym = {{FSTTCS}'22}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {250}, pages = {32:1-32:20}, year = {2022}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2022.32}, abstract = {We~consider atomic congestion games on series-parallel networks, and study the structure of the sets of Nash equilibria and social local optima on a given network when the number of players varies. We establish that these sets are definable in Presburger arithmetic and that they admit semilinear representations whose all period vectors have a common direction. As~an~application, we~prove that the prices of anarchy and stability converge to~1 as the number of players goes to infinity, and show how to exploit these semilinear representations to compute these ratios precisely for a given network and number of players.}, } |

[BMS+22] | Nathalie Bertrand,
Nicolas Markey,
Ocan Sankur, and
Nicolas Waldburger.
Parameterized safety verification of round-based
shared-memory systems.
In ICALP'22,
Leibniz International Proceedings in Informatics, pages 113:1-113:20. Leibniz-Zentrum für Informatik, July 2022.
- Abstract
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm of [J. Aspnes; Fast deterministic consensus in a noisy environment; J. Algorithms, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.
@inproceedings{icalp2022-BMSW, author = {Bertrand, Nathalie and Markey, Nicolas and Sankur, Ocan and Waldburger, Nicolas}, title = {Parameterized safety verification of round-based shared-memory systems}, editor = {Woodruff, David and Boja{\'n}czyk, Miko{\l}aj}, booktitle = {{P}roceedings of the 49th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'22)}, acronym = {{ICALP}'22}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, pages = {113:1-113:20}, year = {2022}, month = jul, doi = {10.4230/LIPIcs.ICALP.2022.113}, abstract = {We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm~of [J.~Aspnes; Fast deterministic consensus in a noisy environment; J.~Algorithms,~2002], we~consider round-based distributed algorithms communicating with shared memory. A~particular challenge in these systems is that 1)~the~number of processes is unbounded, and, more importantly, 2)~there is a fresh set of registers at each round. A~verification algorithm thus needs to manage both sources of infinity. In~this setting, we~prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For~negative instances of the safety verification problem, we~also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.}, } |

[GM22] | Thomas Guyet and
Nicolas Markey.
Logical forms of chronicles.
In TIME'22,
Leibniz International Proceedings in Informatics, pages 7:1-7:15. Leibniz-Zentrum für Informatik, November 2022.
- Abstract
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 that do not order the events in time.In this article, we introduce the subclass of linear chronicles, which defines a temporal order of occurrence of the event 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.
@inproceedings{time2022-GM, author = {Guyet, {\relax Th}omas and Markey, Nicolas}, title = {Logical forms of chronicles}, editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano}, booktitle = {{P}roceedings of the 29th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'22)}, acronym = {{TIME}'22}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, pages = {7:1-7:15}, year = {2022}, month = nov, doi = {10.4230/LIPIcs.TIME.2022.7}, abstract = {A~chronicle is a temporal model introduced by Dousson~\textit{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 \textsf{TPTL} and~\textsf{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 that do not order the events in time.\par In~this article, we~introduce the subclass of linear chronicles, which defines a temporal order of occurrence of the event 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 \textsf{TPTL} formula. Using existing expressiveness results between \textsf{TPTL} and~\textsf{MTL}, we~show that some chronicles have no equivalent in~\textsf{MTL}. This confirms that the model of chronicle has interesting properties for situation recognition.}, } |

[GMS22] | Aline Goeminne,
Nicolas Markey, and
Ocan Sankur.
Non-Blind Strategies in Timed Network Congestion
Games.
In FORMATS'22,
Lecture Notes in Computer Science 13465, pages 183-199. Springer-Verlag, September 2022.
- Abstract
Network congestion games are a convenient model for reasoning about routing problems in a network: agents have to move from a source to a target vertex while avoiding congestion, measured as a cost depending on the number of players using the same link. Network congestion games have been extensively studied over the last 40 years, while their extension with timing constraints were considered more recently. Most of the results on network congestion games consider blind strategies: they are static, and do not adapt to the strategies selected by the other players. We extend the recent results of [Bertrand *et al.*, Dynamic network congestion games. FSTTCS'20] to timed network congestion games, in which the availability of the edges depend on (discrete) time. We prove that computing Nash equilibria satisfying some constraint on the total cost (and in particular, computing the best and worst Nash equilibria), and computing the social optimum, can be achieved in exponential space. The social optimum can be computed in polynomial space if all players have the same source and target.
@inproceedings{formats2022-GMS, author = {Goeminne, Aline and Markey, Nicolas and Sankur, Ocan}, title = {Non-Blind Strategies in Timed Network Congestion Games}, editor = {Bogomolov, Sergiy and Parker, David}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'22)}, acronym = {{FORMATS}'22}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {13465}, pages = {183-199}, year = {2022}, month = sep, doi = {10.1007/978-3-031-15839-1_11}, abstract = {Network congestion games are a convenient model for reasoning about routing problems in a network: agents have to move from a source to a target vertex while avoiding congestion, measured as a cost depending on the number of players using the same link. Network congestion games have been extensively studied over the last 40 years, while their extension with timing constraints were considered more recently. \par Most of the results on network congestion games consider blind strategies: they are static, and do not adapt to the strategies selected by the other players. We extend the recent results of [Bertrand~\textit{et~al.}, Dynamic network congestion games. FSTTCS'20] to timed network congestion games, in which the availability of the edges depend on (discrete) time. We prove that computing Nash equilibria satisfying some constraint on the total cost (and in particular, computing the best and worst Nash equilibria), and computing the social optimum, can be achieved in exponential space. The social optimum can be computed in polynomial space if all players have the same source and target.}, } |

[NSJ+22] | Reiya Noguchi,
Ocan Sankur,
Thierry Jéron,
Nicolas Markey, and
David Mentré.
Repairing Real-Time Requirements.
In ATVA'22,
Lecture Notes in Computer Science 13505, pages 371-387. Springer-Verlag, October 2022.
- Abstract
We consider the problem of repairing inconsistent real-time requirements with respect to two consistency notions: non-vacuity, which means that each requirement can be realized without violating other ones, and rt-consistency, which means that inevitable violations are detected immediately. We provide an iterative algorithm, based on solving SMT queries, to replace designated parameters of real-time requirements with new Boolean expressions and time constraints, so that the resulting set of requirements becomes consistent.
@inproceedings{atva2022-NSJMM, author = {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron, Thierry and Markey, Nicolas and Mentr{\'e}, David}, title = {Repairing Real-Time Requirements}, editor = {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and Wu, Zhilin}, booktitle = {{P}roceedings of the 20th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'22)}, acronym = {{ATVA}'22}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {13505}, pages = {371-387}, year = {2022}, month = oct, doi = {10.1007/978-3-031-19992-9_24}, abstract = {We~consider the problem of repairing inconsistent real-time requirements with respect to two consistency notions: non-vacuity, which means that each requirement can be realized without violating other ones, and rt-consistency, which means that inevitable violations are detected immediately. We~provide an iterative algorithm, based on solving SMT queries, to replace designated parameters of real-time requirements with new Boolean expressions and time constraints, so that the resulting set of requirements becomes consistent.}, } |

2021 | |

[BBF+21] | Giovanni Bacci,
Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen,
Nicolas Markey, and
Pierre-Alain Reynier.
Optimal and Robust Controller Synthesis Using Energy
Timed Automata with Uncertainty.
Formal Aspects of Computing 33(1):3-25. Springer-Verlag, January 2021.
- Abstract
In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.
@article{fac2020-BBFLMR, author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim Guldstrand and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty}, publisher = {Springer-Verlag}, journal = {Formal Aspects of Computing}, volume = {33}, number = {1}, pages = {3-25}, year = {2021}, month = jan, doi = {10.1007/s00165-020-00521-4}, abstract = {In~this paper, we~propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The~framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We~prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We~also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our~algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we~illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.}, } |

[BHJ+21] | Patricia Bouyer,
Léo Henry,
Samy Jaziri,
Thierry Jéron, and
Nicolas Markey.
Diagnosing timed automata using timed markings.
International Journal on Software Tools for
Technology Transfer 23(2):229-253. Springer-Verlag, April 2021.
- Abstract
We consider the problems of efficiently diagnosing (and predicting) what did (and will) happen after a given sequence of observations of the execution of a partially-observable one-clock timed automaton. This is made difficult by the facts that timed automata are infinite-state systems, and that they can in general not be determinized. We introduce timed markings as a formalism to keep track of the evolution of the set of reachable configurations over time. We show how timed markings can be used to efficiently represent the closure under silent transitions of such automata. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002], and provide some insight to a generalization of our approach to n-clock timed automata.
@article{sttt23(2)-BHJJM, author = {Bouyer, Patricia and Henry, L{\'e}o and Jaziri, Samy and J{\'e}ron, Thierry and Markey, Nicolas}, title = {Diagnosing timed automata using timed markings}, publisher = {Springer-Verlag}, journal = {International Journal on Software Tools for Technology Transfer}, volume = {23}, number = {2}, pages = {229-253}, year = {2021}, month = apr, doi = {10.1007/s10009-021-00606-2}, abstract = {We~consider the problems of efficiently diagnosing (and~predicting) what did (and~will) happen after a given sequence of observations of the execution of a partially-observable one-clock timed automaton. This is made difficult by the facts that timed automata are infinite-state systems, and that they can in general not be determinized. \par We~introduce timed markings as a formalism to keep track of the evolution of the set of reachable configurations over time. We show how timed markings can be used to efficiently represent the closure under silent transitions of such automata. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata,~2002], and provide some insight to a generalization of our approach to {{\(n\)}}-clock timed automata.}, } |

2020 | |

[ALM20] | Étienne André,
Didier Lime, and
Nicolas Markey.
Language-preservation problems in parametric timed
automata.
Logical Methods in Computer Science 16(1).
January 2020.
- Abstract
Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.
@article{lmcs16(1)-ALM, author = {Andr{\'e}, {\'E}tienne and Lime, Didier and Markey, Nicolas}, title = {Language-preservation problems in parametric timed automata}, journal = {Logical Methods in Computer Science}, volume = {16}, number = {1}, year = {2020}, month = jan, doi = {10.23638/LMCS-16(1:5)2020}, abstract = {Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In~this paper, we~address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We~show that these problems are undecidable both for general PTA and for the restricted class of L{\slash}U-PTA, even for integer-valued parameters, or over bounded time. On~the other~hand, we~exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We~also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.}, } |

[GBM20] | Patrick Gardy,
Patricia Bouyer, and
Nicolas Markey.
Dependences in Strategy Logic.
Theory of Computing Systems 64(3):467-507. Springer-Verlag, April 2020.
- Abstract
Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on *strategy dependences*in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero*et al.*, Reasoning about strategies: On the model-checking problem, 2014]. We explain why*elementary*dependences, as defined by Mogavero*et al.*, do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing*timeline*dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics.
@article{tocsys64(3)-GBM, author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas}, title = {Dependences in Strategy Logic}, publisher = {Springer-Verlag}, journal = {Theory of Computing Systems}, volume = {64}, number = {3}, pages = {467-507}, year = {2020}, month = apr, doi = {10.1007/s00224-019-09926-y}, abstract = {Strategy Logic~(\textsf{SL}) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in~\textsf{SL}, one can quantify over strategies, assign them to agents, and express \textsf{LTL} properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking \textsf{SL} has non-elementary complexity; second, the exact semantics of \textsf{SL} is rather intricate, and may not correspond to what is expected. In~this paper, we~focus on \emph{strategy dependences} in~\textsf{SL}, by tracking how existentially-quantified strategies in a formula may (or~may~not) depend on other strategies selected in the formula, revisiting the approach of~[Mogavero \emph{et~al.}, Reasoning about strategies: On~the model-checking problem,~2014]. We~explain why \emph{elementary} dependences, as defined by Mogavero~\emph{et~al.}, do not exactly capture the intended concept of behavioral strategies. We~address this discrepancy by introducing \emph{timeline} dependences, and exhibit a large fragment of \textsf{SL} for which model checking can be performed in \textsf{2EXPTIME} under this new semantics.}, } |

[BMS+20] | Nathalie Bertrand,
Nicolas Markey,
Suman Sadhukhan, and
Ocan Sankur.
Dynamic network congestion games.
In FSTTCS'20,
Leibniz International Proceedings in Informatics 182, pages 40:1-40:16. Leibniz-Zentrum für Informatik, December 2020.
- Abstract
Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games (NCGs), the resources correspond to simple paths in a graph, e.g. representing routing options from a source to a target. In this paper, we introduce a variant of NCGs, referred to as dynamic NCGs: in this setting, players take transitions synchronously, they select their next transitions dynamically, and they are charged a cost that depends on the number of players simultaneously using the same transition. We study, from a complexity perspective, standard concepts of game theory in dynamic NCGs: social optima, Nash equilibria, and subgame perfect equilibria. Our contributions are the following: the existence of a strategy profile with social cost bounded by a constant is in PSPACE and NP-hard. (Pure) Nash equilibria always exist in dynamic NCGs; the existence of a Nash equilibrium with bounded cost can be decided in EXPSPACE, and computing a witnessing strategy profile can be done in doubly-exponential time. The existence of a subgame perfect equilibrium with bounded cost can be decided in 2EXPSPACE, and a witnessing strategy profile can be computed in triply-exponential time.
@inproceedings{fsttcs2020-BMSS, author = {Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan}, title = {Dynamic network congestion games}, editor = {Saxena, Nitin and Simon, Sunil}, booktitle = {{P}roceedings of the 40th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'20)}, acronym = {{FSTTCS}'20}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {182}, pages = {40:1-40:16}, year = {2020}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2020.40}, abstract = {Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games~(NCGs), the resources correspond to simple paths in a graph, e.g.~representing routing options from a source to a target. In this paper, we introduce a variant of~NCGs, referred to as dynamic~NCGs: in~this setting, players take transitions synchronously, they select their next transitions dynamically, and they are charged a cost that depends on the number of players simultaneously using the same transition. \par We~study, from a complexity perspective, standard concepts of game theory in dynamic NCGs: social optima, Nash equilibria, and subgame perfect equilibria. Our contributions are the following: the existence of a strategy profile with social cost bounded by a constant is in PSPACE and NP-hard. (Pure)~Nash equilibria always exist in dynamic~NCGs; the existence of a Nash equilibrium with bounded cost can be decided in EXPSPACE, and computing a witnessing strategy profile can be done in doubly-exponential time. The~existence of a subgame perfect equilibrium with bounded cost can be decided in 2EXPSPACE, and a witnessing strategy profile can be computed in triply-exponential~time.}, } |

[CJM+20] | Emily Clement,
Thierry Jéron,
Nicolas Markey, and
David Mentré.
Computing maximally-permissive strategies in acyclic
timed automata.
In FORMATS'20,
Lecture Notes in Computer Science 12288, pages 111-126. Springer-Verlag, September 2020.
- Abstract
Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models. In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.
@inproceedings{formats2020-CJMM, author = {Clement, Emily and J{\'e}ron, Thierry and Markey, Nicolas and Mentr{\'e}, David}, title = {Computing maximally-permissive strategies in acyclic timed automata}, editor = {Bertrand, Nathalie and Jansen, Nils}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'20)}, acronym = {{FORMATS}'20}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {12288}, pages = {111-126}, year = {2020}, month = sep, doi = {10.1007/978-3-030-57628-8_7}, abstract = {Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in~particular, a~state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models. \par In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and~an associated maximally-permissive strategy) in acyclic timed automata and games.}, } |

[HJM20] | Léo Henry,
Thierry Jéron, and
Nicolas Markey.
Active learning of timed automata with unobservable
resets.
In FORMATS'20,
Lecture Notes in Computer Science 12288, pages 144-160. Springer-Verlag, September 2020.
- Abstract
Active learning of timed languages is concerned with the inference of timed automata by observing some of the timed words in their languages. The learner can query for the membership of words in the language, or propose a candidate model and ask if it is equivalent to the target. The major difficulty of this framework is the inference of clock resets, which are central to the dynamics of timed automata but not directly observable. Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where some transitions may reset no clocks. Central to our contribution is the notion of invalidity, and the algorithm and data structures to deal with it, allowing on-the-fly detection and pruning of reset hypotheses that contradict observations. This notion is a key to any efficient active-learning procedure for generic timed automata.
@inproceedings{formats2020-HJM, author = {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey, Nicolas}, title = {Active learning of timed automata with unobservable resets}, editor = {Bertrand, Nathalie and Jansen, Nils}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'20)}, acronym = {{FORMATS}'20}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {12288}, pages = {144-160}, year = {2020}, month = sep, doi = {10.1007/978-3-030-57628-8_9}, abstract = {Active learning of timed languages is concerned with the inference of timed automata by observing some of the timed words in their languages. The learner can query for the membership of words in the language, or propose a candidate model and ask if it is equivalent to the target. The major difficulty of this framework is the inference of clock resets, which are central to the dynamics of timed automata but not directly observable. \par Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where some transitions may reset no clocks. \par Central to our contribution is the notion of invalidity, and the algorithm and data structures to deal with it, allowing on-the-fly detection and pruning of reset hypotheses that contradict observations. This notion is a key to any efficient active-learning procedure for generic timed automata.}, } |

[JMM+20] | Thierry Jéron,
Nicolas Markey,
David Mentré,
Reiya Noguchi, and
Ocan Sankur.
Incremental methods for checking real-time
consistency.
In FORMATS'20,
Lecture Notes in Computer Science 12288, pages 249-264. Springer-Verlag, September 2020.
- Abstract
Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results.
@inproceedings{formats2020-JMMNS, author = {J{\'e}ron, Thierry and Markey, Nicolas and Mentr{\'e}, David and Noguchi, Reiya and Sankur, Ocan}, title = {Incremental methods for checking real-time consistency}, editor = {Bertrand, Nathalie and Jansen, Nils}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'20)}, acronym = {{FORMATS}'20}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {12288}, pages = {249-264}, year = {2020}, month = sep, doi = {10.1007/978-3-030-57628-8_15}, abstract = {Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We~consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We~generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results.}, } |

2019 | |

[BKM+19] | Patricia Bouyer,
Orna Kupferman,
Nicolas Markey,
Bastien Maubert,
Aniello Murano, and
Giuseppe Perelli.
Reasoning about Quality and Fuzziness of Strategic
Behaviours.
In IJCAI'19,
pages 1588-1594.
IJCAI organization, August 2019.
- Abstract
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 our logic, based on a quantitative extension of Quantified CTL.
@inproceedings{ijcai2019-BKMMMP, author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe}, title = {Reasoning about Quality and Fuzziness of Strategic Behaviours}, editor = {Kraus, Sarit}, booktitle = {{P}roceedings of the 28th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI}'19)}, acronym = {{IJCAI}'19}, publisher = {IJCAI organization}, pages = {1588-1594}, year = {2019}, month = aug, doi = {10.24963/ijcai.2019/220}, abstract = {We~introduce and study {\(\textsf{SL}[\mathcal{F}]\)}---a~quantitative extension of {\(\textsf{SL}\)} (Strategy Logic), one~of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an {\(\textsf{SL}[\mathcal{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 {\(\textsf{SL}[\mathcal{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 our logic, based on a quantitative extension of Quantified~\textsf{CTL}.}, } |

[HMR19] | Loïc Hélouët,
Nicolas Markey, and
Ritam Raha.
Reachability games with relaxed energy constraints.
In GandALF'19,
Electronic Proceedings in Theoretical Computer
Science 305, pages 17-33. September 2019.
- Abstract
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 coNP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players.
@inproceedings{gandalf2019-HMR, author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and Raha, Ritam}, title = {Reachability games with relaxed energy constraints}, editor = {Leroux, J{\'e}r{\^o}me and Raskin, Jean-Fran{\c c}ois}, booktitle = {{P}roceedings of the 10th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics and {F}ormal {V}erification ({GandALF}'19)}, acronym = {{GandALF}'19}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {305}, pages = {17-33}, year = {2019}, month = sep, doi = {10.4204/EPTCS.305.2}, abstract = {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 \textsf{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 \emph{weak upper bound}, the upper bound is \emph{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 \emph{temporary violations} of the upper bound, imposing limits on the number or on the amount of violations.\par 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 \textsf{coNP} in the two-player setting. Allowing for bounded violations makes the problem \textsf{PSPACE}-complete for one-player arenas and \textsf{EXPTIME}-complete for two players.}, } |

[RSM19] | Victor Roussanaly,
Ocan Sankur, and
Nicolas Markey.
Abstraction Refinement Algorithms for Timed
Automata.
In CAV'19,
Lecture Notes in Computer Science 11561, pages 22-40. Springer-Verlag, July 2019.
- Abstract
We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.
@inproceedings{cav2019-RSM, author = {Roussanaly, Victor and Sankur, Ocan and Markey, Nicolas}, title = {Abstraction Refinement Algorithms for Timed Automata}, editor = {Dillig, I{\c s}il and Ta{\c s}iran, Serdar}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'19)}, acronym = {{CAV}'19}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {11561}, pages = {22-40}, year = {2019}, month = jul, doi = {10.1007/978-3-030-25540-4_2}, abstract = {We~present abstraction-refinement algorithms for model checking safety properties of timed automata. The~abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We~implement this idea in two~ways: an~enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.}, } |

[GBL+19] | Mauricio González,
Patricia Bouyer,
Samson Lasaulce, and
Nicolas Markey.
Optimisation en présence de contraintes en
probabilités et processus markoviens
contrôlés.
In GRETSI'19.
August 2019.
- Abstract
This article focuses on the existence and synthesis of strategies in double-weighted Markov decision processes, which satisfy both a probability constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using another reachability condition. This work generalizes a scheduling problem for energy consumption (typically the problem of charging electric vehicles). We study the set of values of a parameter (a threshold) for which the problem has a solution, and show how a partial characterization of this set can be obtained via two sequences of optimization problems. We also discuss the completeness and feasibility of the resulting approach.
@inproceedings{gretsi2019-GBLM, author = {Gonz{\'a}lez, Mauricio and Bouyer, Patricia and Lasaulce, Samson and Markey, Nicolas}, title = {Optimisation en pr\'esence de contraintes en probabilit\'es et processus markoviens contr\^ol\'es}, booktitle = {{A}ctes du 27{\`e}me {C}olloque du {G}roupe d'{\'E}tudes du {T}raitement du {S}ignal et des {I}mages ({GRETSI}'19)}, acronym = {{GRETSI}'19}, year = {2019}, month = aug, abstract = {This article focuses on the existence and synthesis of strategies in double-weighted Markov decision processes, which satisfy both a probability constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using another reachability condition. This work generalizes a scheduling problem for energy consumption (typically the problem of charging electric vehicles). We~study the set of values of a parameter (a~threshold) for which the problem has a solution, and show how a partial characterization of this set can be obtained via two sequences of optimization problems. We~also discuss the completeness and feasibility of the resulting approach.}, } |

2018 | |

[BMR+18] | Patricia Bouyer,
Nicolas Markey,
Mickael Randour,
Kim Guldstrand Larsen, and
Simon Laursen.
Average-energy games.
Acta Informatica 55(2):91-127. Springer-Verlag, March 2018.
- Abstract
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.
@article{acta55(2)-BMRLL, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim Guldstrand and Laursen, Simon}, title = {Average-energy games}, publisher = {Springer-Verlag}, journal = {Acta Informatica}, volume = {55}, number = {2}, pages = {91-127}, year = {2018}, month = mar, doi = {10.1007/s00236-016-0274-1}, abstract = {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 \(\textsf{NP}\cap\textsf{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.}, } |

[LFM+18] | Adrien Le Coënt,
Laurent Fribourg,
Nicolas Markey,
Florian De Vuyst, and
Ludovic Chamoin.
Distributed Synthesis of State-Dependent Switching
Control.
Theoretical Computer Science 750:53-68. Elsevier, November 2018.
- Abstract
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. It 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 for a concrete floor-heating system with 11 rooms and up to 211=2048 switching modes.
@article{tcs750()-LFMDC, author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and Markey, Nicolas and De{~}Vuyst, Florian and Chamoin, Ludovic}, title = {Distributed Synthesis of State-Dependent Switching Control}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {750}, pages = {53-68}, year = {2018}, month = nov, doi = {10.1016/j.tcs.2018.01.021}, abstract = {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\). It~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 for a concrete floor-heating system with 11~rooms and up to \(2^{11}=2048\) switching modes.}, } |

[BBF+18] | Giovanni Bacci,
Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen,
Nicolas Markey, and
Pierre-Alain Reynier.
Optimal and Robust Controller Synthesis Using Energy
Timed Automata with Uncertainty.
In FM'18,
Lecture Notes in Computer Science 10951, pages 203-221. Springer-Verlag, July 2018.
- Abstract
In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.
@inproceedings{fm2018-BBFLMR, author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim Guldstrand and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty}, editor = {Havelund, Klaus and Peleska, Jan and Roscoe, Bill W. and de Vink, Erik}, booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {F}ormal {M}ethods ({FM}'18)}, acronym = {{FM}'18}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {10951}, pages = {203-221}, year = {2018}, month = jul, doi = {10.1007/978-3-319-95582-7_12}, award = {Array}, abstract = {In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.}, } |

[BBM18] | A. R. Balasubramanian,
Nathalie Bertrand, and
Nicolas Markey.
Parameterized verification of synchronization in
constrained reconfigurable broadcast networks.
In TACAS'18 (Part II),
Lecture Notes in Computer Science 10806, pages 38-54. Springer-Verlag, April 2018.
- Abstract
Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the *synchronization property*, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks).In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents.
@inproceedings{tacas2018-2-BBM, author = {Balasubramanian, A. R. and Bertrand, Nathalie and Markey, Nicolas}, title = {Parameterized verification of synchronization in constrained reconfigurable broadcast networks}, editor = {Beyer, Dirk and Huisman, Marieke}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'18)~-- {P}art~{II}}, acronym = {{TACAS}'18 (Part~{II})}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {10806}, pages = {38-54}, year = {2018}, month = apr, doi = {10.1007/978-3-319-89963-3_3}, abstract = {Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We~focus here on the \emph{synchronization property}, asking whether all agents converge to a set of target states after some execution. This~problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while~it~is undecidable for static broadcast networks).\par In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In~particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on~the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents.}, } |

[BGM+18] | Patricia Bouyer,
Mauricio González,
Nicolas Markey, and
Mickael Randour.
Multi-weighted Markov Decision Processes with
Reachability Objectives.
In GandALF'18,
Electronic Proceedings in Theoretical Computer
Science 277, pages 250-264. September 2018.
- Abstract
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{gandalf2018-BGMR, author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and Markey, Nicolas and Randour, Mickael}, title = {Multi-weighted Markov Decision Processes with Reachability Objectives}, editor = {Orlandini, Andrea and Zimmermann, Martin}, booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics and {F}ormal {V}erification ({GandALF}'18)}, acronym = {{GandALF}'18}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {277}, pages = {250-264}, year = {2018}, month = sep, doi = {10.4204/EPTCS.277.18}, abstract = {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.}, } |

[BJM18] | Patricia Bouyer,
Samy Jaziri, and
Nicolas Markey.
Efficient timed diagnosis using automata with timed
domains.
In RV'18,
Lecture Notes in Computer Science 11237, pages 205-221. Springer-Verlag, November 2018.
- Abstract
We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed autmata, 2002].
@inproceedings{rv2018-BJM, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {Efficient timed diagnosis using automata with timed domains}, editor = {Colombo, Christian and Leucker, Martin}, booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on {R}untime {V}erification ({RV}'18)}, acronym = {{RV}'18}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {11237}, pages = {205-221}, year = {2018}, month = nov, doi = {10.1007/978-3-030-03769-7_12}, abstract = {We consider the problems of efficiently diagnosing and predicting what did (or~will) happen in a partially-observable one-clock timed automaton. We~introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We~report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed autmata,~2002].}, } |

[GBM18] | Patrick Gardy,
Patricia Bouyer, and
Nicolas Markey.
Dependences in Strategy Logic.
In STACS'18,
Leibniz International Proceedings in Informatics 96, pages 34:1-34:14. Leibniz-Zentrum für Informatik, February 2018.
- Abstract
Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on *strategy dependences*in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero*et al.*, Reasoning about strategies: On the model-checking problem, 2014]. We explain why*elementary*dependences, as defined by Mogavero*et al.*, do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing*timeline*dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics.
@inproceedings{stacs2018-GBM, author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas}, title = {Dependences in Strategy Logic}, editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte}, booktitle = {{P}roceedings of the 35th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'18)}, acronym = {{STACS}'18}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {96}, pages = {34:1-34:14}, year = {2018}, month = feb, doi = {10.4230/LIPIcs.STACS.2018.34}, abstract = {Strategy Logic~(\textsf{SL}) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in~\textsf{SL}, one can quantify over strategies, assign them to agents, and express \textsf{LTL} properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking \textsf{SL} has non-elementary complexity; second, the exact semantics of \textsf{SL} is rather intricate, and may not correspond to what is expected. In~this paper, we~focus on \emph{strategy dependences} in~\textsf{SL}, by tracking how existentially-quantified strategies in a formula may (or~may~not) depend on other strategies selected in the formula, revisiting the approach of~[Mogavero \emph{et~al.}, Reasoning about strategies: On~the model-checking problem,~2014]. We~explain why \emph{elementary} dependences, as defined by Mogavero~\emph{et~al.}, do not exactly capture the intended concept of behavioral strategies. We~address this discrepancy by introducing \emph{timeline} dependences, and exhibit a large fragment of \textsf{SL} for which model checking can be performed in \textsf{2EXPTIME} under this new semantics.}, } |

[HJM18] | Léo Henry,
Thierry Jéron, and
Nicolas Markey.
Control strategies for off-line testing of timed
systems.
In SPIN'18,
Lecture Notes in Computer Science 10869, pages 171-189. Springer-Verlag, June 2018.
- Abstract
Partial observability and controllability are two well-known issues in test-case synthesis for interactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. Building on the tioco timed testing framework, we extend a previous game interpretation of the test-synthesis problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that tries to minimize both control losses and distance to the satisfaction of a test purpose, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method.
@inproceedings{spin2018-HJM, author = {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey, Nicolas}, title = {Control strategies for off-line testing of timed systems}, editor = {Gallardo, Mar{\'\i}a-del-Mar and Merino, Pedro}, booktitle = {{P}roceedings of the 25th {I}nternational {S}ymposium on {M}odel-{C}herking {S}oftware ({SPIN}'18)}, acronym = {{SPIN}'18}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {10869}, pages = {171-189}, year = {2018}, month = jun, doi = {10.1007/978-3-319-94111-0_10}, abstract = {Partial observability and controllability are two well-known issues in test-case synthesis for interactive systems. We~address the problem of partial control in the synthesis of test cases from timed-automata specifications. Building on the tioco timed testing framework, we~extend a previous game interpretation of the test-synthesis problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We~exhibit strategies of a game that tries to minimize both control losses and distance to the satisfaction of a test purpose, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method.}, } |

[BFL+18] | Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen,
Nicolas Markey,
Joël Ouaknine, and
James Worrell.
Model Checking Real-Time Systems.
In Edmund M. Clarke,
Thomas A. Henzinger,
Helmut Veith, and
Roderick Bloem (eds.),
Handbook of Model Checking.
Springer-Verlag, May 2018.
- Abstract
This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).
@incollection{hmc2018-BFLMOW, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim Guldstrand and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Model Checking Real-Time Systems}, editor = {Clarke, Edmund M. and Henzinger, Thomas A. and Veith, Helmut and Bloem, Roderick}, booktitle = {Handbook of Model Checking}, publisher = {Springer-Verlag}, pages = {1001-1046}, chapter = {29}, year = {2018}, month = may, doi = {10.1007/978-3-319-10575-8_29}, abstract = {This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).}, } |

2017 | |

[BMP+17] | Patricia Bouyer,
Nicolas Markey,
Nicolas Perrin, and
Philipp Schlehuber-Caissier.
Timed automata abstraction of switched dynamical
systems using control funnels.
Real-Time Systems 53(3):327-353. Kluwer Academic, May 2017.
- Abstract
The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We demonstrate the potential of our approach with three examples.
@article{rts53(3)-BMPS, author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas and Schlehuber{-}Caissier, Philipp}, title = {Timed automata abstraction of switched dynamical systems using control funnels}, publisher = {Kluwer Academic}, journal = {Real-Time Systems}, volume = {53}, number = {3}, pages = {327-353}, year = {2017}, month = may, doi = {10.1007/s11241-016-9262-3}, abstract = {The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The~main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We~demonstrate the potential of our approach with three examples.}, } |

[BMV17] | Patricia Bouyer,
Nicolas Markey, and
Steen Vester.
Nash Equilibria in Symmetric Graph Games with
Partial Observation.
Information and Computation 254(2):238-258. Elsevier, June 2017.
- Abstract
We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.
@article{icomp254()-BMV, author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen}, title = {{N}ash Equilibria in Symmetric Graph Games with Partial Observation}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {254}, number = {2}, pages = {238-258}, year = {2017}, month = jun, doi = {10.1016/j.ic.2016.10.010}, abstract = {We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.}, } |

[BHM+17] | Patricia Bouyer,
Piotr Hofman,
Nicolas Markey,
Mickael Randour, and
Martin Zimmermann.
Bounding Average-energy Games.
In FoSSaCS'17,
Lecture Notes in Computer Science 10203, pages 179-195. Springer-Verlag, April 2017.
- Abstract
We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies. By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem. Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.
@inproceedings{fossacs2017-BHMRZ, author = {Bouyer, Patricia and Hofman, Piotr and Markey, Nicolas and Randour, Mickael and Zimmermann, Martin}, title = {Bounding Average-energy Games}, editor = {Esparza, Javier and Murawski, Andrzej}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'17)}, acronym = {{FoSSaCS}'17}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {10203}, pages = {179-195}, year = {2017}, month = apr, doi = {10.1007/978-3-662-54458-7_11}, abstract = {We~consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but~no upper bound) is an open problem; in~particular, there is no known upper bound on the memory that is required for winning strategies.\par By~reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we~show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We~also prove EXPSPACE-hardness of this problem.\par Finally, we~consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.}, } |

[BJM17] | Patricia Bouyer,
Samy Jaziri, and
Nicolas Markey.
On the determinization of timed systems.
In FORMATS'17,
Lecture Notes in Computer Science 10419, pages 25-41. Springer-Verlag, September 2017.
- Abstract
We introduce a new formalism called *automata over a timed domain*which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.
@inproceedings{formats2017-BJM, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {On the determinization of timed systems}, editor = {Abate, Alessandro and Geeraerts, Gilles}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'17)}, acronym = {{FORMATS}'17}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {10419}, pages = {25-41}, year = {2017}, month = sep, doi = {10.1007/978-3-319-65765-3_2}, abstract = {We introduce a new formalism called \emph{automata over a timed domain} which provides an adequate framework for the determinization of timed systems. In~this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We~give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.}, } |

[Mar17] | Nicolas Markey.
Temporal logics for multi-agent systems
(invited talk).
In MFCS'17,
Leibniz International Proceedings in Informatics 84, pages 84:1-84:3. Leibniz-Zentrum für Informatik, August 2017.
@inproceedings{mfcs2017-Mar, author = {Markey, Nicolas}, title = {Temporal logics for multi-agent systems (invited~talk)}, editor = {Larsen, Kim Guldstrand and Bodlaender, Hans L. and Raskin, Jean-Fran{\c c}ois}, booktitle = {{P}roceedings of the 42nd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'17)}, acronym = {{MFCS}'17}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {84}, pages = {84:1-84:3}, year = {2017}, month = aug, doi = {10.4230/LIPIcs.MFCS.2017.84}, } |

[BLM+17] | Patricia Bouyer,
François Laroussinie,
Nicolas Markey,
Joël Ouaknine, and
James Worrell.
Timed temporal logics.
In Luca Aceto,
Giorgio Bacci,
Giovanni Bacci,
Anna Ingólfsdóttir,
Axel Legay, and
Radu Mardare (eds.),
Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday,
Lecture Notes in Computer Science 10460, pages 211-230. Springer-Verlag, August 2017.
- Abstract
Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.
@incollection{kimfest2017-BLMOW, author = {Bouyer, Patricia and Laroussinie, Fran{\c c}ois and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Timed temporal logics}, editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and Mardare, Radu}, booktitle = {Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {10460}, pages = {211-230}, year = {2017}, month = aug, doi = {10.1007/978-3-319-63121-9_11}, abstract = {Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.}, } |

[BJM17] | Patricia Bouyer,
Vincent Jugé, and
Nicolas Markey.
Courcelle's Theorem Made Dynamic.
Technical Report 1702.05183, arXiv,
February 2017.
- Abstract
Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of model checking a fixed monadic second-order formula over evolving subgraphs of a fixed maximal graph having bounded tree-width; here the subgraph evolves by losing or gaining edges (from the maximal graph). We show that this problem is in DynFO (with LOGSPACE precomputation), via a reduction to a Dyck reachability problem on an acyclic automaton.
@techreport{arxiv1702.05183-BJM, author = {Bouyer, Patricia and Jug{\'e}, Vincent and Markey, Nicolas}, title = {{C}ourcelle's Theorem Made Dynamic}, number = {1702.05183}, year = {2017}, month = feb, institution = {arXiv}, abstract = {Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of model checking a fixed monadic second-order formula over evolving subgraphs of a fixed maximal graph having bounded tree-width; here the subgraph evolves by losing or gaining edges (from the maximal graph). We~show that this problem is in DynFO (with LOGSPACE precomputation), via a reduction to a Dyck reachability problem on an acyclic automaton.}, } |

[GBB+17] | Mauricio González,
Olivier Beaude,
Patricia Bouyer,
Samson Lasaulce, and
Nicolas Markey.
Stratégies d'ordonnancement de consommation
d'énergie en présence d'information
imparfaite de prévision.
In GRETSI'17.
September 2017.
- Abstract
Energy consumption problems (e.g., electric vehicles charging) are very related to communication problems. The "water-filling" algorithm can be used, but it is not robust w.r.t. the noise of the "non-flexible", i.e. not-controllable, energy consumption forecasting. We propose a robust algorithm using the probabilistic model-checker PRISM, to exploit the idea of discretizing the consumption action (as for a modulation to small constellation) and the dynamic structure of the problem in a Markov-decision-process model.
@inproceedings{gretsi2017-GBBLM, author = {Gonz{\'a}lez, Mauricio and Beaude, Olivier and Bouyer, Patricia and Lasaulce, Samson and Markey, Nicolas}, title = {Strat{\'e}gies d'ordonnancement de consommation d'{\'e}nergie en pr{\'e}sence d'information imparfaite de pr{\'e}vision}, booktitle = {{A}ctes du 26{\`e}me {C}olloque du {G}roupe d'{\'E}tudes du {T}raitement du {S}ignal et des {I}mages ({GRETSI}'17)}, acronym = {{GRETSI}'17}, year = {2017}, month = sep, abstract = {Energy consumption problems (e.g., electric vehicles charging) are very related to communication problems. The "water-filling" algorithm can be used, but it is not robust w.r.t. the noise of the "non-flexible", i.e. not-controllable, energy consumption forecasting. We~propose a robust algorithm using the probabilistic model-checker PRISM, to exploit the idea of discretizing the consumption action (as~for a modulation to small constellation) and the dynamic structure of the problem in a Markov-decision-process model.}, } |

2016 | |

[BGM16] | Patricia Bouyer,
Patrick Gardy, and
Nicolas Markey.
On the semantics of Strategy Logic.
Information Processing Letters 116(2):75-79. Elsevier, February 2016.
- Abstract
We define and study a slight variation on the semantics of Strategy Logic: while in the classical semantics, all strategies are shifted during the evaluation of temporal modalities, we propose to only shift the strategies that have been assigned to a player, thus matching the intuition that we can assign the very same strategy to the players at different points in time. We prove that surprisingly, this renders the model-checking problem undecidable.
@article{ipl116(2)-BGM, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {On the semantics of Strategy Logic}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {116}, number = {2}, pages = {75-79}, year = {2016}, month = feb, doi = {10.1016/j.ipl.2015.10.004}, abstract = {We define and study a slight variation on the semantics of Strategy Logic: while in the classical semantics, all strategies are shifted during the evaluation of temporal modalities, we propose to only shift the strategies that have been assigned to a player, thus matching the intuition that we can assign the very same strategy to the players at different points in time. We prove that surprisingly, this renders the model-checking problem undecidable.}, } |

[BCM16] | Patricia Bouyer,
Maximilien Colange, and
Nicolas Markey.
Symbolic Optimal Reachability in Weighted Timed
Automata.
In CAV'16,
Lecture Notes in Computer Science 9779, pages 513-530. Springer-Verlag, July 2016.
- Abstract
Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.
@inproceedings{cav2016-BCM, author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas}, title = {Symbolic Optimal Reachability in Weighted Timed Automata}, editor = {Chaudhuri, Swarat and Farzan, Azadeh}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'16)}, acronym = {{CAV}'16}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {9779}, pages = {513-530}, year = {2016}, month = jul, doi = {10.1007/978-3-319-41528-4_28}, url = {http://arxiv.org/abs/1602.00481}, abstract = {Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.}, } |

[BMR+16] | Patricia Bouyer,
Nicolas Markey,
Mickael Randour,
Arnaud Sangnier, and
Daniel Stan.
Reachability in Networks of Register Protocols under
Stochastic Schedulers.
In ICALP'16,
Leibniz International Proceedings in Informatics 55, pages 106:1-106:14. Leibniz-Zentrum für Informatik, July 2016.
- Abstract
We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called *processes*) of the same automaton (called*protocol*), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property : the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
@inproceedings{icalp2016-BMRSS, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Sangnier, Arnaud and Stan, Daniel}, title = {Reachability in Networks of Register Protocols under Stochastic Schedulers}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)~-- Part~{II}}, acronym = {{ICALP}'16}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {55}, pages = {106:1-106:14}, year = {2016}, month = jul, doi = {10.4230/LIPIcs.ICALP.2016.106}, abstract = {We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of~\(N\) copies (called \emph{processes}) of the same automaton (called \emph{protocol}), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number~\(N\) of processes. However, we prove that our setting has a cut-off property : the answer to the almost-sure reachability problem is constant when \(N\) is large enough; we~then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.}, } |

[BMS16] | Patricia Bouyer,
Nicolas Markey, and
Daniel Stan.
Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games.
In GandALF'16,
Electronic Proceedings in Theoretical Computer
Science 226, pages 61-75. September 2016.
- Abstract
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.
@inproceedings{gandalf2016-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel}, title = {Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games}, editor = {Cantone, Domenico and Delzanno, Giorgio}, booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics and {F}ormal {V}erification ({GandALF}'16)}, acronym = {{GandALF}'16}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {226}, pages = {61-75}, year = {2016}, month = sep, doi = {10.4204/EPTCS.226.5}, abstract = {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.}, } |

[DLM16] | Amélie David,
François Laroussinie, and
Nicolas Markey.
On the expressiveness of QCTL.
In CONCUR'16,
Leibniz International Proceedings in Informatics 59, pages 28:1-28:15. Leibniz-Zentrum für Informatik, August 2016.
- Abstract
QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTLk, with at most k nested blocks of quantifiers, is k+1-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the *distinguishing power*of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their*expressive power*(i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QCTLk collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
@inproceedings{concur2016-DLM, author = {David, Am{\'e}lie and Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {On~the expressiveness of~{QCTL}}, editor = {Desharnais, Jules and Jagadeesan, Radha}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, acronym = {{CONCUR}'16}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {59}, pages = {28:1-28:15}, year = {2016}, month = aug, doi = {10.4230/LIPIcs.CONCUR.2016.28}, abstract = {QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTL\textsuperscript{\(k\)}, with at most \(k\) nested blocks of quantifiers, is \(k+1\)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We~address such expressiveness questions in this paper. We first consider the \emph{distinguishing power} of these logics (i.e.,~their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their \emph{expressive power} (i.e.,~their ability to express a property), showing that in terms of expressiveness the hierarchy QCTL\textsuperscript{\(k\)} collapses at level~2 (in~other terms, any~QCTL formula can be expressed using at most two nested blocks of quantifiers).}, } |

[FKM16] | Laurent Fribourg,
Ulrich Kühne, and
Nicolas Markey.
Game-based Synthesis of Distributed Controllers for
Sampled Switched Systems.
In SynCoP'15,
OpenAccess Series in Informatics 44, pages 47-61. Leibniz-Zentrum für Informatik, April 2016.
- Abstract
Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with each other and with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In this paper, we consider a controller synthesis method based on state space decomposition, and propose a game-based approach in order to extend it within a distributed framework.
@inproceedings{syncop2015-FKM, author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey, Nicolas}, title = {Game-based Synthesis of Distributed Controllers for Sampled Switched Systems}, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'15)}, acronym = {{S}yn{C}o{P}'15}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {OpenAccess Series in Informatics}, volume = {44}, pages = {47-61}, year = {2016}, month = apr, doi = {10.4230/OASIcs.SynCoP.2015.48}, abstract = {Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with each other and with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In~this paper, we~consider a controller synthesis method based on state space decomposition, and propose a game-based approach in order to extend it within a distributed framework.}, } |

[LFM+16] | Adrien Le Coënt,
Laurent Fribourg,
Nicolas Markey,
Florian De Vuyst, and
Ludovic Chamoin.
Distributed Synthesis of State-Dependent Switching
Control.
In RP'16,
Lecture Notes in Computer Science 9899, pages 119-133. Springer-Verlag, September 2016.
- Abstract
We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting at R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 211 = 2048 switching modes.
@inproceedings{rp2016-LFMDC, author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and Markey, Nicolas and De{~}Vuyst, Florian and Chamoin, Ludovic}, title = {Distributed Synthesis of State-Dependent Switching Control}, editor = {Larsen, Kim Guldstrand and Srba, Ji{\v r}{\'\i}}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, acronym = {{RP}'16}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {9899}, pages = {119-133}, year = {2016}, month = sep, doi = {10.1007/978-3-319-45994-3_9}, abstract = {We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region~\(R\) of the state space, the method builds a capture set~\(S\) and a control which steers any element of~\(S\) into~\(R\). The method works by iterated backward reachability from~\(R\). More precisely, \(S\)~is given as a parametric extension of~\(R\), and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within~\(R\) all the states starting at~\(R\). We~explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and \(2^{11} = 2048\) switching modes.}, } |

[BDJ+16] | Thomas Brihaye,
Benoît Delahaye,
Loïg Jezequel,
Nicolas Markey, and
Jiří Srba (eds.)
Proceedings of the Cassting Workshop on Games
for the Synthesis of Complex Systems
(Cassting'16) and of the 3rd International
Workshop on Synthesis of Complex Parameters
(SynCoP'16).
Electronic Proceedings in Theoretical Computer
Science 220.
July 2016.
@proceedings{cassting-syncop2016-DJMS, title = {{P}roceedings of the {C}assting Workshop on {G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16) and of the 3rd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)}, editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t and Jezequel, Lo{\"\i}g and Markey, Nicolas and Srba, Ji{\v r}{\'\i}}, booktitle = {{P}roceedings of the {C}assting Workshop on {G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16) and of the 3rd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)}, acronym = {{C}assting{{\slash}}{S}yn{C}o{P}'16}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {220}, year = {2016}, month = jul, confyear = {2016}, confmonth = {4}, doi = {10.4204/EPTCS.220}, url = {http://eptcs.web.cse.unsw.edu.au/ content.cgi?CASSTINGSynCoP2016}, } |

[FM16] | Martin Fränzle and
Nicolas Markey (eds.)
Proceedings of the 14th International
Conferences on Formal Modelling and Analysis
of Timed Systems (FORMATS'16).
Lecture Notes in Computer Science 9884.
Springer-Verlag, August 2016.
@proceedings{formats2016-FM, title = {{P}roceedings of the 14th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'16)}, editor = {Fr{\"a}nzle, Martin and Markey, Nicolas}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'16)}, acronym = {{FORMATS}'16}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {9884}, year = {2016}, month = aug, doi = {10.1007/978-3-319-44878-7}, url = {http://link.springer.com/book/10.1007/978-3-319-44878-7}, } |

2015 | |

[BBM+15] | Patricia Bouyer,
Romain Brenguier,
Nicolas Markey, and
Michael Ummels.
Pure Nash Equilibria in Concurrent Games.
Logical Methods in Computer Science 11(2:9).
June 2015.
- Abstract
We study pure-strategy Nash equilibria in multiplayer concurrent games, for a variety of omega-regular objectives. For simple objectives (e.g. reachability, Büchi objectives), we transform the problem of deciding the existence of a Nash equilibrium in a given concurrent game into that of deciding the existence of a winning strategy in a turn-based two-player game (with a refined objective). We use that transformation to design algorithms for computing Nash equilibria, which in most cases have optimal worst-case complexity. For automata-defined objectives, we extend the above algorithms using a simulation relation which allows us to consider the product of the game with the automata defining the objectives. Building on previous algorithms for simple qualitative objectives, we define and study a semi-quantitative framework, where all players have several boolean objectives equipped with a preorder; a player may for instance want to satisfy all her objectives, or to maximise the number of objectives that she achieves. In most cases, we prove that the algorithms we obtain match the complexity of the problem they address.
@article{lmcs11(2)-BBMU, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {Pure {N}ash Equilibria in Concurrent Games}, journal = {Logical Methods in Computer Science}, volume = {11}, number = {2:9}, year = {2015}, month = jun, doi = {10.2168/LMCS-11(2:9)2015}, abstract = {We study pure-strategy Nash equilibria in multiplayer concurrent games, for a variety of omega-regular objectives. For simple objectives (e.g. reachability, B{\"u}chi objectives), we transform the problem of deciding the existence of a Nash equilibrium in a given concurrent game into that of deciding the existence of a winning strategy in a turn-based two-player game (with a refined objective). We use that transformation to design algorithms for computing Nash equilibria, which in most cases have optimal worst-case complexity. For automata-defined objectives, we extend the above algorithms using a simulation relation which allows us to consider the product of the game with the automata defining the objectives. Building on previous algorithms for simple qualitative objectives, we define and study a semi-quantitative framework, where all players have several boolean objectives equipped with a preorder; a player may for instance want to satisfy all her objectives, or to maximise the number of objectives that she achieves. In most cases, we prove that the algorithms we obtain match the complexity of the problem they address.}, } |

[BMS15] | Patricia Bouyer,
Nicolas Markey, and
Ocan Sankur.
Robust Reachability in Timed Automata and Games:
A Game-based Approach.
Theoretical Computer Science 563:43-74. Elsevier, January 2015.
- Abstract
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.
@article{tcs563()-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Reachability in Timed Automata and Games: A~Game-based Approach}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {563}, pages = {43-74}, year = {2015}, month = jan, doi = {10.1016/j.tcs.2014.08.014}, abstract = {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.}, } |

[LM15] | François Laroussinie and
Nicolas Markey.
Augmenting ATL with strategy contexts.
Information and Computation 245:98-123. Elsevier, December 2015.
- Abstract
We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies. We show that our extension ATLsc is very expressive, but that its decision problems are quite hard: model checking is k-EXPTIME-complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.
@article{icomp245()-LM, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {Augmenting {ATL} with strategy contexts}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {245}, pages = {98-123}, year = {2015}, month = dec, doi = {10.1016/j.ic.2014.12.020}, abstract = {We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies.\par We show that our extension ATLsc is very expressive, but that its decision problems are quite hard: model checking is \(k\)-EXPTIME-complete when the formula has \(k\) nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the~computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.}, } |

[AM15] | Étienne André and
Nicolas Markey.
Language Preservation Problems in Parametric Timed
Automata.
In FORMATS'15,
Lecture Notes in Computer Science 9268, pages 27-43. Springer-Verlag, September 2015.
- Abstract
Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.
@inproceedings{formats2015-AM, author = {Andr{\'e}, {\'E}tienne and Markey, Nicolas}, title = {Language Preservation Problems in Parametric Timed Automata}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'15)}, acronym = {{FORMATS}'15}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {9268}, pages = {27-43}, year = {2015}, month = sep, doi = {10.1007/978-3-319-22975-1_3}, abstract = {Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.}, } |

[BFM15] | Patricia Bouyer,
Erwin Fang, and
Nicolas Markey.
Permissive strategies in timed automata and games.
In AVOCS'15,
Electronic Communications of the EASST 72.
European Association of Software Science and
Technology, September 2015.
- Abstract
Timed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now very well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have recently been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a new approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies return an interval of possible dates when to play the selected action. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata.
@inproceedings{avocs2015-BFM, author = {Bouyer, Patricia and Fang, Erwin and Markey, Nicolas}, title = {Permissive strategies in timed automata and games}, editor = {Grov, Gudmund and Ireland, Andrew}, booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVOCS}'15)}, acronym = {{AVOCS}'15}, publisher = {European Association of Software Science and Technology}, series = {Electronic Communications of the EASST}, volume = {72}, year = {2015}, month = sep, doi = {10.14279/tuj.eceasst.72.1015}, abstract = {Timed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now very well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have recently been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a new approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies return an interval of possible dates when to play the selected action. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata.}, } |

[BGM15] | Patricia Bouyer,
Patrick Gardy, and
Nicolas Markey.
Weighted strategy logic with boolean goals over
one-counter games.
In FSTTCS'15,
Leibniz International Proceedings in Informatics 45, pages 69-83. Leibniz-Zentrum für Informatik, December 2015.
- Abstract
Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero *et al.*Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.
@inproceedings{fsttcs2015-BGM, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {Weighted strategy logic with boolean goals over one-counter games}, editor = {Harsha, Prahladh and Ramalingam, G.}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, acronym = {{FSTTCS}'15}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {45}, pages = {69-83}, year = {2015}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2015.69}, abstract = {Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero \emph{et~al.} Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.}, } |

[BJM15] | Patricia Bouyer,
Samy Jaziri, and
Nicolas Markey.
On the Value Problem in Weighted Timed Games.
In CONCUR'15,
Leibniz International Proceedings in Informatics 42, pages 311-324. Leibniz-Zentrum für Informatik, September 2015.
- Abstract
A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the cost for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal cost and almost-optimal strategies can be computed. In this paper, we show that the value problem is undecidable in general weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. We then provide an algorithm to compute arbitrary approximations of the value in a game, and almost-optimal strategies. The algorithm applies in a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.
@inproceedings{concur2015-BJM, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {On~the Value Problem in Weighted Timed Games}, editor = {Aceto, Luca and de Frutos{-}Escrig, David}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'15)}, acronym = {{CONCUR}'15}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {42}, pages = {311-324}, year = {2015}, month = sep, doi = {10.4230/LIPIcs.CONCUR.2015.311}, abstract = {A~weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the cost for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal cost and almost-optimal strategies can be computed.\par In this paper, we show that the value problem is undecidable in general weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. We then provide an algorithm to compute arbitrary approximations of the value in a game, and almost-optimal strategies. The algorithm applies in a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.}, } |

[BMP+15] | Patricia Bouyer,
Nicolas Markey,
Nicolas Perrin, and
Philipp Schlehuber-Caissier.
Timed automata abstraction of switched dynamical
systems using control funnels.
In FORMATS'15,
Lecture Notes in Computer Science 9268, pages 60-75. Springer-Verlag, September 2015.
- Abstract
The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (the *control funnels*), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We demonstrate the potential of our approach with two examples.
@inproceedings{formats2015-BMPS, author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas and Schlehuber{-}Caissier, Philipp}, title = {Timed automata abstraction of switched dynamical systems using control funnels}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'15)}, acronym = {{FORMATS}'15}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {9268}, pages = {60-75}, year = {2015}, month = sep, doi = {10.1007/978-3-319-22975-1_5}, abstract = {The~development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we~propose a new abstraction, based on time-varying regions of invariance (the~\emph{control funnels}), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We~demonstrate the potential of our approach with two examples.}, } |

[BMR+15] | Patricia Bouyer,
Nicolas Markey,
Mickael Randour,
Kim Guldstrand Larsen, and
Simon Laursen.
Average-energy games.
In GandALF'15,
Electronic Proceedings in Theoretical Computer
Science 193, pages 1-15. September 2015.
- Abstract
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.
@inproceedings{gandalf2015-BMRLL, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim Guldstrand and Laursen, Simon}, title = {Average-energy games}, editor = {Esparza, Javier and Tronci, Enrico}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics and {F}ormal {V}erification ({GandALF}'15)}, acronym = {{GandALF}'15}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {193}, pages = {1-15}, year = {2015}, month = sep, doi = {10.4204/EPTCS.193.1}, abstract = {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.\par We study \emph{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 \textsf{NP}{{\(\cap\)}}\textsf{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.}, } |

[LMS15] | François Laroussinie,
Nicolas Markey, and
Arnaud Sangnier.
ATLsc with partial
observation.
In GandALF'15,
Electronic Proceedings in Theoretical Computer
Science 193, pages 43-57. September 2015.
- Abstract
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.
@inproceedings{gandalf2015-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Sangnier, Arnaud}, title = {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial observation}, editor = {Esparza, Javier and Tronci, Enrico}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics and {F}ormal {V}erification ({GandALF}'15)}, acronym = {{GandALF}'15}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {193}, pages = {43-57}, year = {2015}, month = sep, doi = {10.4204/EPTCS.193.4}, abstract = {Alternating-time temporal logic with strategy contexts ({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a powerful formalism for expressing properties of multi-agent systems: it~extends \textsf{CTL} with \emph{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 \emph{uniform} incomplete observation (where all players have the same observation) preserves decidability of the model checking problem, even for very expressive logics such as {{\(\textsf{ATL}_{\textsf{sc}}\)}}.}, } |

[CLM+15] | Krishnendu Chatterjee,
Stéphane Lafortune,
Nicolas Markey, and
Wolfgang Thomas (eds.)
Non-Zero-Sum-Games and Control (Dagstuhl
Seminar 15061).
Dagstuhl Reports 5(2):1-25. Leibniz-Zentrum für Informatik, June 2015.
- Abstract
In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and—as a special focus—connections with control engineering (supervisory control).
@proceedings{dagrep5(2)-CLMT, title = {Non-Zero-Sum-Games and Control ({D}agstuhl Seminar~15061)}, editor = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and Markey, Nicolas and Thomas, Wolfgang}, booktitle = {Non-Zero-Sum-Games and Control ({D}agstuhl Seminar~15061)}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, journal = {Dagstuhl Reports}, volume = {5}, number = {2}, pages = {1-25}, year = {2015}, month = jun, doi = {10.4230/DagRep.5.2.1}, url = {http://drops.dagstuhl.de/opus/volltexte/2015/5042}, abstract = {In this report, the program, research issues, and results of Dagstuhl Seminar~15061 {"}Non-Zero-Sum-Games and Control{"} are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and---as~a special focus---connections with control engineering (supervisory control).}, } |

2014 | |

[BLM14] | Patricia Bouyer,
Kim Guldstrand Larsen, and
Nicolas Markey.
Lower-Bound Constrained Runs in Weighted Timed
Automata.
Performance Evaluation 73:91-109. Elsevier, March 2014.
- Abstract
We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-constrained run is–for us somewhat unexpectedly–undecidable for weighted timed automata with four or more clocks. This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE. Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).
@article{peva73()-BLM, author = {Bouyer, Patricia and Larsen, Kim Guldstrand and Markey, Nicolas}, title = {Lower-Bound Constrained Runs in Weighted Timed Automata}, publisher = {Elsevier}, journal = {Performance Evaluation}, volume = {73}, pages = {91-109}, year = {2014}, month = mar, doi = {10.1016/j.peva.2013.11.002}, abstract = {We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-constrained run is--for us somewhat unexpectedly--undecidable for weighted timed automata with four or more clocks.\par This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.\par Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in~PSPACE).}, } |

[LM14] | François Laroussinie and
Nicolas Markey.
Quantified CTL: expressiveness and complexity.
Logical Methods in Computer Science 10(4).
December 2014.
- Abstract
While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).
@article{lmcs10(4)-LM, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {Quantified~{CTL}: expressiveness and complexity}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {4}, year = {2014}, month = dec, doi = {10.2168/LMCS-10(4:17)2014}, abstract = {While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we~study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).}, } |

[SBM14] | Ocan Sankur,
Patricia Bouyer, and
Nicolas Markey.
Shrinking Timed Automata.
Information and Computation 234:107-132. Elsevier, February 2014.
- Abstract
We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce *parametric shrinking*of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.
@article{icomp234()-SBM, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas}, title = {Shrinking Timed Automata}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {234}, pages = {107-132}, year = {2014}, month = feb, doi = {10.1016/j.ic.2014.01.002}, abstract = {We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce \emph{parametric shrinking} of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.}, } |

[BGM14] | Patricia Bouyer,
Patrick Gardy, and
Nicolas Markey.
Quantitative verification of weighted Kripke
structures.
In ATVA'14,
Lecture Notes in Computer Science 8837, pages 64-80. Springer-Verlag, November 2014.
- Abstract
Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.
@inproceedings{atva2014-BGM, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {Quantitative verification of weighted {K}ripke structures}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, acronym = {{ATVA}'14}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {8837}, pages = {64-80}, year = {2014}, month = nov, doi = {10.1007/978-3-319-11936-6_6}, abstract = {Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.}, } |

[BMM14] | Patricia Bouyer,
Nicolas Markey, and
Raj Mohan Matteplackel.
Averaging in LTL.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 266-280. Springer-Verlag, September 2014.
- Abstract
For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean—either a property is true, or it is false. We believe that this is too crude in a context where quantitative information and constraints are crucial: correctness should be quantified! In a recent line of works, several authors have proposed quantitative semantics for temporal logics, using e.g. *discounting*modalities (which give less importance to distant events). In the present paper, we define and study a quantitative semantics of LTL with*averaging*modalities, either on the long run or within an until modality. This, in a way, relaxes the classical Boolean semantics of LTL, and provides a measure of certain properties of a model. We prove that computing and even approximating the value of a formula in this logic is undecidable.
@inproceedings{concur2014-BMM, author = {Bouyer, Patricia and Markey, Nicolas and Matteplackel, Raj~Mohan}, title = {Averaging in~{LTL}}, editor = {Baldan, Paolo and Gorla, Daniele}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, acronym = {{CONCUR}'14}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {8704}, pages = {266-280}, year = {2014}, month = sep, doi = {10.1007/978-3-662-44584-6_19}, abstract = {For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean---either a property is~true, or it~is false. We~believe that this is too crude in a context where quantitative information and constraints are crucial: correctness should be quantified!\par In a recent line of works, several authors have proposed quantitative semantics for temporal logics, using e.g. \emph{discounting} modalities (which give less importance to distant events). In~the present paper, we define and study a quantitative semantics of~LTL with \emph{averaging} modalities, either on the long run or within an until modality. This, in a way, relaxes the classical Boolean semantics of~LTL, and provides a measure of certain properties of a model. We~prove that computing and even approximating the value of a formula in this logic is undecidable.}, } |

[BMS14] | Patricia Bouyer,
Nicolas Markey, and
Daniel Stan.
Mixed Nash Equilibria in Concurrent Games.
In FSTTCS'14,
Leibniz International Proceedings in Informatics 29, pages 351-363. Leibniz-Zentrum für Informatik, December 2014.
- Abstract
We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i) the undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii) the undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.
@inproceedings{fsttcs2014-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel}, title = {Mixed {N}ash Equilibria in Concurrent Games}, editor = {Raman, Venkatesh and Suresh, S. P.}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, acronym = {{FSTTCS}'14}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {29}, pages = {351-363}, year = {2014}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2014.351}, abstract = {We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i)~the~undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii)~the~undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.}, } |

[BMV14] | Patricia Bouyer,
Nicolas Markey, and
Steen Vester.
Nash Equilibria in Symmetric Games with Partial
Observation.
In SR'14,
Electronic Proceedings in Theoretical Computer
Science 146, pages 49-55. March 2014.
- Abstract
We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.
@inproceedings{sr2014-BMV, author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen}, title = {Nash Equilibria in Symmetric Games with Partial Observation}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic {R}easoning ({SR}'14)}, acronym = {{SR}'14}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {146}, pages = {49-55}, year = {2014}, month = mar, doi = {10.4204/EPTCS.146.7}, abstract = {We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.}, } |

[DJL+14] | Laurent Doyen,
Line Juhl,
Kim Guldstrand Larsen,
Nicolas Markey, and
Mahsa Shirmohammadi.
Synchronizing words for weighted and timed automata.
In FSTTCS'14,
Leibniz International Proceedings in Informatics 29, pages 121-132. Leibniz-Zentrum für Informatik, December 2014.
- Abstract
The problem of synchronizing automata is concerned with the existence of a word that sends all states ofM the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete. In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.
@inproceedings{fsttcs2014-DJLMS, author = {Doyen, Laurent and Juhl, Line and Larsen, Kim Guldstrand and Markey, Nicolas and Shirmohammadi, Mahsa}, title = {Synchronizing words for weighted and timed automata}, editor = {Raman, Venkatesh and Suresh, S. P.}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, acronym = {{FSTTCS}'14}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {29}, pages = {121-132}, year = {2014}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2014.121}, abstract = {The problem of synchronizing automata is concerned with the existence of a word that sends all states ofM the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete.\par In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.}, } |

[MV14] | Nicolas Markey and
Steen Vester.
Symmetry Reduction in Infinite Games with Finite
Branching.
In ATVA'14,
Lecture Notes in Computer Science 8837, pages 281-296. Springer-Verlag, November 2014.
- Abstract
Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL*, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL*.
@inproceedings{atva2014-MV, author = {Markey, Nicolas and Vester, Steen}, title = {Symmetry Reduction in Infinite Games with Finite Branching}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, acronym = {{ATVA}'14}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {8837}, pages = {281-296}, year = {2014}, month = nov, doi = {10.1007/978-3-319-11936-6_21}, abstract = {Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL\textsuperscript{*}, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL\textsuperscript{*}.}, } |

[SLS+14] | Youcheng Sun,
Giuseppe Lipari,
Romain Soulat,
Laurent Fribourg, and
Nicolas Markey.
Component-Based Analysis of Hierarchical Scheduling
using Linear Hybrid Automata.
In RTCSA'14.
IEEE Comp. Soc. Press, August 2014.
- Abstract
Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns, etc. In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium size components.
@inproceedings{rtcsa2014-SLSFM, author = {Sun, Youcheng and Lipari, Giuseppe and Soulat, Romain and Fribourg, Laurent and Markey, Nicolas}, title = {Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {R}eal-{T}ime {C}omputing {S}ystems and {A}pplications ({RTCSA}'14)}, acronym = {{RTCSA}'14}, publisher = {IEEE Comp. Soc. Press}, year = {2014}, month = aug, doi = {10.1109/RTCSA.2014.6910502}, abstract = {Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns,~etc.\par In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a~component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium size components.}, } |

[Mar14] | Nicolas Markey.
Cassting: Synthesizing Complex Systems Using
Non-Zero-Sum Games.
ERCIM News 97:25-26. European Research Consortium for Informatics and
Mathematics, April 2014.
@article{ercimnews97-Mar, author = {Markey, Nicolas}, title = {Cassting: Synthesizing Complex Systems Using Non-Zero-Sum Games}, publisher = {European Research Consortium for Informatics and Mathematics}, journal = {ERCIM News}, volume = {97}, pages = {25-26}, year = {2014}, month = apr, url = {http://ercim-news.ercim.eu/en97/special/ cassting-synthesizing-complex-systems-using-non-zero-sum-games}, } |

2013 | |

[BMS13] | Patricia Bouyer,
Nicolas Markey, and
Ocan Sankur.
Robust Weighted Timed Automata and Games.
In FORMATS'13,
Lecture Notes in Computer Science 8053, pages 31-46. Springer-Verlag, August 2013.
- Abstract
Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.
@inproceedings{formats2013-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Weighted Timed Automata and Games}, editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'13)}, acronym = {{FORMATS}'13}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {8053}, pages = {31-46}, year = {2013}, month = aug, doi = {10.1007/978-3-642-40229-6_3}, abstract = {Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.}, } |

[LM13] | François Laroussinie and
Nicolas Markey.
Satisfiability of ATL with strategy contexts.
In GandALF'13,
Electronic Proceedings in Theoretical Computer
Science 119, pages 208-223. August 2013.
- Abstract
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.
@inproceedings{gandalf2013-LM, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {Satisfiability of {ATL} with strategy contexts}, editor = {Puppis, Gabriele and Villa, Tiziano}, booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics and {F}ormal {V}erification ({GandALF}'13)}, acronym = {{GandALF}'13}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {119}, pages = {208-223}, year = {2013}, month = aug, doi = {10.4204/EPTCS.119.18}, abstract = {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 \emph{strategy contexts}, while Strategy Logic has \emph{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.\par We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to \emph{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.}, } |

[SBM+13] | Ocan Sankur,
Patricia Bouyer,
Nicolas Markey, and
Pierre-Alain Reynier.
Robust Controller Synthesis in Timed Automata.
In CONCUR'13,
Lecture Notes in Computer Science 8052, pages 546-560. Springer-Verlag, August 2013.
- Abstract
We consider the fundamental problem of Büchi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.
@inproceedings{concur2013-SBMR, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Robust Controller Synthesis in Timed Automata}, editor = {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'13)}, acronym = {{CONCUR}'13}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {8052}, pages = {546-560}, year = {2013}, month = aug, doi = {10.1007/978-3-642-40184-8_38}, abstract = {We consider the fundamental problem of B{\"u}chi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.}, } |

[BMS13] | Patricia Bouyer,
Nicolas Markey, and
Ocan Sankur.
Robustness in timed automata.
In RP'13,
Lecture Notes in Computer Science 8169, pages 1-18. Springer-Verlag, September 2013.
- Abstract
In this paper we survey several approaches to the robustness of timed automata, that is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected. We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.
@inproceedings{rp2013-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robustness in timed automata}, editor = {Abdulla, Parosh Aziz and Potapov, Igor}, booktitle = {{P}roceedings of the 7th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)}, acronym = {{RP}'13}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {8169}, pages = {1-18}, year = {2013}, month = sep, doi = {10.1007/978-3-642-41036-9_1}, abstract = {In this paper we survey several approaches to the robustness of timed automata, that~is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected.\par We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.}, } |

2012 | |

[BMO+12] | Patricia Bouyer,
Nicolas Markey,
Joël Ouaknine,
Philippe Schnoebelen, and
James Worrell.
On Termination and Invariance for Faulty Channel
Systems.
Formal Aspects of Computing 24(4-6):595-607. Springer-Verlag, July 2012.
- Abstract
A *channel machine*consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines with*insertion errors*, i.e., machines in whose channels messages can spontaneously appear. We consider the invariance problem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.
@article{fac24(4-6)-BMOSW, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and Worrell, James}, title = {On Termination and Invariance for Faulty Channel Systems}, publisher = {Springer-Verlag}, journal = {Formal Aspects of Computing}, volume = {24}, number = {4-6}, pages = {595-607}, year = {2012}, month = jul, doi = {10.1007/s00165-012-0234-7}, abstract = {A~\emph{channel machine} consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines with \emph{insertion errors}, i.e., machines in whose channels messages can spontaneously appear. We consider the invariance problem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.}, } |

[BBM+12] | Patricia Bouyer,
Romain Brenguier,
Nicolas Markey, and
Michael Ummels.
Concurrent games with ordered objectives.
In FoSSaCS'12,
Lecture Notes in Computer Science 7213, pages 301-315. Springer-Verlag, March 2012.
- Abstract
We consider concurrent games played on graphs, in which each player has several qualitative (e.g. reachability or Büchi) objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled). We study two fundamental problems in that setting: (1) the *value problem*, which aims at deciding the existence of a strategy that ensures a given payoff; (2) the*Nash equilibrium problem*, where we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We characterise the exact complexities of these problems for several relevant preorders, and several kinds of objectives.
@inproceedings{fossacs2012-BBMU, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {Concurrent games with ordered objectives}, editor = {Birkedal, Lars}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'12)}, acronym = {{FoSSaCS}'12}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {7213}, pages = {301-315}, year = {2012}, month = mar, doi = {10.1007/978-3-642-28729-9_20}, abstract = {We consider concurrent games played on graphs, in which each player has several qualitative (e.g. reachability or B{\"u}chi) objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled).\par We study two fundamental problems in that setting: (1)~the \emph{value problem}, which aims at deciding the existence of a strategy that ensures a given payoff; (2)~the \emph{Nash equilibrium problem}, where we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We characterise the exact complexities of these problems for several relevant preorders, and several kinds of objectives.}, } |

[BLM12] | Patricia Bouyer,
Kim Guldstrand Larsen, and
Nicolas Markey.
Lower-Bound Constrained Runs in Weighted Timed
Automata.
In QEST'12,
pages 128-137.
IEEE Comp. Soc. Press, September 2012.
- Abstract
We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from [Bouyer *et al.*, "Infinite runs in weighted timed automata with energy constraints", FORMATS'08], we show that the existence of an infinite lower-bound-constrained run is—for us somewhat unexpectedly—undecidable for weighted timed automata with four or more clocks.This undecidability result assumes a fixed and know initial credit. We show that the related problem of existence of an initial credit for which there ex- ist a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. Finally, we prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.
@inproceedings{qest2012-BLM, author = {Bouyer, Patricia and Larsen, Kim Guldstrand and Markey, Nicolas}, title = {Lower-Bound Constrained Runs in Weighted Timed Automata}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'12)}, acronym = {{QEST}'12}, publisher = {IEEE Comp. Soc. Press}, pages = {128-137}, year = {2012}, month = sep, doi = {10.1109/QEST.2012.28}, abstract = {We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from [Bouyer \textit{et~al.}, {"}Infinite runs in weighted timed automata with energy constraints{"}, FORMATS'08], we show that the existence of an infinite lower-bound-constrained run is---for us somewhat unexpectedly---undecidable for weighted timed automata with four or more clocks.\par This undecidability result assumes a fixed and know initial credit. We show that the related problem of existence of an initial credit for which there ex- ist a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. Finally, we prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.}, } |

[BMS12] | Patricia Bouyer,
Nicolas Markey, and
Ocan Sankur.
Robust reachability in timed automata: a game-based
approach.
In ICALP'12,
Lecture Notes in Computer Science 7392, pages 128-140. Springer-Verlag, July 2012.
- Abstract
Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes 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 a timed automaton; with "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.
@inproceedings{icalp2012-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust reachability in timed automata: a~game-based approach}, editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew and Wattenhofer, Roger}, booktitle = {{P}roceedings of the 39th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'12)~-- Part~{II}}, acronym = {{ICALP}'12}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {7392}, pages = {128-140}, year = {2012}, month = jul, doi = {10.1007/978-3-642-31585-5_15}, abstract = {Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes 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 a timed automaton; with {"}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.}, } |

[DLM12] | Arnaud Da Costa,
François Laroussinie, and
Nicolas Markey.
Quantified CTL: Expressiveness and Model Checking.
In CONCUR'12,
Lecture Notes in Computer Science 7454, pages 177-192. Springer-Verlag, September 2012.
- Abstract
While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking ATL-like temporal logics for games.
@inproceedings{concur2012-DLM, author = {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {Quantified~{CTL}: Expressiveness and Model Checking}, editor = {Koutny, Maciej and Ulidowski, Irek}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, acronym = {{CONCUR}'12}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {7454}, pages = {177-192}, year = {2012}, month = sep, doi = {10.1007/978-3-642-32940-1_14}, abstract = {While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking ATL-like temporal logics for games.}, } |

[SVM+12] | Diego V. Simões De Sousa,
Henrique Viana,
Nicolas Markey, and
Jose Antônio F. de Macêdo.
Querying Trajectories through Model Checking based
on Timed Automata.
In SBBD'12,
pages 33-40.
Sociedade Brasileira de Computação, October 2012.
- Abstract
The popularization of geographical position devices (e.g. GPS) creates new opportunities for analyzing behavior of moving objects. However, such analysis are hindered by a lack of semantic information associated to the basic information provided by GPS. Previous works propose semantic enrichment of trajectories. Through the semantic enrichment, we could check which trajectories have a given moving sequence in an application. Often, this sequence is expressed according to the semantic application, using the approach of semantic trajectories proposed in the literature. This trajectory can be represented as a sequence of predicates that holds in some time interval. However, the solutions for querying moving sequence proposed by previous works have a high computational cost. In this paper, we propose an expressive query language to semantic trajectories that allows temporal constraints. To evaluate a query we will use model checking based on timed automata, that can be performed in polynomial time. As this model checking algorithm is not implemented yet, we propose to use UPPAAL tool, that can be more expensive theoretically, but we expected that will be ecient for our approach. In addition, we will present a query example that demonstrates the expressive power of our language. Although in this paper we will focus on semantic trajectories data, our approach is general enough for being applied to other purposes.
@inproceedings{sbbd2012-SVMM, author = {Sim{\~o}es{ }De{~}Sousa, Diego V. and Viana, Henrique and Markey, Nicolas and de Mac{\^e}do, Jose Ant{\^o}nio F.}, title = {Querying Trajectories through Model Checking based on Timed Automata}, editor = {Casanova, Marco A.}, booktitle = {{P}roceedings of the 27th {B}razilian {S}ymposium on {D}atabases ({SBBD}'12)}, acronym = {{SBBD}'12}, publisher = {Sociedade Brasileira de Computa{\c c}{\~a}o}, pages = {33-40}, year = {2012}, month = oct, abstract = {The popularization of geographical position devices (e.g.~GPS) creates new opportunities for analyzing behavior of moving objects. However, such analysis are hindered by a lack of semantic information associated to the basic information provided by~GPS. Previous works propose semantic enrichment of trajectories. Through the semantic enrichment, we~could check which trajectories have a given moving sequence in an application. Often, this~sequence is expressed according to the semantic application, using the approach of semantic trajectories proposed in the literature. This~trajectory can be represented as a sequence of predicates that holds in some time interval. However, the solutions for querying moving sequence proposed by previous works have a high computational cost. In~this paper, we~propose an expressive query language to semantic trajectories that allows temporal constraints. To~evaluate a query we will use model checking based on timed automata, that can be performed in polynomial time. As~this model checking algorithm is not implemented yet, we propose to use UPPAAL tool, that can be more expensive theoretically, but we expected that will be ecient for our approach. In addition, we will present a query example that demonstrates the expressive power of our language. Although in this paper we will focus on semantic trajectories data, our approach is general enough for being applied to other purposes.}, } |

2011 | |

[BFL+11] | Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen, and
Nicolas Markey.
Quantitative analysis of real-time systems using
priced timed automata.
Communications of the ACM 54(9):78-87. ACM Press, September 2011.
- Abstract
The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nano-seconds to the weekly, monthly, or longer-range reactive planning in a factory or a supply chain.
@article{cacm54(9)-BFLM, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim Guldstrand and Markey, Nicolas}, title = {Quantitative analysis of real-time systems using priced timed automata}, publisher = {ACM Press}, journal = {Communications of the ACM}, volume = {54}, number = {9}, pages = {78-87}, year = {2011}, month = sep, doi = {10.1145/1995376.1995396}, abstract = {The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nano-seconds to the weekly, monthly, or longer-range reactive planning in a factory or a supply chain.}, } |

[BBM+11] | Patricia Bouyer,
Romain Brenguier,
Nicolas Markey, and
Michael Ummels.
Nash Equilibria in Concurrent Games with
Büchi Objectives.
In FSTTCS'11,
Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, December 2011.
- Abstract
We study the problem of the existence (and computation) of Nash equilibria in multi-player concurrent games with Büchi-definable objectives. First, when the objectives are Büchi conditions on the game, we prove that the existence problem can be solved in polynomial time. In a second part, we extend our technique to objectives defined by deterministic Büchi automata, and prove that the problem then becomes EXPTIME-complete. We prove PSPACE-completeness for the case where the Büchi automata are 1-weak.
@inproceedings{fsttcs2011-BBMU, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {{N}ash Equilibria in Concurrent Games with {B}{\"u}chi Objectives}, editor = {Chakraborty, Supratik and Kumar, Amit}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, acronym = {{FSTTCS}'11}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {13}, pages = {375-386}, year = {2011}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2011.375}, abstract = {We study the problem of the existence (and computation) of Nash equilibria in multi-player concurrent games with B{\"u}chi-definable objectives. First, when the objectives are B{\"u}chi conditions on the game, we prove that the existence problem can be solved in polynomial time. In a second part, we extend our technique to objectives defined by deterministic B{\"u}chi automata, and prove that the problem then becomes EXPTIME-complete. We prove PSPACE-completeness for the case where the B{\"u}chi automata are 1-weak.}, } |

[BLM+11] | Patricia Bouyer,
Kim Guldstrand Larsen,
Nicolas Markey,
Ocan Sankur, and
Claus Thrane.
Timed automata can always be made implementable.
In CONCUR'11,
Lecture Notes in Computer Science 6901, pages 76-91. Springer-Verlag, September 2011.
- Abstract
Timed automata follow a mathematical semantics, which assumes perfect precision and synchrony of clocks. Since this hypothesis does not hold in digital systems, properties proven formally on a timed automaton may be lost at implementation. In order to ensure implementability, several approaches have been considered, corresponding to different hypotheses on the implementation platform. We address two of these: a timed automaton is samplable if its semantics is preserved under a discretization of time; it is robust if its semantics is preserved when all timing constraints are relaxed by some small positive parameter. We propose a construction which makes timed automata implementable in the above sense: From any timed automaton A, we build a timed automaton A' that exhibits the same behaviour as A, and moreover is both robust and samplable by construction.
@inproceedings{concur2011-BLMST, author = {Bouyer, Patricia and Larsen, Kim Guldstrand and Markey, Nicolas and Sankur, Ocan and Thrane, Claus}, title = {Timed automata can always be made implementable}, editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'11)}, acronym = {{CONCUR}'11}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {6901}, pages = {76-91}, year = {2011}, month = sep, doi = {10.1007/978-3-642-23217-6_6}, abstract = {Timed automata follow a mathematical semantics, which assumes perfect precision and synchrony of clocks. Since this hypothesis does not hold in digital systems, properties proven formally on a timed automaton may be lost at implementation. In order to ensure implementability, several approaches have been considered, corresponding to different hypotheses on the implementation platform. We address two of these: a~timed automaton is samplable if its semantics is preserved under a discretization of time; it is robust if its semantics is preserved when all timing constraints are relaxed by some small positive parameter. We propose a construction which makes timed automata implementable in the above sense: From any timed automaton~\(\mathcal{A}\), we build a timed automaton~\(\mathcal{A}'\) that exhibits the same behaviour as~\(\mathcal{A}\), and moreover is both robust and samplable by construction.}, } |

[BMO+11] | Patricia Bouyer,
Nicolas Markey,
Jörg Olschewski, and
Michael Ummels.
Measuring Permissiveness in Parity Games:
Mean-Payoff Parity Games Revisited.
In ATVA'11,
Lecture Notes in Computer Science 6996, pages 135-149. Springer-Verlag, October 2011.
- Abstract
We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number/weight of transitions blocked by a strategy. Using a translation into mean-payoff parity games, we prove that deciding (the permissiveness of) a most permissive winning strategy is in NP∩coNP. Along the way, we provide a new study of mean-payoff parity games. In particular, we give a new algorithm for solving these games, which beats all previously known algorithms for this problem.
@inproceedings{atva2011-BMOU, author = {Bouyer, Patricia and Markey, Nicolas and Olschewski, J{\"o}rg and Ummels, Michael}, title = {Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited}, editor = {Bultan, Tevfik and Hsiung, Pao-Ann}, booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'11)}, acronym = {{ATVA}'11}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {6996}, pages = {135-149}, year = {2011}, month = oct, doi = {10.1007/978-3-642-24372-1_11}, abstract = {We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number{\slash}weight of transitions blocked by a strategy. Using a translation into mean-payoff parity games, we prove that deciding (the permissiveness~of) a~most permissive winning strategy is in \(\textsf{NP}\cap\textsf{coNP}\). Along the way, we~provide a new study of mean-payoff parity games. In particular, we give a new algorithm for solving these games, which beats all previously known algorithms for this problem.}, } |

[BMS11] | Patricia Bouyer,
Nicolas Markey, and
Ocan Sankur.
Robust Model-Checking of Timed Automata via Pumping
in Channel Machines.
In FORMATS'11,
Lecture Notes in Computer Science 6919, pages 97-112. Springer-Verlag, September 2011.
- Abstract
Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satised by digital hardware on which the models are implemented. In fact, it was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system. The problem of robust model-checking was then dened to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct. In this work, we show that robust model-checking against ω-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of ω-regular properties, which is both optimal and valid for general timed automata.
@inproceedings{formats2011-BMS, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Model-Checking of Timed Automata via Pumping in Channel Machines}, editor = {Fahrenberg, Uli and Tripakis, Stavros}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'11)}, acronym = {{FORMATS}'11}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {6919}, pages = {97-112}, year = {2011}, month = sep, doi = {10.1007/978-3-642-24310-3_8}, abstract = {Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satised by digital hardware on which the models are implemented. In~fact, it~was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system.\par The problem of robust model-checking was then dened to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct.\par In this work, we show that robust model-checking against \(\omega\)-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of \(\omega\)-regular properties, which is both optimal and valid for general timed automata.}, } |

[SBM11] | Ocan Sankur,
Patricia Bouyer, and
Nicolas Markey.
Shrinking Timed Automata.
In FSTTCS'11,
Leibniz International Proceedings in Informatics 13, pages 90-102. Leibniz-Zentrum für Informatik, December 2011.
- Abstract
We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce *parametric shrinking*of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata both properties are preserved in implementation.
@inproceedings{fsttcs2011-SBM, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas}, title = {Shrinking Timed Automata}, editor = {Chakraborty, Supratik and Kumar, Amit}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, acronym = {{FSTTCS}'11}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {13}, pages = {90-102}, year = {2011}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2011.90}, abstract = {We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce \emph{parametric shrinking} of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata both properties are preserved in implementation.}, } |

[Mar11] | Nicolas Markey.
Robustness in Real-time Systems.
In SIES'11,
pages 28-34.
IEEE Comp. Soc. Press, June 2011.
- Abstract
We review several aspects of robustness of real-time systems, and present recent results on the robust verification of timed automata.
@inproceedings{sies2011-Mar, author = {Markey, Nicolas}, title = {Robustness in Real-time Systems}, booktitle = {{P}roceedings of the 6th {IEEE} {I}nternational {S}ymposium on {I}ndustrial {E}mbedded {S}ystems ({SIES}'11)}, acronym = {{SIES}'11}, publisher = {IEEE Comp. Soc. Press}, pages = {28-34}, year = {2011}, month = jun, doi = {10.1109/SIES.2011.5953652}, abstract = {We~review several aspects of robustness of real-time systems, and present recent results on the robust verification of timed automata.}, } |

[Mar11] | Nicolas Markey.
Verification of Embedded Systems – Algorithms and
Complexity.
Mémoire d'habilitation,
École Normale Supérieure de Cachan, France,
April 2011.
@phdthesis{hdr2011-Mar, author = {Markey, Nicolas}, title = {Verification of Embedded Systems -- Algorithms and Complexity}, year = {2011}, month = apr, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, type = {M\'emoire d'habilitation}, } |

2010 | |

[BCM10] | Patricia Bouyer,
Fabrice Chevalier, and
Nicolas Markey.
On the Expressiveness of TPTL and MTL.
Information and Computation 208(2):97-116. Elsevier, February 2010.
- Abstract
TPTL and MTL are two classical timed extensions of LTL. In this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture *can*be expressed in MTL. More generally, we show that TPTL formulae using only modality F can be translated into MTL.
@article{icomp208(2)-BCM, author = {Bouyer, Patricia and Chevalier, Fabrice and Markey, Nicolas}, title = {On the Expressiveness of {TPTL} and {MTL}}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {208}, number = {2}, pages = {97-116}, year = {2010}, month = feb, doi = {10.1016/j.ic.2009.10.004}, abstract = {TPTL and MTL are two classical timed extensions of~LTL. In~this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than~MTL. But we show that, surprisingly, the TPTL~formula proposed by Alur and Henzinger for witnessing this conjecture \emph{can} be expressed in~MTL. More generally, we show that TPTL formulae using only modality~F can be translated into~MTL.}, } |

[BJL+10] | Thomas Brihaye,
Marc Jungers,
Samson Lasaulce,
Nicolas Markey, and
Ghassan Oreiby.
Using Model Checking for Analyzing Distributed Power
Control Problems.
EURASIP Journal on Wireless Communications and
Networking 2010(861472).
Hindawi Publishing Corp., June 2010.
- Abstract
Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control (PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed PC. It turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.
@article{jwcn2010(861472)-BJLMO, author = {Brihaye, {\relax Th}omas and Jungers, Marc and Lasaulce, Samson and Markey, Nicolas and Oreiby, Ghassan}, title = {Using Model Checking for Analyzing Distributed Power Control Problems}, publisher = {Hindawi Publishing Corp.}, journal = {EURASIP Journal on Wireless Communications and Networking}, volume = {2010}, number = {861472}, year = {2010}, month = jun, doi = {10.1155/2010/861472}, abstract = {Model checking~(MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control~(PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed~PC. It~turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.}, } |

[BBM10] | Patricia Bouyer,
Romain Brenguier, and
Nicolas Markey.
Nash Equilibria for Reachability Objectives in
Multi-player Timed Games.
In CONCUR'10,
Lecture Notes in Computer Science 6269, pages 192-206. Springer-Verlag, September 2010.
- Abstract
We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly infinite) concurrent games. Along the way, we use our characterization to compute Nash equilibria in finite concurrent games.
@inproceedings{concur2010-BBM, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas}, title = {{N}ash Equilibria for Reachability Objectives in Multi-player Timed Games}, editor = {Gastin, Paul and Laroussinie, Fran{\c c}ois}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'10)}, acronym = {{CONCUR}'10}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {6269}, pages = {192-206}, year = {2010}, month = sep, doi = {10.1007/978-3-642-15375-4_14}, abstract = {We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly infinite) concurrent games. Along the way, we~use our characterization to compute Nash equilibria in finite concurrent games.}, } |

[BBM10] | Patricia Bouyer,
Romain Brenguier, and
Nicolas Markey.
Computing Equilibria in Two-Player Timed Games
via Turn-Based Finite Games.
In FORMATS'10,
Lecture Notes in Computer Science 6246, pages 62-76. Springer-Verlag, September 2010.
- Abstract
We study two-player timed games where the objectives of the two players are not opposite. We focus on the standard notion of Nash equilibrium and propose a series of transformations that builds two finite turn-based games out of a timed game, with a precise correspondence between Nash equilibria in the original and in final games. This provides us with an algorithm to compute Nash equilibria in two-player timed games for large classes of properties.
@inproceedings{formats2010-BBM, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas}, title = {Computing Equilibria in Two-Player Timed Games {\textit{via}}~Turn-Based Finite Games}, editor = {Chatterjee, Krishnendu and Henzinger, Thomas A.}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'10)}, acronym = {{FORMATS}'10}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {6246}, pages = {62-76}, year = {2010}, month = sep, doi = {10.1007/978-3-642-15297-9_7}, abstract = {We study two-player timed games where the objectives of the two players are not opposite. We focus on the standard notion of Nash equilibrium and propose a series of transformations that builds two finite turn-based games out of a timed game, with a precise correspondence between Nash equilibria in the original and in final games. This provides us with an algorithm to compute Nash equilibria in two-player timed games for large classes of properties.}, } |

[BFL+10] | Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen, and
Nicolas Markey.
Timed Automata with Observers under Energy
Constraints.
In HSCC'10,
pages 61-70.
ACM Press, April 2010.
- Abstract
In this paper, we study one-clock priced timed automata in which prices can grow linearly (dp/dt=k) or exponentially (dp/dt=kp), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).
@inproceedings{hscc2010-BFLM, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim Guldstrand and Markey, Nicolas}, title = {Timed Automata with Observers under Energy Constraints}, editor = {Johansson, Karl Henrik and Yi, Wang}, booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop on {H}ybrid {S}ystems: {C}omputation and {C}ontrol ({HSCC}'10)}, acronym = {{HSCC}'10}, publisher = {ACM Press}, pages = {61-70}, year = {2010}, month = apr, doi = {10.1145/1755952.1755963}, abstract = {In this paper, we study one-clock priced timed automata in which prices can grow linearly (\(\frac{dp}{dt}=k\)) or exponentially (\(\frac{dp}{dt}=kp\)), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).}, } |

[DLM10] | Arnaud Da Costa,
François Laroussinie, and
Nicolas Markey.
ATL with strategy contexts: Expressiveness and
Model Checking.
In FSTTCS'10,
Leibniz International Proceedings in Informatics 8, pages 120-132. Leibniz-Zentrum für Informatik, December 2010.
- Abstract
We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we prove that they remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.
@inproceedings{fsttcs2010-DLM, author = {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {{ATL} with strategy contexts: Expressiveness and Model Checking}, editor = {Lodaya, Kamal and Mahajan, Meena}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, acronym = {{FSTTCS}'10}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {8}, pages = {120-132}, year = {2010}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2010.120}, abstract = {We study the alternating-time temporal logics \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) where strategy quantifiers reset previously selected strategies.\par We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely \(\textsf{ATL}_{\textsf{sc}}\) and~\(\textsf{ATL}_{\textsf{sc}}^{*}\), equally expressive: any~formula in~\(\textsf{ATL}_{\textsf{sc}}^{*}\) can be translated into an equivalent, linear-size \(\textsf{ATL}_{\textsf{sc}}\) formula. Despite the high expressiveness of these logics, we prove that they remain decidable by designing a tree-automata-based algorithm for model-checking \(\textsf{ATL}_{\textsf{sc}}\) on the full class of \(n\)-player concurrent game structures.}, } |

[HBM+10] | Paul Hunter,
Patricia Bouyer,
Nicolas Markey,
Joël Ouaknine, and
James Worrell.
Computing Rational Radical Sums in Uniform
TC0.
In FSTTCS'10,
Leibniz International Proceedings in Informatics 8, pages 308-316. Leibniz-Zentrum für Informatik, December 2010.
- Abstract
A fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether ∑i=1m Ci . AiXi is zero for given rational numbers Ai, Ci, Xi. It has been known for almost twenty years that this can be decided in polynomial time. In this paper we improve this result by showing membership in uniform TC0. This requires several significant departures from Blömer's polynomial-time algorithm as the latter crucially relies on primitives, such as gcd computation and binary search, that are not known to be in TC0.
@inproceedings{fsttcs2010-HBMOW, author = {Hunter, Paul and Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Computing Rational Radical Sums in Uniform {TC\textsuperscript{0}}}, editor = {Lodaya, Kamal and Mahajan, Meena}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, acronym = {{FSTTCS}'10}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {8}, pages = {308-316}, year = {2010}, month = dec, doi = {10.4230/LIPIcs.FSTTCS.2010.308}, abstract = {A~fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether \(\sum_{i=1}^m C_i \cdot A_i^{X_i}\) is zero for given rational numbers~\(A_i\), \(C_i\),~\(X_i\). It~has been known for almost twenty years that this can be decided in polynomial time. In this paper we improve this result by showing membership in uniform \(\textsf{TC}^0\). This requires several significant departures from Bl{\"o}mer's polynomial-time algorithm as the latter crucially relies on primitives, such as gcd computation and binary search, that are not known to be in~\(\textsf{TC}^0\).}, } |

[MW10] | Nicolas Markey and
Jef Wijsen (eds.)
Proceedings of the 17th International
Symposium on Temporal Representation and
Reasoning (TIME'10).
IEEE Comp. Soc. Press, September 2010.
@proceedings{time2010-MW, title = {{P}roceedings of the 17th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'10)}, editor = {Markey, Nicolas and Wijsen, Jef}, booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'10)}, acronym = {{TIME}'10}, publisher = {IEEE Comp. Soc. Press}, year = {2010}, month = sep, doi = {10.1109/TIME.2010.4}, url = {http://ieeexplore.ieee.org/xpl/ tocresult.jsp? reload=true&isnumber=5601852}, } |

2009 | |

[BDL+09] | Thomas Brihaye,
Arnaud Da Costa,
François Laroussinie, and
Nicolas Markey.
ATL with Strategy Contexts and Bounded Memory.
In LFCS'09,
Lecture Notes in Computer Science 5407, pages 92-106. Springer-Verlag, January 2009.
- Abstract
We extend the alternating-time temporal logics ATL and ATL* with *strategy contexts*and*memory constraints*: the first extension make strategy quantifiers to not "forget" the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies.We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Game Logic, Strategy Logic, ...). We then address the problem of model-checking for our logics, providing a PSPACE algoritm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case.
@inproceedings{lfcs2009-BDLM, author = {Brihaye, {\relax Th}omas and Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {{ATL} with Strategy Contexts and Bounded Memory}, editor = {Artemov, Sergei N. and Nerode, Anil}, booktitle = {{P}roceedings of the {I}nternational {S}ymposium {L}ogical {F}oundations of {C}omputer {S}cience ({LFCS}'09)}, acronym = {{LFCS}'09}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {5407}, pages = {92-106}, year = {2009}, month = jan, doi = {10.1007/978-3-540-92687-0_7}, abstract = {We extend the alternating-time temporal logics ATL and ATL\textsuperscript{*} with \emph{strategy contexts} and \emph{memory constraints}: the first extension make strategy quantifiers to not {"}forget{"} the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies.\par We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL\textsuperscript{*}, Game Logic, Strategy Logic,~...). We~then address the problem of model-checking for our logics, providing a PSPACE algoritm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case.}, } |

[BDM+09] | Patricia Bouyer,
Marie Duflot,
Nicolas Markey, and
Gabriel Renault.
Measuring Permissivity in Finite Games.
In CONCUR'09,
Lecture Notes in Computer Science 5710, pages 196-210. Springer-Verlag, September 2009.
- Abstract
In this paper, we extend the classical notion of strategies in turn-based finite games by allowing several moves to be selected. We define and study a quantitative measure for permissivity of such strategies by assigning penalties when blocking transitions. We prove that for reachability objectives, most permissive strategies exist, can be chosen memoryless, and can be computed in polynomial time, while it is in NP∩coNP for discounted and mean penalties.
@inproceedings{concur2009-BDMR, author = {Bouyer, Patricia and Duflot, Marie and Markey, Nicolas and Renault, Gabriel}, title = {Measuring Permissivity in Finite Games}, editor = {Bravetti, Mario and Zavattaro, Gianluigi}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'09)}, acronym = {{CONCUR}'09}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {5710}, pages = {196-210}, year = {2009}, month = sep, doi = {10.1007/978-3-642-04081-8_14}, abstract = {In this paper, we extend the classical notion of strategies in turn-based finite games by allowing several moves to be selected. We~define and study a quantitative measure for permissivity of such strategies by assigning penalties when blocking transitions. We~prove that for reachability objectives, most permissive strategies exist, can be chosen memoryless, and can be computed in polynomial time, while it is in \(\textsf{NP}\cap\textsf{coNP}\) for discounted and mean penalties.}, } |

[CM09] | Franck Cassez and
Nicolas Markey.
Control of Timed Systems.
In Claude Jard and
Olivier H. Roux (eds.),
Communicating Embedded Systems – Software and
Design.
Wiley-ISTE, October 2009.
@incollection{ces2009-CM, author = {Cassez, Franck and Markey, Nicolas}, title = {Control of Timed Systems}, editor = {Jard, Claude and Roux, Olivier H.}, booktitle = {Communicating Embedded Systems~-- Software and Design}, publisher = {Wiley-ISTE}, pages = {83-120}, chapter = {3}, year = {2009}, month = oct, url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288}, } |

2008 | |

[BLM08] | Patricia Bouyer,
Kim Guldstrand Larsen, and
Nicolas Markey.
Model Checking One-clock Priced Timed Automata.
Logical Methods in Computer Science 4(2).
May 2008.
- Abstract
We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model checking WMTL (LTL with cost-constrained modalities) is decidable only if there is a single clock in the model and a single stopwatch cost variable ( *i.e.*, whose slopes lie in {0,1}).
@article{lmcs4(2)-BLM, author = {Bouyer, Patricia and Larsen, Kim Guldstrand and Markey, Nicolas}, title = {Model Checking One-clock Priced Timed Automata}, journal = {Logical Methods in Computer Science}, volume = {4}, number = {2}, year = {2008}, month = may, doi = {10.2168/LMCS-4(2:9)2008}, abstract = {We consider the model of priced (a.k.a.~weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic~WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We~also prove that model checking WMTL (LTL with cost-constrained modalities) is decidable only if there is a single clock in the model and a single stopwatch cost variable (\textit{i.e.}, whose slopes lie in~\(\{0,1\}\)).}, } |

[DDM+08] | Martin De Wulf,
Laurent Doyen,
Nicolas Markey, and
Jean-François Raskin.
Robust Safety of Timed Automata.
Formal Methods in System Design 33(1-3):45-84. Springer-Verlag, December 2008.
- Abstract
Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by Δ>0 and clocks can drift by ε>0. The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks. We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters Δ and ε such that the timed automaton never enters the bad states under the relaxed semantics.
@article{fmsd33(1-3)-DDMR, author = {De{~}Wulf, Martin and Doyen, Laurent and Markey, Nicolas and Raskin, Jean-Fran{\c c}ois}, title = {Robust Safety of Timed Automata}, publisher = {Springer-Verlag}, journal = {Formal Methods in System Design}, volume = {33}, number = {1-3}, pages = {45-84}, year = {2008}, month = dec, doi = {10.1007/s10703-008-0056-7}, abstract = {Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by~\(\Delta>0\) and clocks can drift by~\(\epsilon>0\). The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks.\par We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters~\(\Delta\) and~\(\epsilon\) such that the timed automaton never enters the bad states under the relaxed semantics.}, } |

[LMO08] | François Laroussinie,
Nicolas Markey, and
Ghassan Oreiby.
On the Expressiveness and Complexity of ATL.
Logical Methods in Computer Science 4(2).
May 2008.
- Abstract
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.
@article{lmcs4(2)-LMO, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Oreiby, Ghassan}, title = {On the Expressiveness and Complexity of~{ATL}}, journal = {Logical Methods in Computer Science}, volume = {4}, number = {2}, year = {2008}, month = may, doi = {10.2168/LMCS-4(2:7)2008}, abstract = {ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of~ATL (built on modalities {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be completed in order to express the duals of its modalities: it~is necessary to add the modality {"}Release{"}. We~then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete, depending on the underlying multi-agent model (ATS and CGS,~resp.). We also prove that~ATL\({}^{+}\) model-checking is \(\Delta_{3}^{P}\)-complete over both models, even with a fixed number of agents.}, } |

[BBB+08] | Nathalie Bertrand,
Patricia Bouyer,
Thomas Brihaye, and
Nicolas Markey.
Quantitative Model-Checking of One-Clock Timed
Automata under Probabilistic Semantics.
In QEST'08,
pages 55-64.
IEEE Comp. Soc. Press, September 2008.
- Abstract
In [Baier *et al.*,*Probabilistic and Topological Semantics for Timed Automata*, FSTTCS'07] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability 1 in a timed automaton, and solved for the class of single-clock timed automata.In this paper, we consider the quantitative model-checking problem for ω-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an ω-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.
@inproceedings{qest2008-BBBM, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Markey, Nicolas}, title = {Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'08)}, acronym = {{QEST}'08}, publisher = {IEEE Comp. Soc. Press}, pages = {55-64}, year = {2008}, month = sep, doi = {10.1109/QEST.2008.19}, abstract = {In [Baier \emph{et~al.}, \textit{Probabilistic and Topological Semantics for Timed Automata}, FSTTCS'07] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability~\(1\) in a timed automaton, and solved for the class of single-clock timed automata.\par In this paper, we consider the quantitative model-checking problem for \(\omega\)-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an \(\omega\)-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.}, } |

[BFL+08] | Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen,
Nicolas Markey, and
Jiří Srba.
Infinite Runs in Weighted Timed Automata with Energy
Constraints.
In FORMATS'08,
Lecture Notes in Computer Science 5215, pages 33-47. Springer-Verlag, September 2008.
- Abstract
We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource ( *e.g.*energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (*e.g.*remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.
@inproceedings{formats2008-BFLMS, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim Guldstrand and Markey, Nicolas and Srba, Ji{\v r}{\'\i}}, title = {Infinite Runs in Weighted Timed Automata with Energy Constraints}, editor = {Cassez, Franck and Jard, Claude}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'08)}, acronym = {{FORMATS}'08}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {5215}, pages = {33-47}, year = {2008}, month = sep, doi = {10.1007/978-3-540-85778-5_4}, abstract = {We~study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we~consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (\emph{e.g.}~energy). We~ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (\emph{e.g.}~remains between~\(0\) and some given upper-bound). We~also consider a game version of the above, where certain transitions may be uncontrollable.}, } |

[BGM+08] | Thomas Brihaye,
Mohamed Ghannem,
Nicolas Markey, and
Lionel Rieg.
Good friends are hard to find!.
In TIME'08,
pages 32-40.
IEEE Comp. Soc. Press, June 2008.
- Abstract
We focus on the problem of finding (the size of) a minimal winning coalition in a multi-player game. More precisely, we prove that deciding whether there is a winning coalition of size at most k is NP-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.
@inproceedings{time2008-BGMR, author = {Brihaye, {\relax Th}omas and Ghannem, Mohamed and Markey, Nicolas and Rieg, Lionel}, title = {Good friends are hard to find!}, booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'08)}, acronym = {{TIME}'08}, publisher = {IEEE Comp. Soc. Press}, pages = {32-40}, year = {2008}, month = jun, doi = {10.1109/TIME.2008.10}, abstract = {We focus on the problem of finding (the~size of) a~minimal winning coalition in a multi-player game. More precisely, we~prove that deciding whether there is a winning coalition of size at most~\(k\) is NP-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.}, } |

[BMO+08] | Patricia Bouyer,
Nicolas Markey,
Joël Ouaknine,
Philippe Schnoebelen, and
James Worrell.
On Termination for Faulty Channel Machines.
In STACS'08,
Leibniz International Proceedings in Informatics 1, pages 121-132. Leibniz-Zentrum für Informatik, February 2008.
- Abstract
A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with *insertion errors*,*i.e.*, machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity.
@inproceedings{stacs2008-BMOSW, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and Worrell, James}, title = {On Termination for Faulty Channel Machines}, editor = {Albers, Susanne and Weil, Pascal}, booktitle = {{P}roceedings of the 25th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'08)}, acronym = {{STACS}'08}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {1}, pages = {121-132}, year = {2008}, month = feb, doi = {10.4230/LIPIcs.STACS.2008.1339}, abstract = {A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with \emph{insertion errors}, \textit{i.e.}, machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We~consider the termination problem: are all the computations of a given insertion channel machine finite? We~show that this problem has non-elementary, yet primitive recursive complexity.}, } |

[BMO+08] | Patricia Bouyer,
Nicolas Markey,
Joël Ouaknine, and
James Worrell.
On Expressiveness and Complexity in Real-time Model
Checking.
In ICALP'08,
Lecture Notes in Computer Science 5126, pages 124-135. Springer-Verlag, July 2008.
- Abstract
Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called *punctual*specifications. In this paper we introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of MITL. We conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.
@inproceedings{icalp2008-BMOW, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {On Expressiveness and Complexity in Real-time Model Checking}, editor = {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg, Leslie Ann and Halld{\'o}rsson, Magn{\'u}s M. and Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor}, booktitle = {{P}roceedings of the 35th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'08)~-- Part~{II}}, acronym = {{ICALP}'08}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {5126}, pages = {124-135}, year = {2008}, month = jul, doi = {10.1007/978-3-540-70583-3_11}, abstract = {Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called \emph{punctual} specifications. In~this paper we~introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of~MITL. We~conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.}, } |

[BMR08] | Patricia Bouyer,
Nicolas Markey, and
Pierre-Alain Reynier.
Robust Analysis of Timed Automata via Channel
Machines.
In FoSSaCS'08,
Lecture Notes in Computer Science 4962, pages 157-171. Springer-Verlag, March 2008.
- Abstract
Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of MTL, is EXPSPACE-Complete.
@inproceedings{fossacs2008-BMR, author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Robust Analysis of Timed Automata via Channel Machines}, editor = {Amadio, Roberto}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'08)}, acronym = {{FoSSaCS}'08}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4962}, pages = {157-171}, year = {2008}, month = mar, doi = {10.1007/978-3-540-78499-9_12}, abstract = {Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a~new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of~MTL, is EXPSPACE-Complete.}, } |

[CM08] | Franck Cassez and
Nicolas Markey.
Contrôle des systèmes temporisés.
In Olivier H. Roux and
Claude Jard (eds.),
Approches formelles des systèmes embarqués
communicants.
Hermès, October 2008.
@incollection{afsec2008-CM, author = {Cassez, Franck and Markey, Nicolas}, title = {Contr{\^o}le des syst{\`e}mes temporis{\'e}s}, editor = {Roux, Olivier H. and Jard, Claude}, booktitle = {Approches formelles des syst{\`e}mes embarqu{\'e}s communicants}, publisher = {Herm{\`e}s}, pages = {105-144}, chapter = {4}, year = {2008}, month = oct, url = {http://e.lavoisier.fr/produit/9782746243156}, } |

2007 | |

[BLM07] | Patricia Bouyer,
Kim Guldstrand Larsen, and
Nicolas Markey.
Model Checking One-clock Priced Timed Automata.
In FoSSaCS'07,
Lecture Notes in Computer Science 4423, pages 108-122. Springer-Verlag, March 2007.
- Abstract
We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions. We prove that model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete under the "single-clock" assumption. In contrast, it has been recently proved that the model-checking problem is undecidable for this model as soon as the system has three clocks. We also prove that the model-checking of WCTL becomes undecidable, even under this "single-clock" assumption.
@inproceedings{fossacs2007-BLM, author = {Bouyer, Patricia and Larsen, Kim Guldstrand and Markey, Nicolas}, title = {Model Checking One-clock Priced Timed Automata}, editor = {Seidl, Helmut}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'07)}, acronym = {{FoSSaCS}'07}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4423}, pages = {108-122}, year = {2007}, month = mar, doi = {10.1007/978-3-540-71389-0_9}, abstract = {We consider the model of priced (a.k.a.~weighted) timed automata, an extension of timed automata with cost information on both locations and transitions. We prove that model-checking this class of models against the logic~WCTL, CTL~with cost-constrained modalities, is PSPACE-complete under the {"}single-clock{"} assumption. In~contrast, it~has been recently proved that the model-checking problem is undecidable for this model as soon as the system has three clocks. We also prove that the model-checking of~WCTL becomes undecidable, even under this {"}single-clock{"} assumption.}, } |

[BLM+07] | Thomas Brihaye,
François Laroussinie,
Nicolas Markey, and
Ghassan Oreiby.
Timed Concurrent Game Structures.
In CONCUR'07,
Lecture Notes in Computer Science 4703, pages 445-459. Springer-Verlag, September 2007.
- Abstract
We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical *timed game automata*of Asarin*et al.*, our timed CGSs are "more concurrent", in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the "element of surprise" of timed game automata reported by de Alfaro*et al.*We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable *via*region abstraction, and in particular that strategies are "region-stable" if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger*et al.*
@inproceedings{concur2007-BLMO, author = {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c c}ois and Markey, Nicolas and Oreiby, Ghassan}, title = {Timed Concurrent Game Structures}, editor = {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'07)}, acronym = {{CONCUR}'07}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4703}, pages = {445-459}, year = {2007}, month = sep, doi = {10.1007/978-3-540-74407-8_30}, abstract = {We propose a new model for timed games, based on concurrent game structures~(CGSs). Compared to the classical \emph{timed game automata} of~Asarin \emph{et~al.}, our timed~CGSs are {"}more concurrent{"}, in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the {"}element of surprise{"} of timed game automata reported by de~Alfaro \emph{et~al.}\par We prove that our model has nice properties, in particular that model-checking timed CGSs against timed \(\textsf{ATL}\) is decidable \emph{via} region abstraction, and in particular that strategies are {"}region-stable{"} if winning objectives are. We also propose a new extension of \(\textsf{TATL}\), containing~\(\textsf{ATL}^{*}\), which we call~\(\textsf{TALTL}\). We~prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger \emph{et~al.}}, } |

[BM07] | Patricia Bouyer and
Nicolas Markey.
Costs are Expensive!.
In FORMATS'07,
Lecture Notes in Computer Science 4763, pages 53-68. Springer-Verlag, October 2007.
- Abstract
We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.
@inproceedings{formats2007-BM, author = {Bouyer, Patricia and Markey, Nicolas}, title = {Costs are Expensive!}, editor = {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'07)}, acronym = {{FORMATS}'07}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4763}, pages = {53-68}, year = {2007}, month = oct, doi = {10.1007/978-3-540-75454-1_6}, abstract = {We study the model-checking problem for WMTL, a~cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We~draw a complete picture of the decidability for that problem: it~is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We~finally give some consequences on the undecidability of linear hybrid automata.}, } |

[BMO+07] | Patricia Bouyer,
Nicolas Markey,
Joël Ouaknine, and
James Worrell.
The Cost of Punctuality.
In LICS'07,
pages 109-118.
IEEE Comp. Soc. Press, July 2007.
- Abstract
In an influential paper titled "The Benefits of Relaxing Punctuality", Alur, Feder, and Henzinger introduced Metric Interval Temporal Logic (MITL) as a fragment of the real-time logic Metric Temporal Logic (MTL) in which exact or punctual timing constraints are banned. Their main result showed that model checking and satisfiability for MITL are both EXPSPACE-Complete. Until recently, it was widely believed that admitting even the simplest punctual specifications in any linear-time temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no punctual fragment of MTL was known to have even primitive recursive complexity (with certain decidable fragments having provably non-primitive recursive complexity). In this paper we identify a `co-flat' subset of MTL that is capable of expressing a large class of punctual specifications and for which model checking (although not satisfiability) has no complexity cost over MITL. Our logic is moreover qualitatively different from MITL in that it can express properties that are not timed-regular. Correspondingly, our decision procedures do not involve translating formulas into finite-state automata, but rather into certain kinds of reversal-bounded Turing machines. Using this translation we show that the model checking problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete if timing constraints are encoded in unary.
@inproceedings{lics2007-BMOW, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {The Cost of Punctuality}, booktitle = {{P}roceedings of the 22nd {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'07)}, acronym = {{LICS}'07}, publisher = {IEEE Comp. Soc. Press}, pages = {109-118}, year = {2007}, month = jul, doi = {10.1109/LICS.2007.49}, abstract = {In an influential paper titled {"}The Benefits of Relaxing Punctuality{"}, Alur, Feder, and~Henzinger introduced Metric Interval Temporal Logic~(MITL) as a fragment of the real-time logic Metric Temporal Logic~(MTL) in which exact or punctual timing constraints are banned. Their main result showed that model checking and satisfiability for~MITL are both EXPSPACE-Complete.\par Until recently, it was widely believed that admitting even the simplest punctual specifications in any linear-time temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no punctual fragment of~MTL was known to have even primitive recursive complexity (with certain decidable fragments having provably non-primitive recursive complexity).\par In this paper we identify a `co-flat' subset of~MTL that is capable of expressing a large class of punctual specifications and for which model checking (although not satisfiability) has no complexity cost over~MITL. Our logic is moreover qualitatively different from~MITL in that it can express properties that are not timed-regular. Correspondingly, our decision procedures do not involve translating formulas into finite-state automata, but rather into certain kinds of reversal-bounded Turing machines. Using this translation we show that the model checking problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete if timing constraints are encoded in unary.}, } |

[LMO07] | François Laroussinie,
Nicolas Markey, and
Ghassan Oreiby.
On the Expressiveness and Complexity of ATL.
In FoSSaCS'07,
Lecture Notes in Computer Science 4423, pages 243-257. Springer-Verlag, March 2007.
- Abstract
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.
@inproceedings{fossacs2007-LMO, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Oreiby, Ghassan}, title = {On the Expressiveness and Complexity of~{ATL}}, editor = {Seidl, Helmut}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'07)}, acronym = {{FoSSaCS}'07}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4423}, pages = {243-257}, year = {2007}, month = mar, doi = {10.1007/978-3-540-71389-0_18}, abstract = {ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of~ATL (built on modalities {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be completed in order to express the duals of its modalities: it~is necessary to add the modality {"}Release{"}. We~then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete, depending on the underlying multi-agent model (ATS and CGS,~resp.). We also prove that~ATL\({}^{+}\) model-checking is \(\Delta_{3}^{P}\)-complete over both models, even with a fixed number of agents.}, } |

2006 | |

[BBM06] | Patricia Bouyer,
Thomas Brihaye, and
Nicolas Markey.
Improved Undecidability Results on Weighted Timed
Automata.
Information Processing Letters 98(5):188-194. Elsevier, June 2006.
- Abstract
In this paper, we improve two recent undecidability results of Brihaye, Bruyère and Raskin about weighted timed automata, an extension of timed automata with a cost variable. Our results rely on a new encoding of the two counters of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.
@article{ipl98(5)-BBM, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Markey, Nicolas}, title = {Improved Undecidability Results on Weighted Timed Automata}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {98}, number = {5}, pages = {188-194}, year = {2006}, month = jun, doi = {10.1016/j.ipl.2006.01.012}, abstract = {In this paper, we improve two recent undecidability results of Brihaye, Bruy{\`e}re and Raskin about weighted timed automata, an extension of timed automata with a cost variable. Our results rely on a new encoding of the two counters of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.}, } |

[LMS06] | François Laroussinie,
Nicolas Markey, and
Philippe Schnoebelen.
Efficient timed model checking for discrete-time
systems.
Theoretical Computer Science 353(1-3):249-271. Elsevier, March 2006.
- Abstract
We consider model checking of timed temporal formulae in *durational transition graphs*(DTGs),*i.e.*, Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied.We exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration). Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes Δ2P-complete or PSPACE-complete depending on the considered semantics.
@article{tcs353(1-3)-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Efficient timed model checking for discrete-time systems}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {353}, number = {1-3}, pages = {249-271}, year = {2006}, month = mar, doi = {10.1016/j.tcs.2005.11.020}, abstract = {We consider model checking of timed temporal formulae in \emph{durational transition graphs} (DTGs), \emph{i.e.}, Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied. \par We exhibit an important gap between logics where subscripts of the form {"}\(= c\){"} (exact duration) are allowed, and simpler logics that only allow subscripts of the form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded duration).\par Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes \(\Delta_{2}^{P}\)-complete or PSPACE-complete depending on the considered semantics.}, } |

[MR06] | Nicolas Markey and
Jean-François Raskin.
Model Checking Restricted Sets of Timed Paths.
Theoretical Computer Science 358(2-3):273-292. Elsevier, August 2006.
- Abstract
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.
@article{tcs358(2-3)-MR, author = {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois}, title = {Model Checking Restricted Sets of Timed Paths}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {358}, number = {2-3}, pages = {273-292}, year = {2006}, month = aug, doi = {10.1016/j.tcs.2006.01.019}, abstract = {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 \textit{(i)}~a~single finite (or ultimately periodic) timed path, \textit{(ii)}~an~infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, \textit{(iii)}~an~infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph. \par 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.}, } |

[MS06] | Nicolas Markey and
Philippe Schnoebelen.
Mu-calculus path checking.
Information Processing Letters 97(6):225-230. Elsevier, March 2006.
- Abstract
We investigate the path model checking problem for the μ-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the μ-calculus.
@article{ipl97(6)-MS, author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Mu-calculus path checking}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {97}, number = {6}, pages = {225-230}, year = {2006}, month = mar, doi = {10.1016/j.ipl.2005.11.010}, abstract = {We investigate the path model checking problem for the \(\mu\)-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the \(\mu\)-calculus.}, } |

[BLM+06] | Patricia Bouyer,
Kim Guldstrand Larsen,
Nicolas Markey, and
Jacob Illum Rasmussen.
Almost Optimal Strategies in One-Clock Priced Timed
Automata.
In FSTTCS'06,
Lecture Notes in Computer Science 4337, pages 345-356. Springer-Verlag, December 2006.
- Abstract
We consider timed games extended with cost information, and prove computability of the optimal cost and of ε-optimal memoryless strategies in timed games with one clock. In contrast, this problem has recently been proved undecidable for timed games with three clocks.
@inproceedings{fsttcs2006-BLMR, author = {Bouyer, Patricia and Larsen, Kim Guldstrand and Markey, Nicolas and Rasmussen, Jacob Illum}, title = {Almost Optimal Strategies in One-Clock Priced Timed Automata}, editor = {Arun-Kumar, S. and Garg, Naveen}, booktitle = {{P}roceedings of the 26th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)}, acronym = {{FSTTCS}'06}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4337}, pages = {345-356}, year = {2006}, month = dec, doi = {10.1007/11944836_32}, abstract = {We consider timed games extended with cost information, and prove computability of the optimal cost and of \(\epsilon\)-optimal memoryless strategies in timed games with one~clock. In~contrast, this problem has recently been proved undecidable for timed games with three clocks.}, } |

[BMR06] | Patricia Bouyer,
Nicolas Markey, and
Pierre-Alain Reynier.
Robust Model-Checking of Linear-Time Properties in
Timed Automata.
In LATIN'06,
Lecture Notes in Computer Science 3887, pages 238-249. Springer-Verlag, March 2006.
- Abstract
Formal verification of timed systems is well understood, but their *implementation*is still challenging. Recent works by Raskin*et al.*have brought out a model of parameterized timed automata that can be used to prove*implementability*of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of Büchi-like and LTL properties. We also verify bounded-response-time properties.
@inproceedings{latin2006-BMR, author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Robust Model-Checking of Linear-Time Properties in Timed Automata}, editor = {Correa, Jos{\'e} R. and Hevia, Alejandro and Kiwi, Marcos}, booktitle = {{P}roceedings of the 7th {L}atin {A}merican {S}ymposium on {T}heoretical {IN}formatics ({LATIN}'06)}, acronym = {{LATIN}'06}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3887}, pages = {238-249}, year = {2006}, month = mar, doi = {10.1007/11682462_25}, abstract = {Formal verification of timed systems is well understood, but their \emph{implementation} is still challenging. Recent works by Raskin \emph{et al.} have brought out a model of parameterized timed automata that can be used to prove \emph{implementability} of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of B{\"u}chi-like and LTL properties. We also verify bounded-response-time properties.}, } |

[LMO06] | François Laroussinie,
Nicolas Markey, and
Ghassan Oreiby.
Model-Checking Timed ATL for Durational Concurrent
Game Structures.
In FORMATS'06,
Lecture Notes in Computer Science 4202, pages 245-259. Springer-Verlag, September 2006.
- Abstract
We extend the framework of ATL model-checking to "simply timed" concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.
@inproceedings{formats2006-LMO, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Oreiby, Ghassan}, title = {Model-Checking Timed~{ATL} for Durational Concurrent Game Structures}, editor = {Asarin, Eugene and Bouyer, Patricia}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, acronym = {{FORMATS}'06}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {4202}, pages = {245-259}, year = {2006}, month = sep, doi = {10.1007/11867340_18}, abstract = {We extend the framework of ATL model-checking to {"}simply timed{"} concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.}, } |

2005 | |

[BCM05] | Patricia Bouyer,
Fabrice Chevalier, and
Nicolas Markey.
On the Expressiveness of TPTL and MTL.
In FSTTCS'05,
Lecture Notes in Computer Science 3821, pages 432-443. Springer-Verlag, December 2005.
- Abstract
TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the **F**modality can be translated into MTL.
@inproceedings{fsttcs2005-BCM, author = {Bouyer, Patricia and Chevalier, Fabrice and Markey, Nicolas}, title = {On the Expressiveness of {TPTL} and {MTL}}, editor = {Ramanujam, R. and Sen, Sandeep}, booktitle = {{P}roceedings of the 25th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'05)}, acronym = {{FSTTCS}'05}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3821}, pages = {432-443}, year = {2005}, month = dec, doi = {10.1007/11590156_35}, abstract = {TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the \textbf{F} modality can be translated into MTL.}, } |

[AMR+05] | Karine Altisen,
Nicolas Markey,
Pierre-Alain Reynier, and
Stavros Tripakis.
Implémentabilité des automates
temporisés.
In MSR'05,
pages 395-406.
Hermès, October 2005.
@inproceedings{msr2005-AMRT, author = {Altisen, Karine and Markey, Nicolas and Reynier, Pierre-Alain and Tripakis, Stavros}, title = {Impl{\'e}mentabilit{\'e} des automates temporis{\'e}s}, editor = {Alla, Hassane and Rutten, {\'E}ric}, booktitle = {{A}ctes du 5{\`e}me {C}olloque {F}rancophone sur la {M}od{\'e}lisation des {S}yst{\`e}mes r{\'e}actifs ({MSR}'05)}, acronym = {{MSR}'05}, publisher = {Herm{\`e}s}, pages = {395-406}, year = {2005}, month = oct, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf}, } |

2004 | |

[Mar04] | Nicolas Markey.
Past is for Free: On the Complexity of Verifying
Linear Temporal Properties with Past.
Acta Informatica 40(6-7):431-458. Springer-Verlag, May 2004.
- Abstract
We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that "past is for free", in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.
@article{acta40(6-7)-Mar, author = {Markey, Nicolas}, title = {Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past}, publisher = {Springer-Verlag}, journal = {Acta Informatica}, volume = {40}, number = {6-7}, pages = {431-458}, year = {2004}, month = may, doi = {10.1007/s00236-003-0136-5}, abstract = {We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that {"}past is for free{"}, in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.}, } |

[MS04] | Nicolas Markey and
Philippe Schnoebelen.
A PTIME-Complete Matching Problem for
SLP-Compressed Words.
Information Processing Letters 90(1):3-6. Elsevier, April 2004.
- Abstract
SLP-compressed words are words given by simple deterministic grammars called "straight-line programs". We prove that the problem of deciding whether an SLP-compressed word is recognized by a FSA is complete for polynomial-time.
@article{ipl90(1)-MS, author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {A {PTIME}-Complete Matching Problem for {SLP}-Compressed Words}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {90}, number = {1}, pages = {3-6}, year = {2004}, month = apr, doi = {10.1016/j.ipl.2004.01.002}, abstract = {SLP-compressed words are words given by simple deterministic grammars called {"}straight-line programs{"}. We prove that the problem of deciding whether an SLP-compressed word is recognized by a FSA is complete for polynomial-time.}, } |

[DCM+04] | Jennifer M. Davoren,
Vaughan Coulthard,
Nicolas Markey, and
Thomas Moor.
Non-deterministic Temporal Logics for General Flow
Systems.
In HSCC'04,
Lecture Notes in Computer Science 2993, pages 280-295. Springer-Verlag, March 2004.
- Abstract
In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discrete-time transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.
@inproceedings{hscc2004-DCMM, author = {Davoren, Jennifer M. and Coulthard, Vaughan and Markey, Nicolas and Moor, Thomas}, title = {Non-deterministic Temporal Logics for General Flow Systems}, editor = {Alur, Rajeev and Pappas, George J.}, booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on {H}ybrid {S}ystems: {C}omputation and {C}ontrol ({HSCC}'04)}, acronym = {{HSCC}'04}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2993}, pages = {280-295}, year = {2004}, month = mar, doi = {10.1007/978-3-540-24743-2_19}, abstract = {In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discrete-time transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL\(^*\), which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL\(^*\), but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL\(^*\) and establish its soundness w.r.t. the general flow semantics.}, } |

[DDM+04] | Martin De Wulf,
Laurent Doyen,
Nicolas Markey, and
Jean-François Raskin.
Robustness and Implementability of Timed Automata.
In FORMATS-FTRTFT'04,
Lecture Notes in Computer Science 3253, pages 118-133. Springer-Verlag, September 2004.
- Abstract
In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by Δ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter Δ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a Δ. We show that this question is closely related to a notion of robustness for timed automata defined in (A. Puri: *Dynamical Properties of Timed Automata*. FTRTFT, 1998) and prove that the implementability problem is decidable.
@inproceedings{ftrtft2004-DDMR, author = {De{~}Wulf, Martin and Doyen, Laurent and Markey, Nicolas and Raskin, Jean-Fran{\c c}ois}, title = {Robustness and Implementability of Timed Automata}, editor = {Lakhnech, Yassine and Yovine, Sergio}, booktitle = {{P}roceedings of the {J}oint {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal {T}echniques in {R}eal-Time and {F}ault-Tolerant {S}ystems ({FTRTFT}'04)}, acronym = {{FORMATS-FTRTFT}'04}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3253}, pages = {118-133}, year = {2004}, month = sep, doi = {10.1007/978-3-540-30206-3_10}, abstract = {In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by \(\Delta\) to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter \(\Delta\) for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a \(\Delta\). We show that this question is closely related to a notion of robustness for timed automata defined in (A.~Puri: \textit{Dynamical Properties of Timed Automata}. FTRTFT, 1998) and prove that the implementability problem is decidable.}, } |

[LMS04] | François Laroussinie,
Nicolas Markey, and
Philippe Schnoebelen.
Model Checking Timed Automata with One or Two
Clocks.
In CONCUR'04,
Lecture Notes in Computer Science 3170, pages 387-401. Springer-Verlag, August 2004.
- Abstract
In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL, over TAs with one clock or two clocks. First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL, over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.
@inproceedings{concur2004-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Model Checking Timed Automata with One or Two Clocks}, editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'04)}, acronym = {{CONCUR}'04}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3170}, pages = {387-401}, year = {2004}, month = aug, doi = {10.1007/978-3-540-28644-8_25}, abstract = {In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL, over TAs with one clock or two clocks.\par First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL, over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.}, } |

[MR04] | Nicolas Markey and
Jean-François Raskin.
Model Checking Restricted Sets of Timed Paths.
In CONCUR'04,
Lecture Notes in Computer Science 3170, pages 432-447. Springer-Verlag, August 2004.
- Abstract
In this paper, we study the complexity of model-checking formulas of three important real-time logics (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)*a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph,*(iii)*a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.
@inproceedings{concur2004-MR, author = {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois}, title = {Model Checking Restricted Sets of Timed Paths}, editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'04)}, acronym = {{CONCUR}'04}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3170}, pages = {432-447}, year = {2004}, month = aug, doi = {10.1007/978-3-540-28644-8_28}, abstract = {In this paper, we study the complexity of model-checking formulas of three important real-time logics (MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are \textit{(i)} a single finite (or ultimately periodic) timed path, \textit{(ii)} a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, \textit{(iii)} a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.}, } |

[MS04] | Nicolas Markey and
Philippe Schnoebelen.
Symbolic Model Checking for Simply Timed Systems.
In FORMATS-FTRTFT'04,
Lecture Notes in Computer Science 3253, pages 102-117. Springer-Verlag, September 2004.
- Abstract
We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).
@inproceedings{formats2004-MS, author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Symbolic Model Checking for Simply Timed Systems}, editor = {Lakhnech, Yassine and Yovine, Sergio}, booktitle = {{P}roceedings of the {J}oint {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal {T}echniques in {R}eal-Time and {F}ault-Tolerant {S}ystems ({FTRTFT}'04)}, acronym = {{FORMATS-FTRTFT}'04}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3253}, pages = {102-117}, year = {2004}, month = sep, doi = {10.1007/978-3-540-30206-3_9}, abstract = {We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A~simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).}, } |

[Mar04] | Nicolas Markey.
TSMV : model-checking symbolique de systémes
simplement temporisés.
In AFADL'04.
June 2004.
@inproceedings{afadl2004-Mar, author = {Markey, Nicolas}, title = {{TSMV}~: model-checking symbolique de syst{\'e}mes simplement temporis{\'e}s}, editor = {Julliand, Jacques}, booktitle = {Actes de la 6\`eme Conf\'erence {A}pproches {F}ormelles dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels ({AFADL}'04)}, acronym = {{AFADL}'04}, year = {2004}, month = jun, } |

[MS04] | Nicolas Markey and
Philippe Schnoebelen.
TSMV: Symbolic Model Checking for Simply Timed
Systems.
In QEST'04,
pages 330-331.
IEEE Comp. Soc. Press, September 2004.
- Abstract
TSMV is an extension of NuSMV, the open-source symbolic model checker, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries an integer duration (possibly zero). This simple model supports efficient symbolic algorithms for RTCTL formulae.
@inproceedings{qest2004-MS, author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {{TSMV}: Symbolic Model Checking for Simply Timed Systems}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'04)}, acronym = {{QEST}'04}, publisher = {IEEE Comp. Soc. Press}, pages = {330-331}, year = {2004}, month = sep, doi = {10.1109/QEST.2004.1348052}, abstract = {TSMV is an extension of NuSMV, the open-source symbolic model checker, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries an integer duration (possibly zero). This simple model supports efficient symbolic algorithms for RTCTL formulae.}, } |

2003 | |

[Mar03] | Nicolas Markey.
Temporal Logic with Past is Exponentially More
Succinct.
EATCS Bulletin 79:122-128. EATCS, February 2003.
- Abstract
We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.
@article{eatcs-bull79()-Mar, author = {Markey, Nicolas}, title = {Temporal Logic with Past is Exponentially More Succinct}, publisher = {EATCS}, journal = {EATCS Bulletin}, volume = {79}, pages = {122-128}, year = {2003}, month = feb, abstract = {We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.}, } |

[MS03] | Nicolas Markey and
Philippe Schnoebelen.
Model Checking a Path (Preliminary Report).
In CONCUR'03,
Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, August 2003.
- Abstract
We consider the problem of checking whether a finite (or ultimately periodic) run satisfies a temporal logic formula. This problem is at the heart of "runtime verification" but it also appears in many other situations. By considering several extended temporal logics, we show that the problem of model checking a path can usually be solved efficiently, and profit from specialized algorithms. We further show it is possible to efficiently check paths given in compressed form.
@inproceedings{concur2003-MS, author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Model Checking a Path (Preliminary Report)}, editor = {Amadio, Roberto and Lugiez, Denis}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'03)}, acronym = {{CONCUR}'03}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2761}, pages = {251-265}, year = {2003}, month = aug, doi = {10.1007/978-3-540-45187-7_17}, abstract = {We consider the problem of checking whether a finite (or ultimately periodic) run satisfies a temporal logic formula. This problem is at the heart of {"}runtime verification{"} but it also appears in many other situations. By considering several extended temporal logics, we show that the problem of model checking a path can usually be solved efficiently, and profit from specialized algorithms. We further show it is possible to efficiently check paths given in compressed form.}, } |

[Mar03] | Nicolas Markey.
Logiques temporelles pour la vérification :
expressivité, complexité, algorithmes.
Thèse de doctorat,
Lab. Informatique Fondamentale d'Orléans,
France,
April 2003.
@phdthesis{phd2003-Mar, author = {Markey, Nicolas}, title = {Logiques temporelles pour la v{\'e}rification~: expressivit{\'e}, complexit{\'e}, algorithmes}, year = {2003}, month = apr, school = {Lab.~Informatique Fondamentale d'Orl{\'e}ans, France}, type = {Th\`ese de doctorat}, } |

2002 | |

[LMS02] | François Laroussinie,
Nicolas Markey, and
Philippe Schnoebelen.
On Model Checking Durational Kripke Structures
(Extended Abstract).
In FoSSaCS'02,
Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, April 2002.
- Abstract
We consider quantitative model checking in *durational Kripke structures*(Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).A surprising outcome of this study is that it provides the second example of a Δ2P-complete model checking problem.
@inproceedings{fossacs2002-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {On Model Checking Durational {K}ripke Structures (Extended Abstract)}, editor = {Nielsen, Mogens and Engberg, Uffe}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'02)}, acronym = {{FoSSaCS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2303}, pages = {264-279}, year = {2002}, month = apr, doi = {10.1007/3-540-45931-6_19}, abstract = {We consider quantitative model checking in \emph{durational Kripke structures} (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form {"}\(= c\){"} (exact duration) are allowed, and simpler logics that only allow subscripts of the form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded duration).\par A surprising outcome of this study is that it provides the second example of a \(\Delta_2^P\)-complete model checking problem.}, } |

[LMS02] | François Laroussinie,
Nicolas Markey, and
Philippe Schnoebelen.
Temporal Logic with Forgettable Past.
In LICS'02,
pages 383-392.
IEEE Comp. Soc. Press, July 2002.
- Abstract
We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.
@inproceedings{lics2002-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Temporal Logic with Forgettable Past}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {383-392}, year = {2002}, month = jul, doi = {10.1109/LICS.2002.1029846}, award = {Array}, abstract = {We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.}, } |

[Mar02] | Nicolas Markey.
Past is for Free: On the Complexity of Verifying
Linear Temporal Properties with Past.
In EXPRESS'02,
Electronic Notes in Theoretical Computer Science 68(2), pages 89-106. Elsevier, August 2002.
- Abstract
We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our results show that "past is for free", that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We also remark that existential and universal model-checking can have different complexity for certain fragments.
@inproceedings{express2002-Mar, author = {Markey, Nicolas}, title = {Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {89-106}, year = {2002}, month = aug, doi = {10.1016/S1571-0661(05)80366-4}, abstract = {We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past~(PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our~results show that {"}past is for free{"}, that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We~also remark that existential and universal model-checking can have different complexity for certain fragments.}, } |

2001 | |

[LMS01] | François Laroussinie,
Nicolas Markey, and
Philippe Schnoebelen.
Model Checking CTL+ and FCTL is hard.
In FoSSaCS'01,
Lecture Notes in Computer Science 2030, pages 318-331. Springer-Verlag, April 2001.
- Abstract
Among the branching-time temporal logics used for the specification and verification of systems, CTL+, FCTL and ECTL+ are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is Δ2p-complete.
@inproceedings{fossacs2001-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Model Checking {CTL}{\(^+\)} and {FCTL} is hard}, editor = {Honsell, Furio and Miculan, Marino}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'01)}, acronym = {{FoSSaCS}'01}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2030}, pages = {318-331}, year = {2001}, month = apr, doi = {10.1007/3-540-45315-6_21}, abstract = {Among the branching-time temporal logics used for the specification and verification of systems, CTL\(^+\), FCTL and ECTL\(^+\) are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is \(\Delta_2^p\)-complete.}, } |

- 68
- 18
- 16
- 15
- 12
- 7
- 7
- 7
- 6
- 6
- 6
- 5
- 5
- 5
- 5
- 5
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1