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