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 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. September 2018. To appear.
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},
  year =                {2018},
  month =               sep,
  note =                {To~appear},
  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.},
}
[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 quantified 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 quantified 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},
}