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. Springer-Verlag, July 2018. To appear.
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 inﬁnite-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 inﬁnite runs. Our algorithms are based on quantiﬁer 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-,
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 =              {Roscoe, Bill W. and Peleska, Jan},
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},
year =                {2018},
month =               jul,
note =                {To~appear},
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
inﬁnite-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 inﬁnite runs. Our
algorithms are based on quantiﬁer 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.},
}

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

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