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 constrained reconfigurable broadcast networks}, 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 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 \emph{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).\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 \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.}, } |

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