Reachability and liveness in parametric timed automata

Autor: Étienne André, Didier Lime, Olivier H. Roux

Publikováno v: Logical Methods in Computer Science, Vol Volume 18, Issue 1 (2022)

We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interesting problems are undecidable. Notably, the parametric reachability emp

Externí odkaz: https://doaj.org/article/43f1e7cde3144f0191cb76c17e779036

Language Preservation Problems in Parametric Timed Automata

Autor: Étienne André, Didier Lime, Nicolas Markey

Publikováno v: Logical Methods in Computer Science, Vol Volume 16, Issue 1 (2020)

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 valu

Externí odkaz: https://doaj.org/article/1433fd30f392498c95e6456a5a3d73c8

Guaranteeing Timed Opacity using Parametric Timed Model Checking

Autor: Étienne André, Dylan Marinho, Jun Sun, Didier Lime

Publikováno v: ACM Transactions on Software Engineering and Methodology
ACM Transactions on Software Engineering and Methodology, 2022, 31 (4), pp.1-36. ⟨10.1145/3502851⟩

Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage occurs whenever an attacker successfully deduces confidential internal information. In this work, we consider that

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d66ca4bfeb114d72fcf4b6eef2775411
http://arxiv.org/abs/2206.05438

Logical time control of concurrent DES

Autor: Olivier Roux, Didier Lime, Jean-Luc Béchennec

Publikováno v: Discrete Event Dynamic Systems
Discrete Event Dynamic Systems, Springer Verlag, 2021, ⟨10.1007/s10626-020-00333-x⟩

The synthesis of controllers for reactive systems can be done by computing winning strategies in two-player games. Timed (game) Automata are an appropriate formalism to model real-time embedded systems but are not easy to use for controller synthesis

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fbfd6d8d64e216c1e64a4f8b9e192e95
https://hal.archives-ouvertes.fr/hal-03103458

A Turn-Based Approach for Qualitative Time Concurrent Games

Autor: Serge Haddad, Olivier Roux, Didier Lime

Publikováno v: Application and Theory of Petri Nets and Concurrency ISBN: 9783030769826
Petri Nets
PETRI NETS 2021-42nd International Conference on Applications and Theory of Petri Nets and Concurrency
PETRI NETS 2021-42nd International Conference on Applications and Theory of Petri Nets and Concurrency, Jun 2021, Paris, France. pp.76-92, ⟨10.1007/978-3-030-76983-3_5⟩

International audience; We address concurrent games with a qualitative notion of time with parity objectives. This setting allows to express how potential controllers interact with their environment and more specifically includes relevant features: t

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::102101727710c73bbafed8cd1154fb81
https://doi.org/10.1007/978-3-030-76983-3_5