2020
[ALM20] Étienne André, Didier Lime, and Nicolas Markey. Language-preservation problems in parametric timed automata. Logical Methods in Computer Science 16(1). January 2020.
Abstract

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.

@article{lmcs16(1)-ALM,
  author =              {Andr{\'e}, {\'E}tienne and Lime, Didier and Markey,
                         Nicolas},
  title =               {Language-preservation problems in parametric timed
                         automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {16},
  number =              {1},
  year =                {2020},
  month =               jan,
  doi =                 {10.23638/LMCS-16(1:5)2020},
  abstract =            {Parametric timed automata (PTA) are a powerful
                         formalism to model and reason about concurrent
                         systems with some unknown timing delays. In~this
                         paper, we~address the (untimed) language- and
                         trace-preservation problems: given a reference
                         parameter valuation, does there exist another
                         parameter valuation with the same untimed language,
                         or with the same set of traces? We~show that these
                         problems are undecidable both for general PTA and
                         for the restricted class of L{\slash}U-PTA, even for
                         integer-valued parameters, or over bounded time.
                         On~the other~hand, we~exhibit decidable subclasses:
                         1-clock PTA, and 1-parameter deterministic L-PTA and
                         U-PTA. We~also consider robust versions of these
                         problems, where we additionally require that the
                         language be preserved for all valuations between the
                         reference valuation and the new valuation.},
}
[GBM20] Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. Theory of Computing Systems 64(3):467–507. Springer-Verlag, April 2020.
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{tocsys64(3)-GBM,
  author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Dependences in Strategy Logic},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {64},
  number =              {3},
  pages =               {467–507},
  year =                {2020},
  month =               apr,
  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.},
}