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

The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We demonstrate the potential of our approach with three examples.

@article{rts53(3)-BMPS,
author =              {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title =               {Timed automata abstraction of switched dynamical
systems using control funnels},
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, and Simon Laursen. Average-energy games. Acta Informatica. Springer-Verlag, 2017. 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 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, and Steen Vester. Nash Equilibria in Symmetric Graph Games with Partial Observation. Information and Computation 254(2):238-258. Elsevier, June 2017.
Abstract

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.

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

[BHM+17] Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding Average-energy Games. In FoSSaCS'17, Lecture Notes in Computer Science 10203, pages 179-195. Springer-Verlag, April 2017.
Abstract

We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies.

By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.

Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.

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

[BJM17] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the determinization of timed systems. In FORMATS'17, Lecture Notes in Computer Science 10419. Springer-Verlag, September 2017. To appear.
Abstract

We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.

@inproceedings{formats2017-BJM,
author =              {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title =               {On the determinization of timed systems},
editor =              {Abate, Alessandro and Geeraerts, Gilles},
booktitle =           {{P}roceedings of the 15th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'17)},
acronym =             {{FORMATS}'17},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {10419},
year =                {2017},
month =               sep,
doi =                 {10.1007/978-3-319-65765-3 2},
note =                {To~appear},
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.},
}

[BFL+17] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine, and James Worrell. Model Checking Real-Time Systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds.), Handbook of Model Checking. Springer-Verlag, 2017. 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).

@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, and James Worrell. Timed temporal logics. In Luca Aceto, Giorgio Bacci, Giovani Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare (eds.), Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 10460, pages 211-230. Springer-Verlag, August 2017.
Abstract

Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.

@incollection{kimfest2017-BLMOW,
author =              {Bouyer, Patricia and Laroussinie, Fran{\c c}ois and
Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
James},
title =               {Timed temporal logics},
editor =              {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
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.},
}

[GBM17] Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. Technical Report 1708.05849, arXiv, August 2017.
Abstract

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
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, and Nicolas Markey. On the semantics of Strategy Logic. Information Processing Letters 116(2):75-79. Elsevier, February 2016.
Abstract

We define and study a slight variation on the semantics of Strategy Logic: while in the classical semantics, all strategies are shifted during the evaluation of temporal modalities, we propose to only shift the strategies that have been assigned to a player, thus matching the intuition that we can assign the very same strategy to the players at different points in time. We prove that surprisingly, this renders the model-checking problem undecidable.

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

[BCM16] Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic Optimal Reachability in Weighted Timed Automata. In CAV'16, Lecture Notes in Computer Science 9779, pages 513-530. Springer-Verlag, July 2016.
Abstract

Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.

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

[BMR+16] Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in Networks of Register Protocols under Stochastic Schedulers. In ICALP'16, Leibniz International Proceedings in Informatics 55, pages 106:1-106:14. Leibniz-Zentrum für Informatik, July 2016.
Abstract

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property : the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.

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

[BMS16] Patricia Bouyer, Nicolas Markey, and Daniel Stan. Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games. In GandALF'16, Electronic Proceedings in Theoretical Computer Science 226, pages 61-75. September 2016.
Abstract

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

@inproceedings{gandalf2016-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title =               {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
editor =              {Cantone, Domenico and Delzanno, Giorgio},
booktitle =           {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'16)},
acronym =             {{GandALF}'16},
series =              {Electronic Proceedings in Theoretical Computer
Science},
volume =              {226},
pages =               {61-75},
year =                {2016},
month =               sep,
doi =                 {10.4204/EPTCS.226.5},
abstract =            {We study the existence of mixed-strategy equilibria
in concurrent games played on graphs. While
existence is guaranteed with safety objectives for
each player, Nash equilibria need not exist when
players are given arbitrary terminal-reward
objectives, and their existence is undecidable with
qualitative reachability objectives (and~only three
players). However, these results rely on the fact
that the players can enforce infinite plays while
trying to improve their payoffs. In this paper, we
introduce a relaxed notion of equilibria, where
deviations are imprecise. We prove that contrary to
Nash equilibria, such (stationary) equilibria always
exist, and we develop a PSPACE algorithm to compute
one.},
}

[DLM16] Amélie David, François Laroussinie, and Nicolas Markey. On the expressiveness of QCTL. In CONCUR'16, Leibniz International Proceedings in Informatics 59, pages 28:1-28:15. Leibniz-Zentrum für Informatik, August 2016.
Abstract

QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTLk, with at most k nested blocks of quantifiers, is k+1-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QCTLk collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).

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

[FKM16] Laurent Fribourg, Ulrich Kühne, and Nicolas Markey. Game-based Synthesis of Distributed Controllers for Sampled Switched Systems. In SynCoP'15, OpenAccess Series in Informatics 44, pages 47-61. Leibniz-Zentrum für Informatik, April 2016.
Abstract

Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with each other and with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In this paper, we consider a controller synthesis method based on state space decomposition, and propose a game-based approach in order to extend it within a distributed framework.

@inproceedings{syncop2015-FKM,
author =              {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey,
Nicolas},
title =               {Game-based Synthesis of Distributed Controllers for
Sampled Switched Systems},
editor =              {Andr{\'e}, {\'E}tienne and Frehse, Goran},
booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}ynthesis of {C}omplex {P}arameters
({S}yn{C}o{P}'15)},
acronym =             {{S}yn{C}o{P}'15},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {OpenAccess Series in Informatics},
volume =              {44},
pages =               {47-61},
year =                {2016},
month =               apr,
doi =                 {10.4230/OASIcs.SynCoP.2015.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, and Ludovic Chamoin. Distributed Synthesis of State-Dependent Switching Control. In RP'16, Lecture Notes in Computer Science 9899, pages 119-133. Springer-Verlag, September 2016.
Abstract

We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting at R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 211 = 2048 switching modes.

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

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

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

2015
[BBM+15] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash Equilibria in Concurrent Games. Logical Methods in Computer Science 11(2:9). June 2015.
Abstract

We study pure-strategy Nash equilibria in multiplayer concurrent games, for a variety of omega-regular objectives. For simple objectives (e.g. reachability, Büchi objectives), we transform the problem of deciding the existence of a Nash equilibrium in a given concurrent game into that of deciding the existence of a winning strategy in a turn-based two-player game (with a refined objective). We use that transformation to design algorithms for computing Nash equilibria, which in most cases have optimal worst-case complexity. For automata-defined objectives, we extend the above algorithms using a simulation relation which allows us to consider the product of the game with the automata defining the objectives. Building on previous algorithms for simple qualitative objectives, we define and study a semi-quantitative framework, where all players have several boolean objectives equipped with a preorder; a player may for instance want to satisfy all her objectives, or to maximise the number of objectives that she achieves. In most cases, we prove that the algorithms we obtain match the complexity of the problem they address.

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

[BMS15] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust Reachability in Timed Automata and Games: A Game-based Approach. Theoretical Computer Science 563:43-74. Elsevier, January 2015.
Abstract

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

@article{tcs563()-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robust Reachability in Timed Automata and Games:
A~Game-based Approach},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {563},
pages =               {43-74},
year =                {2015},
month =               jan,
doi =                 {10.1016/j.tcs.2014.08.014},
abstract =            {Reachability checking is one of the most basic
problems in verification. By solving this problem in
a game, one can synthesize a strategy that dictates
the actions to be performed for ensuring that the
target location is reached. In this work, we are
interested in synthesizing {"}robust{"} strategies
for ensuring reachability of a location in timed
automata. By robust, we mean that it must still
ensure reachability even when the delays are
perturbed by the environment. We model this
perturbed semantics as a game between the controller
and its environment, and solve the parameterized
robust reachability problem: we show that the
existence of an upper bound on the perturbations
under which there is a strategy reaching a target
location is EXPTIME-complete. We also extend our
algorithm, with the same complexity, to turn-based
timed games, where the successor state is entirely
determined by the environment in some locations.},
}

[LM15] François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts. Information and Computation 245:98-123. Elsevier, December 2015.
Abstract

We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies.

We show that our extension ATLsc is very expressive, but that its decision problems are quite hard: model checking is k-EXPTIME-complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.

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

[AM15] Étienne André and Nicolas Markey. Language Preservation Problems in Parametric Timed Automata. In FORMATS'15, Lecture Notes in Computer Science 9268, pages 27-43. Springer-Verlag, September 2015.
Abstract

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.

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

[BFM15] Patricia Bouyer, Erwin Fang, and Nicolas Markey. Permissive strategies in timed automata and games. In AVOCS'15, Electronic Communications of the EASST 72. European Association of Software Science and Technology, September 2015.
Abstract

Timed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now very well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have recently been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a new approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies return an interval of possible dates when to play the selected action. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata.

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

[BGM15] Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted strategy logic with boolean goals over one-counter games. In FSTTCS'15, Leibniz International Proceedings in Informatics 45, pages 69-83. Leibniz-Zentrum für Informatik, December 2015.
Abstract

Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero et al. Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.

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

[BJM15] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In CONCUR'15, Leibniz International Proceedings in Informatics 42, pages 311-324. Leibniz-Zentrum für Informatik, September 2015.
Abstract

A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the cost for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal cost and almost-optimal strategies can be computed.

In this paper, we show that the value problem is undecidable in general weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. We then provide an algorithm to compute arbitrary approximations of the value in a game, and almost-optimal strategies. The algorithm applies in a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.

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

[BMP+15] Patricia Bouyer, Nicolas Markey, Nicolas Perrin, and Philipp Schlehuber-Caissier. Timed automata abstraction of switched dynamical systems using control funnels. In FORMATS'15, Lecture Notes in Computer Science 9268, pages 60-75. Springer-Verlag, September 2015.
Abstract

The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (the control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We demonstrate the potential of our approach with two examples.

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

[BMR+15] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen. Average-energy games. In GandALF'15, Electronic Proceedings in Theoretical Computer Science 193, pages 1-15. September 2015.
Abstract

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy.

We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in 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, and Arnaud Sangnier. ATLsc with partial observation. In GandALF'15, Electronic Proceedings in Theoretical Computer Science 193, pages 43-57. September 2015.
Abstract

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

@inproceedings{gandalf2015-LMS,
author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
Sangnier, Arnaud},
title =               {{{$$\textsf{ATL}_{\textsf{sc}}$$}} with partial
observation},
editor =              {Esparza, Javier and Tronci, Enrico},
booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'15)},
acronym =             {{GandALF}'15},
series =              {Electronic Proceedings in Theoretical Computer
Science},
volume =              {193},
pages =               {43-57},
year =                {2015},
month =               sep,
doi =                 {10.4204/EPTCS.193.4},
abstract =            {Alternating-time temporal logic with strategy
contexts ({{$$\textsf{ATL}_{\textsf{sc}}$$}}) is a
powerful formalism for expressing properties of
multi-agent systems: it~extends \textsf{CTL} with
\emph{strategy quantifiers}, offering a convenient
way of expressing both collaboration and antagonism
between several agents. Incomplete observation of
the state space is a desirable feature in such a
framework, but it quickly leads to undecidable
verification problems. In this paper, we prove that
\emph{uniform} incomplete observation (where all
players have the same observation) preserves
decidability of the model checking problem, even for
very expressive logics such as
{{$$\textsf{ATL}_{\textsf{sc}}$$}}.},
}

[CLM+15] Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas (eds.) Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061). Dagstuhl Reports 5(2):1-25. Leibniz-Zentrum für Informatik, June 2015.
Abstract

In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and–-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, and Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. Performance Evaluation 73:91-109. Elsevier, March 2014.
Abstract

We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-constrained run is–for us somewhat unexpectedly–undecidable for weighted timed automata with four or more clocks.

This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.

Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).

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

[LM14] François Laroussinie and Nicolas Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science 10(4). December 2014.
Abstract

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).

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

[SBM14] Ocan Sankur, Patricia Bouyer, and Nicolas Markey. Shrinking Timed Automata. Information and Computation 234:107-132. Elsevier, February 2014.
Abstract

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.

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

[BGM14] Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Quantitative verification of weighted Kripke structures. In ATVA'14, Lecture Notes in Computer Science 8837, pages 64-80. Springer-Verlag, November 2014.
Abstract

Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.

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

[BMM14] Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In CONCUR'14, Lecture Notes in Computer Science 8704, pages 266-280. Springer-Verlag, September 2014.
Abstract

For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean–-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, and Daniel Stan. Mixed Nash Equilibria in Concurrent Games. In FSTTCS'14, Leibniz International Proceedings in Informatics 29, pages 351-363. Leibniz-Zentrum für Informatik, December 2014.
Abstract

We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i) the undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii) the undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.

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

[BMV14] Patricia Bouyer, Nicolas Markey, and Steen Vester. Nash Equilibria in Symmetric Games with Partial Observation. In SR'14, Electronic Proceedings in Theoretical Computer Science 146, pages 49-55. March 2014.
Abstract

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.

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

[DJL+14] Laurent Doyen, Line Juhl, Kim Guldstrand Larsen, Nicolas Markey, and Mahsa 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, December 2014.
Abstract

The problem of synchronizing automata is concerned with the existence of a word that sends all states ofM the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete.

In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.

@inproceedings{fsttcs2014-DJLMS,
author =              {Doyen, Laurent and Juhl, Line and Larsen, Kim
Guldstrand and Markey, Nicolas and 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 and Steen Vester. Symmetry Reduction in Infinite Games with Finite Branching. In ATVA'14, Lecture Notes in Computer Science 8837, pages 281-296. Springer-Verlag, November 2014.
Abstract

Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL*, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL*.

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

[SLS+14] Youcheng Sun, Giuseppe Lipari, Romain Soulat, Laurent Fribourg, and Nicolas Markey. Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata. In RTCSA'14. IEEE Comp. Soc. Press, August 2014.
Abstract

Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns, etc.

In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium size components.

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

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

2013
[BMS13] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust Weighted Timed Automata and Games. In FORMATS'13, Lecture Notes in Computer Science 8053, pages 31-46. Springer-Verlag, August 2013.
Abstract

Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.

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

[LM13] François Laroussinie and Nicolas Markey. Satisfiability of ATL with strategy contexts. In GandALF'13, Electronic Proceedings in Theoretical Computer Science 119, pages 208-223. August 2013.
Abstract

Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts, while Strategy Logic has first-order quantification over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable.

We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to turn-based games. We prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we prove that restricting strategy quantification to memoryless strategies brings back undecidability.

@inproceedings{gandalf2013-LM,
author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title =               {Satisfiability of {ATL} with strategy contexts},
editor =              {Puppis, Gabriele and Villa, Tiziano},
booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'13)},
acronym =             {{GandALF}'13},
series =              {Electronic Proceedings in Theoretical Computer
Science},
volume =              {119},
pages =               {208-223},
year =                {2013},
month =               aug,
doi =                 {10.4204/EPTCS.119.18},
abstract =            {Various extensions of the temporal logic ATL have
recently been introduced to express rich properties
of multi-agent systems. Among these, ATLsc extends
ATL with \emph{strategy contexts}, while Strategy
Logic has \emph{first-order quantification} over
strategies. There is a price to pay for the rich
expressiveness of these logics: model-checking is
non-elementary, and satisfiability is
undecidable.\par We prove in this paper that
satisfiability is decidable in several special
cases. The most important one is when restricting to
\emph{turn-based} games. We~prove that decidability
also holds for concurrent games if the number of
moves available to the agents is bounded. Finally,
we~prove that restricting strategy quantification to
memoryless strategies brings back undecidability.},
}

[SBM+13] Ocan Sankur, Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Controller Synthesis in Timed Automata. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 546-560. Springer-Verlag, August 2013.
Abstract

We consider the fundamental problem of Büchi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.

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

[BMS13] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robustness in timed automata. In RP'13, Lecture Notes in Computer Science 8169, pages 1-18. Springer-Verlag, September 2013.
Abstract

In this paper we survey several approaches to the robustness of timed automata, that is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected.

We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.

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

2012
[BMO+12] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination and Invariance for Faulty Channel Systems. Formal Aspects of Computing 24(4-6):595-607. Springer-Verlag, July 2012.
Abstract

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
channel and write messages to the tail of a channel.
In this paper we focus on channel machines with
\emph{insertion errors}, i.e., machines in whose
channels messages can spontaneously appear. We
consider the invariance problem: does a given
insertion channel machine have an infinite
computation all of whose configurations satisfy a
given predicate? We show that this problem is
primitive-recursive if the predicate is closed under
message losses. We also give a non-elementary lower
bound for the invariance problem under this
restriction. Finally, using the previous result, we
show that the satisfiability problem for the safety
fragment of Metric Temporal Logic is
non-elementary.},
}

[BBM+12] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Concurrent games with ordered objectives. In FoSSaCS'12, Lecture Notes in Computer Science 7213, pages 301-315. Springer-Verlag, March 2012.
Abstract

We consider concurrent games played on graphs, in which each player has several qualitative (e.g. reachability or Büchi) objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled).

We study two fundamental problems in that setting: (1) the value problem, which aims at deciding the existence of a strategy that ensures a given payoff; (2) the Nash equilibrium problem, where we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We characterise the exact complexities of these problems for several relevant preorders, and several kinds of objectives.

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

[BLM12] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. In QEST'12, pages 128-137. IEEE Comp. Soc. Press, September 2012.
Abstract

We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from [Bouyer et al., "Infinite runs in weighted timed automata with energy constraints", FORMATS'08], we show that the existence of an infinite lower-bound-constrained run is–-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, and Ocan Sankur. Robust reachability in timed automata: a game-based approach. In ICALP'12, Lecture Notes in Computer Science 7392, pages 128-140. Springer-Verlag, July 2012.
Abstract

Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in a timed automaton; with "robust", we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete.

@inproceedings{icalp2012-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robust reachability in timed automata: a~game-based
approach},
editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
and Wattenhofer, Roger},
booktitle =           {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- Part~{II}},
acronym =             {{ICALP}'12},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {7392},
pages =               {128-140},
year =                {2012},
month =               jul,
doi =                 {10.1007/978-3-642-31585-5_15},
abstract =            {Reachability checking is one of the most basic
problems in verification. By solving this problem,
one synthesizes a strategy that dictates the actions
to be performed for ensuring that the target
location is reached. In this work, we are interested
in synthesizing {"}robust{"} strategies for ensuring
reachability of a location in a timed automaton;
with {"}robust{"}, we mean that it must still ensure
reachability even when the delays are perturbed by
the environment. We model this perturbed semantics
as a game between the controller and its
environment, and solve the parameterized robust
reachability problem: we show that the existence of
an upper bound on the perturbations under which
there is a strategy reaching a target location is
EXPTIME-complete.},
}

[DLM12] Arnaud Da Costa, François Laroussinie, and Nicolas Markey. Quantified CTL: Expressiveness and Model Checking. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 177-192. Springer-Verlag, September 2012.
Abstract

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking ATL-like temporal logics for games.

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

[SVM+12] Diego V. Simões De Sousa, Henrique Viana, Nicolas Markey, and Jose Antônio F. de Macêdo. Querying Trajectories through Model Checking based on Timed Automata. In SBBD'12, pages 33-40. Sociedade Brasileira de Computação, October 2012.
Abstract

The popularization of geographical position devices (e.g. GPS) creates new opportunities for analyzing behavior of moving objects. However, such analysis are hindered by a lack of semantic information associated to the basic information provided by GPS. Previous works propose semantic enrichment of trajectories. Through the semantic enrichment, we could check which trajectories have a given moving sequence in an application. Often, this sequence is expressed according to the semantic application, using the approach of semantic trajectories proposed in the literature. This trajectory can be represented as a sequence of predicates that holds in some time interval. However, the solutions for querying moving sequence proposed by previous works have a high computational cost. In this paper, we propose an expressive query language to semantic trajectories that allows temporal constraints. To evaluate a query we will use model checking based on timed automata, that can be performed in polynomial time. As this model checking algorithm is not implemented yet, we propose to use UPPAAL tool, that can be more expensive theoretically, but we expected that will be ecient for our approach. In addition, we will present a query example that demonstrates the expressive power of our language. Although in this paper we will focus on semantic trajectories data, our approach is general enough for being applied to other purposes.

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

2011
[BFL+11] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, and Nicolas Markey. Quantitative analysis of real-time systems using priced timed automata. Communications of the ACM 54(9):78-87. ACM Press, September 2011.
Abstract

The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nano-seconds to the weekly, monthly, or longer-range reactive planning in a factory or a supply chain.

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

[BBM+11] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Nash Equilibria in Concurrent Games with Büchi Objectives. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, December 2011.
Abstract

We study the problem of the existence (and computation) of Nash equilibria in multi-player concurrent games with Büchi-definable objectives. First, when the objectives are Büchi conditions on the game, we prove that the existence problem can be solved in polynomial time. In a second part, we extend our technique to objectives defined by deterministic Büchi automata, and prove that the problem then becomes EXPTIME-complete. We prove PSPACE-completeness for the case where the Büchi automata are 1-weak.

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

[BLM+11] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, Ocan Sankur, and Claus Thrane. Timed automata can always be made implementable. In CONCUR'11, Lecture Notes in Computer Science 6901, pages 76-91. Springer-Verlag, September 2011.
Abstract

Timed automata follow a mathematical semantics, which assumes perfect precision and synchrony of clocks. Since this hypothesis does not hold in digital systems, properties proven formally on a timed automaton may be lost at implementation. In order to ensure implementability, several approaches have been considered, corresponding to different hypotheses on the implementation platform. We address two of these: a timed automaton is samplable if its semantics is preserved under a discretization of time; it is robust if its semantics is preserved when all timing constraints are relaxed by some small positive parameter. We propose a construction which makes timed automata implementable in the above sense: From any timed automaton A, we build a timed automaton A' that exhibits the same behaviour as A, and moreover is both robust and samplable by construction.

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

[BMO+11] Patricia Bouyer, Nicolas Markey, Jörg Olschewski, and Michael Ummels. Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited. In ATVA'11, Lecture Notes in Computer Science 6996, pages 135-149. Springer-Verlag, October 2011.
Abstract

We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number/weight of transitions blocked by a strategy. Using a translation into mean-payoff parity games, we prove that deciding (the permissiveness of) a most permissive winning strategy is in NP∩coNP. Along the way, we provide a new study of mean-payoff parity games. In particular, we give a new algorithm for solving these games, which beats all previously known algorithms for this problem.

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

[BMS11] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust Model-Checking of Timed Automata via Pumping in Channel Machines. In FORMATS'11, Lecture Notes in Computer Science 6919, pages 97-112. Springer-Verlag, September 2011.
Abstract

Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satised by digital hardware on which the models are implemented. In fact, it was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system.

The problem of robust model-checking was then dened to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct.

In this work, we show that robust model-checking against ω-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of ω-regular properties, which is both optimal and valid for general timed automata.

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

[SBM11] Ocan Sankur, Patricia Bouyer, and Nicolas Markey. Shrinking Timed Automata. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 90-102. Leibniz-Zentrum für Informatik, December 2011.
Abstract

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata both properties are preserved in implementation.

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

[Mar11] Nicolas Markey. Robustness in Real-time Systems. In SIES'11, pages 28-34. IEEE Comp. Soc. Press, June 2011.
Abstract

We review several aspects of robustness of real-time systems, and present recent results on the robust verification of timed automata.

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

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

2010
[BCM10] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2):97-116. Elsevier, February 2010.
Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only modality F can be translated into MTL.

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

[BJL+10] Thomas Brihaye, Marc Jungers, Samson Lasaulce, Nicolas Markey, and Ghassan Oreiby. Using Model Checking for Analyzing Distributed Power Control Problems. EURASIP Journal on Wireless Communications and Networking 2010(861472). Hindawi Publishing Corp., June 2010.
Abstract

Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control (PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed PC. It turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.

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

[BBM10] Patricia Bouyer, Romain Brenguier, and Nicolas Markey. Nash Equilibria for Reachability Objectives in Multi-player Timed Games. In CONCUR'10, Lecture Notes in Computer Science 6269, pages 192-206. Springer-Verlag, September 2010.
Abstract

We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly infinite) concurrent games. Along the way, we use our characterization to compute Nash equilibria in finite concurrent games.

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

[BBM10] Patricia Bouyer, Romain Brenguier, and Nicolas Markey. Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games. In FORMATS'10, Lecture Notes in Computer Science 6246, pages 62-76. Springer-Verlag, September 2010.
Abstract

We study two-player timed games where the objectives of the two players are not opposite. We focus on the standard notion of Nash equilibrium and propose a series of transformations that builds two finite turn-based games out of a timed game, with a precise correspondence between Nash equilibria in the original and in final games. This provides us with an algorithm to compute Nash equilibria in two-player timed games for large classes of properties.

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

[BFL+10] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, and Nicolas Markey. Timed Automata with Observers under Energy Constraints. In HSCC'10, pages 61-70. ACM Press, April 2010.
Abstract

In this paper, we study one-clock priced timed automata in which prices can grow linearly (dp/dt=k) or exponentially (dp/dt=kp), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).

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

[DLM10] Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with strategy contexts: Expressiveness and Model Checking. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 120-132. Leibniz-Zentrum für Informatik, December 2010.
Abstract

We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies.

We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we prove that they remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.

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

[HBM+10] Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. Computing Rational Radical Sums in Uniform TC0. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 308-316. Leibniz-Zentrum für Informatik, December 2010.
Abstract

A fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether i=1m Ci . AiXi is zero for given rational numbers Ai, 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 and Jef Wijsen (eds.) Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10). IEEE Comp. Soc. Press, September 2010.
@proceedings{time2010-MW,
title =               {{P}roceedings of the 17th {I}nternational
{S}ymposium on {T}emporal {R}epresentation and
{R}easoning ({TIME}'10)},
editor =              {Markey, Nicolas and Wijsen, Jef},
booktitle =           {{P}roceedings of the 17th {I}nternational
{S}ymposium on {T}emporal {R}epresentation and
{R}easoning ({TIME}'10)},
acronym =             {{TIME}'10},
publisher =           {IEEE Comp. Soc. Press},
year =                {2010},
month =               sep,
doi =                 {10.1109/TIME.2010.4},
url =                 {http://ieeexplore.ieee.org/xpl/ tocresult.jsp?
}

2009
[BDL+09] Thomas Brihaye, Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts and Bounded Memory. In LFCS'09, Lecture Notes in Computer Science 5407, pages 92-106. Springer-Verlag, January 2009.
Abstract

We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension make strategy quantifiers to not "forget" the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies.

We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Game Logic, Strategy Logic, ...). We then address the problem of model-checking for our logics, providing a PSPACE algoritm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case.

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

[BDM+09] Patricia Bouyer, Marie Duflot, Nicolas Markey, and Gabriel Renault. Measuring Permissivity in Finite Games. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 196-210. Springer-Verlag, September 2009.
Abstract

In this paper, we extend the classical notion of strategies in turn-based finite games by allowing several moves to be selected. We define and study a quantitative measure for permissivity of such strategies by assigning penalties when blocking transitions. We prove that for reachability objectives, most permissive strategies exist, can be chosen memoryless, and can be computed in polynomial time, while it is in NP∩coNP for discounted and mean penalties.

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

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

2008
[BLM08] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Model Checking One-clock Priced Timed Automata. Logical Methods in Computer Science 4(2). May 2008.
Abstract

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model checking WMTL (LTL with cost-constrained modalities) is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).

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

[DDM+08] Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robust Safety of Timed Automata. Formal Methods in System Design 33(1-3):45-84. Springer-Verlag, December 2008.
Abstract

Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by Δ>0 and clocks can drift by ε>0. The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks.

We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters Δ and ε such that the timed automaton never enters the bad states under the relaxed semantics.

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

[LMO08] François Laroussinie, Nicolas Markey, and Ghassan Oreiby. On the Expressiveness and Complexity of ATL. Logical Methods in Computer Science 4(2). May 2008.
Abstract

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.

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

[BBB+08] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. In QEST'08, pages 55-64. IEEE Comp. Soc. Press, September 2008.
Abstract

In [Baier et al., Probabilistic and Topological Semantics for Timed Automata, FSTTCS'07] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability 1 in a timed automaton, and solved for the class of single-clock timed automata.

In this paper, we consider the quantitative model-checking problem for ω-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an ω-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.

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

[BFL+08] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jiří Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In FORMATS'08, Lecture Notes in Computer Science 5215, pages 33-47. Springer-Verlag, September 2008.
Abstract

We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.

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

[BGM+08] Thomas Brihaye, Mohamed Ghannem, Nicolas Markey, and Lionel Rieg. Good friends are hard to find!. In TIME'08, pages 32-40. IEEE Comp. Soc. Press, June 2008.
Abstract

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

@inproceedings{time2008-BGMR,
author =              {Brihaye, {\relax Th}omas and Ghannem, Mohamed and
Markey, Nicolas and Rieg, Lionel},
title =               {Good friends are hard to find!},
booktitle =           {{P}roceedings of the 15th {I}nternational
{S}ymposium on {T}emporal {R}epresentation and
{R}easoning ({TIME}'08)},
acronym =             {{TIME}'08},
publisher =           {IEEE Comp. Soc. Press},
pages =               {32-40},
year =                {2008},
month =               jun,
doi =                 {10.1109/TIME.2008.10},
abstract =            {We focus on the problem of finding (the~size of)
a~minimal winning coalition in a multi-player game.
More precisely, we~prove that deciding whether there
is a winning coalition of size at most~$$k$$ is
NP-complete, while deciding whether $$k$$ is the
optimal size is DP-complete. We~also study different
variants of our original problem: the function
problem, where the aim is to effectively compute the
coalition; more succinct encoding of the game; and
richer families of winning objectives.},
}

[BMO+08] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination for Faulty Channel Machines. In STACS'08, Leibniz International Proceedings in Informatics 1, pages 121-132. Leibniz-Zentrum für Informatik, February 2008.
Abstract

A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity.

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

[BMO+08] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. On Expressiveness and Complexity in Real-time Model Checking. In ICALP'08, Lecture Notes in Computer Science 5126, pages 124-135. Springer-Verlag, July 2008.
Abstract

Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called punctual specifications. In this paper we introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of MITL. We conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.

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

[BMR08] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Analysis of Timed Automata via Channel Machines. In FoSSaCS'08, Lecture Notes in Computer Science 4962, pages 157-171. Springer-Verlag, March 2008.
Abstract

Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of MTL, is EXPSPACE-Complete.

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

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

2007
[BLM07] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Model Checking One-clock Priced Timed Automata. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 108-122. Springer-Verlag, March 2007.
Abstract

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions. We prove that model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete under the "single-clock" assumption. In contrast, it has been recently proved that the model-checking problem is undecidable for this model as soon as the system has three clocks. We also prove that the model-checking of WCTL becomes undecidable, even under this "single-clock" assumption.

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

[BLM+07] Thomas Brihaye, François Laroussinie, Nicolas Markey, and Ghassan Oreiby. Timed Concurrent Game Structures. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 445-459. Springer-Verlag, September 2007.
Abstract

We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical timed game automata of Asarin et al., our timed CGSs are "more concurrent", in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the "element of surprise" of timed game automata reported by de Alfaro et al.

We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable via region abstraction, and in particular that strategies are "region-stable" if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger et al.

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

[BM07] Patricia Bouyer and Nicolas Markey. Costs are Expensive!. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 53-68. Springer-Verlag, October 2007.
Abstract

We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.

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

[BMO+07] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. The Cost of Punctuality. In LICS'07, pages 109-118. IEEE Comp. Soc. Press, July 2007.
Abstract

In an influential paper titled "The Benefits of Relaxing Punctuality", Alur, Feder, and Henzinger introduced Metric Interval Temporal Logic (MITL) as a fragment of the real-time logic Metric Temporal Logic (MTL) in which exact or punctual timing constraints are banned. Their main result showed that model checking and satisfiability for MITL are both EXPSPACE-Complete.

Until recently, it was widely believed that admitting even the simplest punctual specifications in any linear-time temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no punctual fragment of MTL was known to have even primitive recursive complexity (with certain decidable fragments having provably non-primitive recursive complexity).

In this paper we identify a co-flat' subset of MTL that is capable of expressing a large class of punctual specifications and for which model checking (although not satisfiability) has no complexity cost over MITL. Our logic is moreover qualitatively different from MITL in that it can express properties that are not timed-regular. Correspondingly, our decision procedures do not involve translating formulas into finite-state automata, but rather into certain kinds of reversal-bounded Turing machines. Using this translation we show that the model checking problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete if timing constraints are encoded in unary.

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

[LMO07] François Laroussinie, Nicolas Markey, and Ghassan Oreiby. On the Expressiveness and Complexity of ATL. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 243-257. Springer-Verlag, March 2007.
Abstract

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.

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

2006
[BBM06] Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5):188-194. Elsevier, June 2006.
Abstract

In this paper, we improve two recent undecidability results of Brihaye, Bruyère and Raskin about weighted timed automata, an extension of timed automata with a cost variable. Our results rely on a new encoding of the two counters of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.

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

[LMS06] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Efficient timed model checking for discrete-time systems. Theoretical Computer Science 353(1-3):249-271. Elsevier, March 2006.
Abstract

We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied.

We exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).

Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes Δ2P-complete or PSPACE-complete depending on the considered semantics.

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

[MR06] Nicolas Markey and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. Theoretical Computer Science 358(2-3):273-292. Elsevier, August 2006.
Abstract

In this paper, we study the complexity of model-checking formulas of four important real-time logics (TPTL, MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

Several results are quite negative: TPTL and MTL remain undecidable along region- and zone-paths. On the other hand, we obtained PTIME algorithms for model checking TCTL along a region path, and for MTL along a single timed path.

@article{tcs358(2-3)-MR,
author =              {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois},
title =               {Model Checking Restricted Sets of Timed Paths},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {358},
number =              {2-3},
pages =               {273-292},
year =                {2006},
month =               aug,
doi =                 {10.1016/j.tcs.2006.01.019},
abstract =            {In this paper, we study the complexity of
model-checking formulas of four important real-time
logics (TPTL, MTL, MITL, and TCTL) over restricted
sets of timed paths. The classes of restricted sets
of timed paths that we consider are
\textit{(i)}~a~single finite (or ultimately
periodic) timed path, \textit{(ii)}~an~infinite set
of finite (or infinite) timed paths defined by a
finite (or ultimately periodic) path in a region
graph, \textit{(iii)}~an~infinite set of finite (or
infinite) timed paths defined by a finite (or
ultimately periodic) path in a zone graph. \par
Several results are quite negative: TPTL and MTL
remain undecidable along region- and zone-paths. On
the other hand, we obtained PTIME algorithms for
model checking TCTL along a region path, and for MTL
along a single timed path.},
}

[MS06] Nicolas Markey and Philippe Schnoebelen. Mu-calculus path checking. Information Processing Letters 97(6):225-230. Elsevier, March 2006.
Abstract

We investigate the path model checking problem for the μ-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the μ-calculus.

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

[BLM+06] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost Optimal Strategies in One-Clock Priced Timed Automata. In FSTTCS'06, Lecture Notes in Computer Science 4337, pages 345-356. Springer-Verlag, December 2006.
Abstract

We consider timed games extended with cost information, and prove computability of the optimal cost and of ε-optimal memoryless strategies in timed games with one clock. In contrast, this problem has recently been proved undecidable for timed games with three clocks.

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

[BMR06] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Model-Checking of Linear-Time Properties in Timed Automata. In LATIN'06, Lecture Notes in Computer Science 3887, pages 238-249. Springer-Verlag, March 2006.
Abstract

Formal verification of timed systems is well understood, but their implementation is still challenging. Recent works by Raskin et al. have brought out a model of parameterized timed automata that can be used to prove implementability of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of Büchi-like and LTL properties. We also verify bounded-response-time properties.

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

[LMO06] François Laroussinie, Nicolas Markey, and Ghassan Oreiby. Model-Checking Timed ATL for Durational Concurrent Game Structures. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 245-259. Springer-Verlag, September 2006.
Abstract

We extend the framework of ATL model-checking to "simply timed" concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.

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

2005
[BCM05] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. In FSTTCS'05, Lecture Notes in Computer Science 3821, pages 432-443. Springer-Verlag, December 2005.
Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the F modality can be translated into MTL.

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

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

2004
[Mar04] Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. Acta Informatica 40(6-7):431-458. Springer-Verlag, May 2004.
Abstract

We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that "past is for free", in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.

@article{acta40(6-7)-Mar,
author =              {Markey, Nicolas},
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
allowing symmetric past-time modalities does not
bring additional theoretical complexity. This result
holds even for small fragments and even when nesting
future formulas into past formulas.},
}

[MS04] Nicolas Markey and Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1):3-6. Elsevier, April 2004.
Abstract

SLP-compressed words are words given by simple deterministic grammars called "straight-line programs". We prove that the problem of deciding whether an SLP-compressed word is recognized by a FSA is complete for polynomial-time.

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

[DCM+04] Jenifer Davoren, Vaughan Coulthard, Nicolas Markey, and Thomas Moor. Non-deterministic Temporal Logics for General Flow Systems. In HSCC'04, Lecture Notes in Computer Science 2993, pages 280-295. Springer-Verlag, March 2004.
Abstract

In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discrete-time transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.

@inproceedings{hscc2004-DCMM,
author =              {Davoren, 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, and Jean-François Raskin. Robustness and Implementability of Timed Automata. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 118-133. Springer-Verlag, September 2004.
Abstract

In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by Δ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter Δ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a Δ. We show that this question is closely related to a notion of robustness for timed automata defined in (A. Puri: Dynamical Properties of Timed Automata. FTRTFT, 1998) and prove that the implementability problem is decidable.

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

[LMS04] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model Checking Timed Automata with One or Two Clocks. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 387-401. Springer-Verlag, August 2004.
Abstract

In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL, over TAs with one clock or two clocks.

First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL, over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.

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

[MR04] Nicolas Markey and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 432-447. Springer-Verlag, August 2004.
Abstract

In this paper, we study the complexity of model-checking formulas of three important real-time logics (MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

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

[MS04] Nicolas Markey and Philippe Schnoebelen. Symbolic Model Checking for Simply Timed Systems. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 102-117. Springer-Verlag, September 2004.
Abstract

We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).

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

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

[MS04] Nicolas Markey and Philippe Schnoebelen. TSMV: Symbolic Model Checking for Simply Timed Systems. In QEST'04, pages 330-331. IEEE Comp. Soc. Press, September 2004.
Abstract

TSMV is an extension of NuSMV, the open-source symbolic model checker, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries an integer duration (possibly zero). This simple model supports efficient symbolic algorithms for RTCTL formulae.

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

2003
[Mar03] Nicolas Markey. Temporal Logic with Past is Exponentially More Succinct. EATCS Bulletin 79:122-128. EATCS, February 2003.
Abstract

We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.

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

[MS03] Nicolas Markey and Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In CONCUR'03, Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, August 2003.
Abstract

We consider the problem of checking whether a finite (or ultimately periodic) run satisfies a temporal logic formula. This problem is at the heart of "runtime verification" but it also appears in many other situations. By considering several extended temporal logics, we show that the problem of model checking a path can usually be solved efficiently, and profit from specialized algorithms. We further show it is possible to efficiently check paths given in compressed form.

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

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

2002
[LMS02] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, April 2002.
Abstract

We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).

A surprising outcome of this study is that it provides the second example of a Δ2P-complete model checking problem.

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

[LMS02] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Comp. Soc. Press, July 2002.
Abstract

We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.

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

[Mar02] Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 89-106. Elsevier, August 2002.
Abstract

We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our results show that "past is for free", that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We also remark that existential and universal model-checking can have different complexity for certain fragments.

@inproceedings{express2002-Mar,
author =              {Markey, Nicolas},
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.
is it does not bring additional theoretical
complexity, even for small fragments, and even when
nesting future formulae into past formulae. We~also
remark that existential and universal model-checking
can have different complexity for certain
fragments.},
}

2001
[LMS01] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model Checking CTL+ and FCTL is hard. In FoSSaCS'01, Lecture Notes in Computer Science 2030, pages 318-331. Springer-Verlag, April 2001.
Abstract

Among the branching-time temporal logics used for the specification and verification of systems, CTL+, FCTL and ECTL+ are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is Δ2p-complete.

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