2019
[GBM19] Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. Theory of Computing Systems. Springer-Verlag, 2019.
Abstract

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

@article{tocsys2019-GBM,
author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
Nicolas},
title =               {Dependences in Strategy Logic},
publisher =           {Springer-Verlag},
journal =             {Theory of Computing Systems},
year =                {2019},
doi =                 {10.1007/s00224-019-09926-y},
abstract =            {Strategy Logic~(\textsf{SL}) is a very expressive
temporal logic for specifying and verifying
properties of multi-agent systems: in~\textsf{SL},
one can quantify over strategies, assign them to
agents, and express \textsf{LTL} properties of the
resulting plays. Such a powerful framework has two
drawbacks: first, model checking \textsf{SL} has
non-elementary complexity; second, the exact
semantics of \textsf{SL} is rather intricate, and
may not correspond to what is expected. In~this
paper, we~focus on \emph{strategy dependences}
in~\textsf{SL}, by tracking how
existentially-quantified strategies in a formula may
(or~may~not) depend on other strategies selected in
the formula, revisiting the approach of~[Mogavero
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.},
}

[BKM+19] Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, and Giuseppe Perelli. Reasoning about Quality and Fuzziness of Strategic Behaviours. In IJCAI'19, pages 1588-1594. IJCAI organization, August 2019.
Abstract

We introduce and study SL[F]–-mdash;a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0,1], reflecting "how much" or "how well" the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for our logic, based on a quantitative extension of Quantified CTL.

@inproceedings{ijcai2019-BKMMMP,
author =              {Bouyer, Patricia and Kupferman, Orna and Markey,
Nicolas and Maubert, Bastien and Murano, Aniello and
Perelli, Giuseppe},
title =               {Reasoning about Quality and Fuzziness of Strategic
Behaviours},
editor =              {Kraus, Sarit},
booktitle =           {{P}roceedings of the 28th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'19)},
acronym =             {{IJCAI}'19},
publisher =           {IJCAI organization},
pages =               {1588-1594},
year =                {2019},
month =               aug,
doi =                 {10.24963/ijcai.2019/220},
abstract =            {We~introduce and study
{$$\textsf{SL}[\mathcal{F}]$$}---a~quantitative
extension of {$$\textsf{SL}$$} (Strategy Logic),
one~of the most natural and expressive logics
describing strategic behaviours. The satisfaction
value of an {$$\textsf{SL}[\mathcal{F}]$$} formula
is a real value in~{$$[0,1]$$}, reflecting {"}how
much{"} or {"}how well{"} the strategic on-going
objectives of the underlying agents are satisfied.
We~demonstrate the applications of
{$$\textsf{SL}[\mathcal{F}]$$} in quantitative
reasoning about multi-agent systems, by showing how
it can express concepts of stability in multi-agent
systems, and how it generalises some fuzzy temporal
logics. We~also provide a model-checking algorithm
for our logic, based on a quantitative extension of
Quantified~\textsf{CTL}.},
}

[HMR19] Loïc Hélouët, Nicolas Markey, and Ritam Raha. Reachability games with relaxed energy constraints. In GandALF'19, Electronic Proceedings in Theoretical Computer Science. September 2019.
Abstract

We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two kinds of relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, in the sense that it allows receiving more energy when the upper bound is already reached, but the extra energy will not be stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations.

We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in coNP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players.

@inproceedings{gandalf2019-HMR,
author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
Raha, Ritam},
title =               {Reachability games with relaxed energy constraints},
editor =              {Leroux, J{\'e}r{\^o}me and Raskin, Jean-Fran{\c
c}ois},
booktitle =           {{P}roceedings of the 10th {I}nternational
{S}ymposium on {G}ames, {A}utomata, {L}ogics and
{F}ormal {V}erification ({GandALF}'19)},
acronym =             {{GandALF}'19},
series =              {Electronic Proceedings in Theoretical Computer
Science},
year =                {2019},
month =               sep,
abstract =            {We study games with reachability objectives under
energy constraints. We first prove that under strict
energy constraints (either only lower-bound
constraint or interval constraint), those games are
\textsf{LOGSPACE}-equivalent to energy games with
the same energy constraints but without reachability
objective (i.e., for infinite runs). We then
consider two kinds of relaxations of the upper-bound
constraints (while keeping the lower-bound
constraint strict): in the first one, called
\emph{weak upper bound}, the upper bound is
\emph{absorbing}, in the sense that it allows
receiving more energy when the upper bound is
already reached, but the extra energy will not be
stored; in~the second~one, we~allow for
\emph{temporary violations} of the upper bound,
imposing limits on the number or on the amount of
violations.\par We prove that when considering weak
upper bound, reachability objectives require memory,
but can still be solved in polynomial-time for
one-player arenas; we prove that they are in
\textsf{coNP} in the two-player setting. Allowing
for bounded violations makes the problem
\textsf{PSPACE}-complete for one-player arenas and
\textsf{EXPTIME}-complete for two players.},
}

[RSM19] Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction Refinement Algorithms for Timed Automata. In CAV'19, Lecture Notes in Computer Science 11561, pages 22-40. Springer-Verlag, July 2019.
Abstract

We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.

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

[GBL+19] Mauricio González, Patricia Bouyer, Samson Lasaulce, and Nicolas Markey. Optimisation en présence de contraintes en probabilités et processus markoviens contrôlés. In GRETSI'19. August 2019.
Abstract

This article focuses on the existence and synthesis of strategies in double-weighted Markov decision processes, which satisfy both a probability constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable deﬁned using another reachability condition. This work generalizes a scheduling problem for energy consumption (typically the problem of charging electric vehicles). We study the set of values of a parameter (a threshold) for which the problem has a solution, and show how a partial characterization of this set can be obtained via two sequences of optimization problems. We also discuss the completeness and feasibility of the resulting approach.

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