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 750:53-68. Elsevier, November 2018.
- 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{tcs750()-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}, volume = {750}, pages = {53-68}, year = {2018}, month = nov, doi = {10.1016/j.tcs.2018.01.021}, 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 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.}, } |

[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 277, pages 250-264. September 2018.
- 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}, volume = {277}, pages = {250-264}, year = {2018}, month = sep, doi = {10.4204/EPTCS.277.18}, 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.}, } |

[BJM18] | Patricia Bouyer,
Samy Jaziri, and
Nicolas Markey.
Efficient timed diagnosis using automata with timed
domains.
In RV'18,
Lecture Notes in Computer Science 11237, pages 205-221. Springer-Verlag, November 2018.
- Abstract
We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed autmata, 2002].
@inproceedings{rv2018-BJM, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {Efficient timed diagnosis using automata with timed domains}, editor = {Colombo, Christian and Leucker, Martin}, booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on {R}untime {V}erification ({RV}'18)}, acronym = {{RV}'18}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {11237}, pages = {205-221}, year = {2018}, month = nov, doi = {10.1007/978-3-030-03769-7_12}, abstract = {We consider the problems of efficiently diagnosing and predicting what did (or~will) happen in a partially-observable one-clock timed automaton. We~introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We~report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed autmata,~2002].}, } |

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

[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, author = {Haddad, Serge}, 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 Hadjicostis, Christoforos N.}, title = {On~the history of diagnosability and opacity in discrete event systems}, publisher = {Elsevier}, journal = {Annual Reviews in Control}, volume = {45}, pages = {257-266}, year = {2018}, doi = {10.1016/j.arcontrol.2018.04.002}, } |