2017
[BMP+17] Patricia Bouyer, Nicolas Markey, Nicolas Perrin et Philipp Schlehuber-Caissier. Timed automata abstraction of switched dynamical systems using control funnels. Real-Time Systems 53(3):327-353. Kluwer Academic, mai 2017.
Résumé

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.},
}
[BMR+17] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen et Simon Laursen. Average-energy games. Acta Informatica. Springer-Verlag, 2017. À paraïtre.
Résumé

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{acta-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},
  year =                {2017},
  doi =                 {10.1007/s00236-016-0274-1},
  note =                {To~appear},
  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.},
}
[BMV17] Patricia Bouyer, Nicolas Markey et Steen Vester. Nash Equilibria in Symmetric Graph Games with Partial Observation. Information and Computation 254(2):238-258. Elsevier, juin 2017.
Résumé

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 et Martin Zimmermann. Bounding Average-energy Games. In FoSSaCS'17, Lecture Notes in Computer Science 10203, pages 179-195. Springer-Verlag, avril 2017.
Résumé

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 et Nicolas Markey. On the determinization of timed systems. In FORMATS'17, Lecture Notes in Computer Science 10419, pages 25-41. Springer-Verlag, septembre 2017.
Résumé

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 83, pages 84:1-84:3. Leibniz-Zentrum für Informatik, août 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 42th {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 =              {83},
  pages =               {84:1-84:3},
  year =                {2017},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2017.84},
}
[BFL+17] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine et James Worrell. Model Checking Real-Time Systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith et Roderick Bloem (eds.), Handbook of Model Checking. Springer-Verlag, 2017. À paraïtre.
Résumé

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{hmc2017-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},
  year =                {2017},
  note =                {To~appear},
  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).},
}
[BLM+17] Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine et James Worrell. Timed temporal logics. In Luca Aceto, Giorgio Bacci, Giovani Bacci, Anna Ingólfsdóttir, Axel Legay et 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, août 2017.
Résumé

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, Giovani
                         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-65764-6_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é et Nicolas Markey. Courcelle's Theorem Made Dynamic. Technical Report 1702.05183, arXiv, Février 2017.
Résumé

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.},
}
[GBM17] Patrick Gardy, Patricia Bouyer et Nicolas Markey. Dependences in Strategy Logic. Technical Report 1708.05849, arXiv, Août 2017.
Résumé

Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express 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. We study different kinds of dependences, refining the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014], and prove that they give rise to different satisfaction relations. In the setting where strategies may only depend on what they have observed, we identify a large fragment of SL for which we prove model checking can be performed in 2EXPTIME.

@techreport{arxiv1708.05849-GBM,
  author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Dependences in Strategy Logic},
  number =              {1708.05849},
  year =                {2017},
  month =               aug,
  institution =         {arXiv},
  abstract =            {Strategy Logic~(\textsf{SL}) is a very expressive
                         logic for specifying and verifying properties of
                         multi-agent systems: in~\textsf{SL}, one can
                         quantify over strategies, assign them to agents, and
                         express 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. We~study different kinds of
                         dependences, refining the approach of~[Mogavero
                         \emph{et~al.}, Reasoning about strategies: On~the
                         model-checking problem,~2014], and prove that they
                         give rise to different satisfaction relations.
                         In~the setting where strategies may only depend on
                         what they have observed, we~identify a large
                         fragment of~\textsf{SL} for which we prove model
                         checking can be performed in \textsf{2EXPTIME}.},
}
2016
[BGM16] Patricia Bouyer, Patrick Gardy et Nicolas Markey. On the semantics of Strategy Logic. Information Processing Letters 116(2):75-79. Elsevier, février 2016.
Résumé

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 et Nicolas Markey. Symbolic Optimal Reachability in Weighted Timed Automata. In CAV'16, Lecture Notes in Computer Science 9779, pages 513-530. Springer-Verlag, juillet 2016.
Résumé

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 et 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, juillet 2016.
Résumé

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 et 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. Septembre 2016.
Résumé

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 et 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, août 2016.
Résumé

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 et 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, avril 2016.
Résumé

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.47},
  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 et Ludovic Chamoin. Distributed Synthesis of State-Dependent Switching Control. In RP'16, Lecture Notes in Computer Science 9899, pages 119-133. Springer-Verlag, septembre 2016.
