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 \emph{et~al.}, Reasoning about strategies: On~the 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. We~address this discrepancy by introducing \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, 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.}, } |