2018
[BMR+18] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen. Average-energy games. Acta Informatica 55(2). Springer-Verlag, March 2018.
Abstract

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

@article{acta55(2)-BMRLL,
author =              {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Larsen, Kim Guldstrand and Laursen,
Simon},
title =               {Average-energy games},
publisher =           {Springer-Verlag},
journal =             {Acta Informatica},
volume =              {55},
number =              {2},
year =                {2018},
month =               mar,
doi =                 {10.1007/s00236-016-0274-1},
abstract =            {Two-player quantitative zero-sum games provide a
natural framework to synthesize controllers with
performance guarantees for reactive systems within
an uncontrollable environment. Classical settings
include mean-payoff games, where the objective is to
optimize the long-run average gain per action, and
energy games, where the system has to avoid running
out of energy. We study average-energy games, where
the goal is to optimize the long-run average of the
accumulated energy. We show that this objective
arises naturally in several applications, and that
it yields interesting connections with previous
concepts in the literature. We prove that deciding
the winner in such games is in
$$\textsf{NP}\cap\textsf{coNP}$$ and at least as
hard as solving mean-payoff games, and we establish
that memoryless strategies suffice to win. We also
consider the case where the system has to minimize
the average-energy while maintaining the accumulated
energy within predefined bounds at all times: this
corresponds to operating with a finite-capacity
storage for energy. We give results for one-player
and two-player games, and establish complexity
bounds and memory requirements.},
}

[LFM+18] Adrien Le Coënt, Laurent Fribourg, Nicolas Markey, Florian De Vuyst, and Ludovic Chamoin. Distributed Synthesis of State-Dependent Switching Control. Theoretical Computer Science. Elsevier, 2018. To appear.
Abstract

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

@article{tcs-LFMDC,
author =              {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Markey, Nicolas and De{~}Vuyst, Florian and Chamoin,
Ludovic},
title =               {Distributed Synthesis of State-Dependent Switching
Control},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
year =                {2018},
doi =                 {10.1016/j.tcs.2018.01.021},
note =                {To~appear},
abstract =            {We present a correct-by-design method of
state-dependent control synthesis for sampled
switching systems. Given a target region~$$R$$ of
the state space, our~method builds a capture
set~$$S$$ and a~control that steers any element
of~$$S$$ into~$$R$$. The~method works by iterated
backward reachability from~$$R$$. It~is also used to
synthesize a recurrence control that makes any state
of~$$R$$ return to~$$R$$ infinitely often.
We~explain how the synthesis method can be performed
in a compositional manner, and apply it to the
synthesis of a compositional control for a concrete
floor-heating system with 11~rooms and up to
$$2^{11}=2048$$ switching modes.},
}

[BBF+18] Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Pierre-Alain Reynier. Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty. In FM'18, Lecture Notes in Computer Science 10951, pages 203-221. Springer-Verlag, July 2018.
Abstract

In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.

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

[BBM18] A. R. Balasubramanian, Nathalie Bertrand, and Nicolas Markey. Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In TACAS'18 (Part II), Lecture Notes in Computer Science 10806, pages 38-54. Springer-Verlag, April 2018.
Abstract

Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the synchronization property, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks).

In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents.

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

[BGM+18] Patricia Bouyer, Mauricio González, Nicolas Markey, and Mickael Randour. Multi-weighted Markov Decision Processes with Reachability Objectives. In GandALF'18, Electronic Proceedings in Theoretical Computer Science. September 2018. To appear.
Abstract

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.

@inproceedings{gandalf2018-BGMR,
author =              {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and
Markey, Nicolas and Randour, Mickael},
title =               {Multi-weighted Markov Decision Processes with
Reachability Objectives},
editor =              {Orlandini, Andrea and Zimmermann, Martin},
booktitle =           {{P}roceedings of the 9th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'18)},
acronym =             {{GandALF}'18},
series =              {Electronic Proceedings in Theoretical Computer
Science},
year =                {2018},
month =               sep,
note =                {To~appear},
abstract =            {In~this paper, we~are interested in the synthesis of
schedulers in double-weighted Markov decision
processes, which satisfy both a percentile
constraint over a weighted reachability condition,
and a quantitative constraint on the expected value
of a random variable defined using a weighted
reachability condition. This~problem is inspired by
the modelization of an electric-vehicle charging
problem. We study the cartography of the problem,
when one parameter varies, and show how a partial
cartography can be obtained via two sequences of
opimization problems. We~discuss completeness and
feasability of the method.},
}

[GBM18] Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. In STACS'18, Leibniz International Proceedings in Informatics 96, pages 34:1-34:14. Leibniz-Zentrum für Informatik, February 2018.
Abstract

Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics.

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

[HJM18] Léo Henry, Thierry Jéron, and Nicolas Markey. Control strategies for off-line testing of timed systems. In SPIN'18, Lecture Notes in Computer Science 10869, pages 171-189. Springer-Verlag, June 2018.
Abstract

Partial observability and controllability are two well-known issues in test-case synthesis for interactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. Building on the tioco timed testing framework, we extend a previous game interpretation of the test-synthesis problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that tries to minimize both control losses and distance to the satisfaction of a test purpose, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method.

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

[BFL+18] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine, and James Worrell. Model Checking Real-Time Systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds.), Handbook of Model Checking. Springer-Verlag, May 2018.
Abstract

This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).

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

[CHV+18] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. Handbook of Model Checking. Springer-Verlag, April 2018.
@book{hbmc18-CHVB,
author =              {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut and Bloem, Roderick},
title =               {Handbook of Model Checking},
publisher =           {Springer-Verlag},
year =                {2018},
month =               apr,
doi =                 {10.1007/978-3-319-10575-8},
}

[Had18] Serge Haddad. Memoryless determinacy of finite parity games: Another simple proof. Information Processing Letters 132:19-21. Elsevier, April 2018.
@article{ipl132()-Had,
title =               {Memoryless determinacy of finite parity games:
Another simple proof},
publisher =           {Elsevier},
journal =             {Information Processing Letters},
volume =              {132},
pages =               {19-21},
year =                {2018},
month =               apr,
doi =                 {10.1016/j.ipl.2017.11.012},
}

[HMM18] Loïc Hélouët, Hervé Marchand, and John Mullins. Concurrent secrets with quantiﬁed suspicion. In ACSD'18. IEEE Comp. Soc. Press, June 2018.
@inproceedings{acsd2018-HMM,
author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Marchand, Herv{\'e}
and Mullins, John},
title =               {Concurrent secrets with quantiﬁed suspicion},
editor =              {Chatain, {\relax Th}omas and Grosu, Radu and
Juh{\'a}s, Gabriel},
booktitle =           {{P}roceedings of the 18th {I}nternational
{C}onference on {A}pplication of {C}oncurrency to
{S}ystem {D}esign ({ACSD}'18)},
acronym =             {{ACSD}'18},
publisher =           {IEEE Comp. Soc. Press},
year =                {2018},
month =               jun,
}

[LLH18] Stéphane Lafortune, Feng Lin, and Christoforos N. Hadjicostis. On the history of diagnosability and opacity in discrete event systems. Annual Reviews in Control 45:257-266. Elsevier, 2018.
@article{aric45()-LLH,
author =              {Lafortune, St{\'e}phane and Lin, Feng and