Résumé

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{ 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 et 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. Juillet 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{ 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 et 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, août 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 et Michael Ummels. Pure Nash Equilibria in Concurrent Games. Logical Methods in Computer Science 11(2:9). Juin 2015.
Résumé

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 et Ocan Sankur. Robust Reachability in Timed Automata and Games: A Game-based Approach. Theoretical Computer Science 563:43-74. Elsevier, janvier 2015.
Résumé

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 et Nicolas Markey. Augmenting ATL with strategy contexts. Information and Computation 245:98-123. Elsevier, décembre 2015.
Résumé

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é et Nicolas Markey. Language Preservation Problems in Parametric Timed Automata. In FORMATS'15, Lecture Notes in Computer Science 9268, pages 27-43. Springer-Verlag, septembre 2015.
Résumé

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 et 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, septembre 2015.
Résumé

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 et 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, décembre 2015.
Résumé

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 et 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, septembre 2015.
Résumé

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 et 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, septembre 2015.
Résumé

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 et Simon Laursen. Average-energy games. In GandALF'15, Electronic Proceedings in Theoretical Computer Science 193, pages 1-15. Septembre 2015.
Résumé

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 NPcoNP 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 et Arnaud Sangnier. ATLsc with partial observation. In GandALF'15, Electronic Proceedings in Theoretical Computer Science 193, pages 43-57. Septembre 2015.
Résumé

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 et Wolfgang Thomas (eds.) Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061). Dagstuhl Reports 5(2):1-25. Leibniz-Zentrum für Informatik, juin 2015.
Résumé

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–-mdash;as a special focus–-mdash;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 et Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. Performance Evaluation 73:91-109. Elsevier, mars 2014.
Résumé

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 et Nicolas Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science 10(4). Décembre 2014.
Résumé

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 et Nicolas Markey. Shrinking Timed Automata. Information and Computation 234:107-132. Elsevier, février 2014.
Résumé

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 et Nicolas Markey. Quantitative verification of weighted Kripke structures. In ATVA'14, Lecture Notes in Computer Science 8837, pages 64-80. Springer-Verlag, novembre 2014.
Résumé

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 et Raj Mohan Matteplackel. Averaging in LTL. In CONCUR'14, Lecture Notes in Computer Science 8704, pages 266-280. Springer-Verlag, septembre 2014.
Résumé

For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean–-mdash;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 et 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, décembre 2014.
Résumé

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 et Steen Vester. Nash Equilibria in Symmetric Games with Partial Observation. In SR'14, Electronic Proceedings in Theoretical Computer Science 146, pages 49-55. Mars 2014.
Résumé

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 et Mahsa Shrimohammadi. Synchronizing words for weighted and timed automata. In FSTTCS'14, Leibniz International Proceedings in Informatics 29, pages 121-132. Leibniz-Zentrum für Informatik, décembre 2014.
Résumé

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 Shrimohammadi,
                         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 et Steen Vester. Symmetry Reduction in Infinite Games with Finite Branching. In ATVA'14, Lecture Notes in Computer Science 8837, pages 281-296. Springer-Verlag, novembre 2014.
Résumé

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 et Nicolas Markey. Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata. In RTCSA'14. IEEE Comp. Soc. Press, août 2014.
Résumé

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, avril 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 et Ocan Sankur. Robust Weighted Timed Automata and Games. In FORMATS'13, Lecture Notes in Computer Science 8053, pages 31-46. Springer-Verlag, août 2013.
Résumé

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 et Nicolas Markey. Satisfiability of ATL with strategy contexts. In GandALF'13, Electronic Proceedings in Theoretical Computer Science 119, pages 208-223. Août 2013.
Résumé

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 et Pierre-Alain Reynier. Robust Controller Synthesis in Timed Automata. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 546-560. Springer-Verlag, août 2013.
Résumé

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 et Ocan Sankur. Robustness in timed automata. In RP'13, Lecture Notes in Computer Science 8169, pages 1-18. Springer-Verlag, septembre 2013.
Résumé

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 et James Worrell. On Termination and Invariance for Faulty Channel Systems. Formal Aspects of Computing 24(4-6):595-607. Springer-Verlag, juillet 2012.
Résumé

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 et Michael Ummels. Concurrent games with ordered objectives. In FoSSaCS'12, Lecture Notes in Computer Science 7213, pages 301-315. Springer-Verlag, mars 2012.
Résumé

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 et Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. In QEST'12, pages 128-137. IEEE Comp. Soc. Press, septembre 2012.
Résumé

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–-mdash;for us somewhat unexpectedly–-mdash;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 et 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, juillet 2012.
Résumé

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 et Nicolas Markey. Quantified CTL: Expressiveness and Model Checking. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 177-192. Springer-Verlag, septembre 2012.
Résumé

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 et 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, octobre 2012.
Résumé

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 et Nicolas Markey. Quantitative analysis of real-time systems using priced timed automata. Communications of the ACM 54(9):78-87. ACM Press, septembre 2011.
Résumé

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 et 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, décembre 2011.
Résumé

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 et Claus Thrane. Timed automata can always be made implementable. In CONCUR'11, Lecture Notes in Computer Science 6901, pages 76-91. Springer-Verlag, septembre 2011.
Résumé

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 et 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, octobre 2011.
Résumé

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 et 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, septembre 2011.
Résumé

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 et Nicolas Markey. Shrinking Timed Automata. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 90-102. Leibniz-Zentrum für Informatik, décembre 2011.
Résumé

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, juin 2011.
Résumé

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, Avril 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 et Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2):97-116. Elsevier, février 2010.
Résumé

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 et Ghassan Oreiby. Using Model Checking for Analyzing Distributed Power Control Problems. EURASIP Journal on Wireless Communications and Networking 2010(861472). Hindawi Publishing Corp., juin 2010.
Résumé

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 et 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, septembre 2010.
Résumé

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 et 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, septembre 2010.
Résumé

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 et Nicolas Markey. Timed Automata with Observers under Energy Constraints. In HSCC'10, pages 61-70. ACM Press, avril 2010.
Résumé

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 et 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, décembre 2010.
Résumé

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 et 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, décembre 2010.
Résumé

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, CiXi. 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 et Jef Wijsen (eds.) Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10). IEEE Comp. Soc. Press, septembre 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 et Nicolas Markey. ATL with Strategy Contexts and Bounded Memory. In LFCS'09, Lecture Notes in Computer Science 5407, pages 92-106. Springer-Verlag, janvier 2009.
Résumé

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 et Gabriel Renault. Measuring Permissivity in Finite Games. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 196-210. Springer-Verlag, septembre 2009.
Résumé

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 et Nicolas Markey. Control of Timed Systems. In Claude Jard et Olivier H. Roux (eds.), Communicating Embedded Systems – Software and Design. Wiley-ISTE, octobre 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 et Nicolas Markey. Model Checking One-clock Priced Timed Automata. Logical Methods in Computer Science 4(2). Mai 2008.
Résumé

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 et Jean-François Raskin. Robust Safety of Timed Automata. Formal Methods in System Design 33(1-3):45-84. Springer-Verlag, décembre 2008.
Résumé

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 et Ghassan Oreiby. On the Expressiveness and Complexity of ATL. Logical Methods in Computer Science 4(2). Mai 2008.
Résumé

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 et Nicolas Markey. Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. In QEST'08, pages 55-64. IEEE Comp. Soc. Press, septembre 2008.
Résumé

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 et 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, septembre 2008.
Résumé

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{
                         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 et Lionel Rieg. Good friends are hard to find!. In TIME'08, pages 32-40. IEEE Comp. Soc. Press, juin 2008.
Résumé

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 et 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, février 2008.
Résumé

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 et 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, juillet 2008.
Résumé

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 et 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, mars 2008.
Résumé

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 et Nicolas Markey. Contrôle des systèmes temporisés. In Olivier H. Roux et Claude Jard (eds.), Approches formelles des systèmes embarqués communicants. Hermès, octobre 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://www.lavoisier.fr/notice/fr335499.html},
}
2007
[BLM07] Patricia Bouyer, Kim Guldstrand Larsen et Nicolas Markey. Model Checking One-clock Priced Timed Automata. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 108-122. Springer-Verlag, mars 2007.
Résumé

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 et Ghassan Oreiby. Timed Concurrent Game Structures. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 445-459. Springer-Verlag, septembre 2007.
Résumé

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 et Nicolas Markey. Costs are Expensive!. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 53-68. Springer-Verlag, octobre 2007.
Résumé

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 et James Worrell. The Cost of Punctuality. In LICS'07, pages 109-118. IEEE Comp. Soc. Press, juillet 2007.
Résumé

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 et Ghassan Oreiby. On the Expressiveness and Complexity of ATL. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 243-257. Springer-Verlag, mars 2007.
Résumé

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 et Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5):188-194. Elsevier, juin 2006.
Résumé

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 et Philippe Schnoebelen. Efficient timed model checking for discrete-time systems. Theoretical Computer Science 353(1-3):249-271. Elsevier, mars 2006.
Résumé

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 et Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. Theoretical Computer Science 358(2-3):273-292. Elsevier, août 2006.
Résumé

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 et Philippe Schnoebelen. Mu-calculus path checking. Information Processing Letters 97(6):225-230. Elsevier, mars 2006.
Résumé

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 et 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, décembre 2006.
Résumé

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 et 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, mars 2006.
Résumé

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 et 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, septembre 2006.
Résumé

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 et Nicolas Markey. On the Expressiveness of TPTL and MTL. In FSTTCS'05, Lecture Notes in Computer Science 3821, pages 432-443. Springer-Verlag, décembre 2005.
Résumé

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 et Stavros Tripakis. Implémentabilité des automates temporisés. In MSR'05, pages 395-406. Hermès, octobre 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, mai 2004.
Résumé

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 et Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1):3-6. Elsevier, avril 2004.
Résumé

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] Jenifer Davoren, Vaughan Coulthard, Nicolas Markey et Thomas Moor. Non-deterministic Temporal Logics for General Flow Systems. In HSCC'04, Lecture Notes in Computer Science 2993, pages 280-295. Springer-Verlag, mars 2004.
Résumé

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, Jenifer and Coulthard, Vaughan and Markey,
                         Nicolas and Moor, {\relax Th}omas},
  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 et 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, septembre 2004.
Résumé

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 et 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, août 2004.
Résumé

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 et 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, août 2004.
Résumé

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 et Philippe Schnoebelen. Symbolic Model Checking for Simply Timed Systems. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 102-117. Springer-Verlag, septembre 2004.
Résumé

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. Juin 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 et Philippe Schnoebelen. TSMV: Symbolic Model Checking for Simply Timed Systems. In QEST'04, pages 330-331. IEEE Comp. Soc. Press, septembre 2004.
Résumé

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, février 2003.
Résumé

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 et Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In CONCUR'03, Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, août 2003.
Résumé

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, Avril 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 et Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, avril 2002.
Résumé

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 et Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Comp. Soc. Press, juillet 2002.
Résumé

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},
  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, août 2002.
Résumé

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 et Philippe Schnoebelen. Model Checking CTL+ and FCTL is hard. In FoSSaCS'01, Lecture Notes in Computer Science 2030, pages 318-331. Springer-Verlag, avril 2001.
Résumé

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.},
}