Search Results

Documents authored by André, Étienne

Document
DOI: 10.4230/LIPIcs.CSL.2026.31
Parametric Disjunctive Timed Networks

Authors: Étienne André, Swen Jacobs, and Engel Lefaucheux

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e., unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters - a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants.
Cite as

Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric Disjunctive Timed Networks. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 31:1-31:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.CSL.2026.31,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Lefaucheux, Engel},
  title =	{{Parametric Disjunctive Timed Networks}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{31:1--31:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.31},
  URN =		{urn:nbn:de:0030-drops-254562},
  doi =		{10.4230/LIPIcs.CSL.2026.31},
  annote =	{Keywords: parametrised verification, parametric timed automata, verification of infinite-state systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.8
Parameterized Verification of Timed Networks with Clock Invariants

Authors: Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with k-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al. (2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable.
Cite as

Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur. Parameterized Verification of Timed Networks with Clock Invariants. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.FSTTCS.2025.8,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Karra, Shyam Lal and Sankur, Ocan},
  title =	{{Parameterized Verification of Timed Networks with Clock Invariants}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.8},
  URN =		{urn:nbn:de:0030-drops-250878},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.8},
  annote =	{Keywords: Networks of Timed Automata, Parameterized Verification, Timed Petri Nets}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2024.3
Execution-Time Opacity Problems in One-Clock Parametric Timed Automata

Authors: Étienne André, Johan Arcile, and Engel Lefaucheux

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

Abstract
Parametric timed automata (PTAs) extend the concept of timed automata, by allowing timing delays not only specified by concrete values but also by parameters, allowing the analysis of systems with uncertainty regarding timing behaviors. The full execution-time opacity is defined as the problem in which an attacker must never be able to deduce whether some private location was visited, by only observing the execution time. The problem of full ET-opacity emptiness (i.e., the emptiness over the parameter valuations for which full execution-time opacity is satisfied) is known to be undecidable for general PTAs. We therefore focus here on one-clock PTAs with integer-valued parameters over dense time. We show that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved. Our proofs rely on a novel construction as well as on variants of Presburger arithmetics. We finally prove an additional decidability result on an existential variant of execution-time opacity.
Cite as

Étienne André, Johan Arcile, and Engel Lefaucheux. Execution-Time Opacity Problems in One-Clock Parametric Timed Automata. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.FSTTCS.2024.3,
  author =	{Andr\'{e}, \'{E}tienne and Arcile, Johan and Lefaucheux, Engel},
  title =	{{Execution-Time Opacity Problems in One-Clock Parametric Timed Automata}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{3:1--3:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.3},
  URN =		{urn:nbn:de:0030-drops-221923},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.3},
  annote =	{Keywords: Timed opacity, Parametric timed automata, Presburger arithmetic}
}
Document
Artifact
DOI: 10.4230/DARTS.9.1.4
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)

Authors: Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun

Published in: DARTS, Volume 9, Issue 1, Special Issue of the 35th Euromicro Conference on Real-Time Systems (ECRTS 2023)

Abstract
We propose here solutions to the FMTV 2015 challenge of a distributed video processing system using four different formalisms, as well as the description of the challenge itself. This artifact contains several solutions to various subchallenges, and instructions and scripts to reproduce these results smoothly.
Cite as

Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact). In Special Issue of the 35th Euromicro Conference on Real-Time Systems (ECRTS 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 1, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{altmeyer_et_al:DARTS.9.1.4,
  author =	{Altmeyer, Sebastian and Andr\'{e}, \'{E}tienne and Dal Zilio, Silvano and Fejoz, Lo\"{i}c and Harbour, Michael Gonz\'{a}lez and Graf, Susanne and Guti\'{e}rrez, J. Javier and Henia, Rafik and Le Botlan, Didier and Lipari, Giuseppe and Medina, Julio and Navet, Nicolas and Quinton, Sophie and Rivas, Juan M. and Sun, Youcheng},
  title =	{{From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)}},
  pages =	{4:1--4:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{1},
  editor =	{Altmeyer, Sebastian and Andr\'{e}, \'{E}tienne and Dal Zilio, Silvano and Fejoz, Lo\"{i}c and Harbour, Michael Gonz\'{a}lez and Graf, Susanne and Guti\'{e}rrez, J. Javier and Henia, Rafik and Le Botlan, Didier and Lipari, Giuseppe and Medina, Julio and Navet, Nicolas and Quinton, Sophie and Rivas, Juan M. and Sun, Youcheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.1.4},
  URN =		{urn:nbn:de:0030-drops-180257},
  doi =		{10.4230/DARTS.9.1.4},
  annote =	{Keywords: Verification challenge, industrial use case, end-to-end latency, real-time systems, response time analysis}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.ECRTS.2023.19
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper)

Authors: Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun

Published in: LIPIcs, Volume 262, 35th Euromicro Conference on Real-Time Systems (ECRTS 2023)

Abstract
We present here the main features and lessons learned from the first edition of what has now become the ECRTS industrial challenge, together with the final description of the challenge and a comparative overview of the proposed solutions. This verification challenge, proposed by Thales, was first discussed in 2014 as part of a dedicated workshop (FMTV, a satellite event of the FM 2014 conference), and solutions were discussed for the first time at the WATERS 2015 workshop. The use case for the verification challenge is an aerial video tracking system. A specificity of this system lies in the fact that periods are constant but known with a limited precision only. The first part of the challenge focuses on the video frame processing system. It consists in computing maximum values of the end-to-end latency of the frames sent by the camera to the display, for two different buffer sizes, and then the minimum duration between two consecutive frame losses. The second challenge is about computing end-to-end latencies on the tracking and camera control for two different values of jitter. Solutions based on five different tools - Fiacre/Tina, CPAL (simulation and analysis), IMITATOR, UPPAAL and MAST - were submitted for discussion at WATERS 2015. While none of these solutions provided a full answer to the challenge, a combination of several of them did allow to draw some conclusions.
Cite as

Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper). In 35th Euromicro Conference on Real-Time Systems (ECRTS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 262, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{altmeyer_et_al:LIPIcs.ECRTS.2023.19,
  author =	{Altmeyer, Sebastian and Andr\'{e}, \'{E}tienne and Dal Zilio, Silvano and Fejoz, Lo\"{i}c and Harbour, Michael Gonz\'{a}lez and Graf, Susanne and Guti\'{e}rrez, J. Javier and Henia, Rafik and Le Botlan, Didier and Lipari, Giuseppe and Medina, Julio and Navet, Nicolas and Quinton, Sophie and Rivas, Juan M. and Sun, Youcheng},
  title =	{{From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS}},
  booktitle =	{35th Euromicro Conference on Real-Time Systems (ECRTS 2023)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-280-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{262},
  editor =	{Papadopoulos, Alessandro V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2023.19},
  URN =		{urn:nbn:de:0030-drops-180486},
  doi =		{10.4230/LIPIcs.ECRTS.2023.19},
  annote =	{Keywords: Verification challenge, industrial use case, end-to-end latency}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.SynCoP.2015
OASIcs, Volume 44, SynCoP'15, Complete Volume

Authors: Étienne André and Goran Frehse

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
OASIcs, Volume 44, SynCoP'15, Complete Volume
Cite as

2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{andre_et_al:OASIcs.SynCoP.2015,
  title =	{{OASIcs, Volume 44, SynCoP'15, Complete Volume}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015},
  URN =		{urn:nbn:de:0030-drops-56168},
  doi =		{10.4230/OASIcs.SynCoP.2015},
  annote =	{Keywords: Software/Program Verification}
}
Document
Front Matter
DOI: 10.4230/OASIcs.SynCoP.2015.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Étienne André and Goran Frehse

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:OASIcs.SynCoP.2015.i,
  author =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{i--xii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.i},
  URN =		{urn:nbn:de:0030-drops-56034},
  doi =		{10.4230/OASIcs.SynCoP.2015.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
Informal Presentation
DOI: 10.4230/OASIcs.SynCoP.2015.104
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation)

Authors: Étienne André, Camille Coti, and Hoang Gia Nguyen

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Parametric timed automata (PTA) allow the specification and verification of timed systems incompletely specified, or featuring timing constants that may change either in the design phase, or at runtime. The behavioral cartography of PTA (BC) relies on the idea of covering a bounded parameter domain with tiles, i.e., parts of the parameter domain in which the discrete behavior is uniform. This is achieved by iterating the inverse method (IM) on the (yet uncovered) integer parameter valuations ("points") of the bounded parametric domain: given a reference point, IM generalizes the behavior corresponding to this point by synthesizing a constraint containing other (integer and real-valued) points with the same discrete behavior. Then, given a linear time property, it is easy to partition the parametric domain into a subset of "good" tiles and a subset of "bad" ones (which correspond to good and bad behaviors). Useful applications of BC include the optimization of timing constants, and the measure of the system robustness (values around the reference parameters) w.r.t. the untimed language. In practice, a parameter domain with a large number of integer points will require a long time to compute BC. To alleviate that, our goal is to take advantage of powerful distributed architectures. Distributing BC is theoretically easy, since it is trivial that two executions of IM from two different points can be performed on two different nodes. However, distributing it efficiently is challenging. For example, calling two executions of IM from two contiguous integer points has a large probability to yield the same tile in both cases, resulting in a loss of time for one of the two nodes. Thus, the critical question is how to distribute efficiently the point on which to call IM. In a previous work, a master-worker scheme is proposed, where the master assigns points to each worker process, which is called a point-based distribution scheme. In this point-based distribution scheme, choosing the point distribution approach on the master side is the key point that will decide the algorithm performance. Since the master has no ability to foresee the tiles on cartography (the "shape" of a cartography is unknown in general), two or more processes can receive close points, that then yield the same result, leading to a loss of efficiency. Besides that, two or more tiles can overlap each other; hence, the question is whether we stop an going process starting from a point that is already covered by another tile. Finally, a very large parameter domain (with many integer points) can cause a bottleneck phenomenon on the master side since many worker processes ask for point, while the master is busy to find uncovered points. From the previous problems, we proposed an enhanced master-worker distributed algorithm, based on a domain decomposition scheme. The main idea is that the master splits the parameter domain into subdomains, and assigns them to the workers. Then workers will work on their own set of points, hence reducing the probability of choosing close points since the workers work as far as possible from each other. Then, when a worker finishes the coverage of its subdomain, it asks the master for a new subdomain: the master splits a slow worker's subdomain into two parts, and sends it to the fast worker. Furthermore, we used a heuristic approach to decide whether to stop a process working on a point that has been covered by a tile of another worker. In all our experiments, our enhanced distributed algorithm outperforms previous algorithms.
Cite as

Étienne André, Camille Coti, and Hoang Gia Nguyen. Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 104-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:OASIcs.SynCoP.2015.104,
  author =	{Andr\'{e}, \'{E}tienne and Coti, Camille and Nguyen, Hoang Gia},
  title =	{{Enhanced Distributed Behavioral Cartography of Parametric Timed Automata}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{104--105},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.104},
  URN =		{urn:nbn:de:0030-drops-56134},
  doi =		{10.4230/OASIcs.SynCoP.2015.104},
  annote =	{Keywords: Formal methods, model checking, distributed algorithmic, real-time systems, parameter synthesis}
}
Document
DOI: 10.4230/OASIcs.FSFMA.2013.18
Dynamic Clock Elimination in Parametric Timed Automata

Authors: Étienne André

Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)

Abstract
The formalism of parametric timed automata provides designers with a formal way to specify and verify real-time concurrent systems where iming requirements are unknown (or parameters). Such models are usually subject to the state space explosion. A popular way to partially reduce the size of the state space is to reduce the number of clock variables. In this work, we present a technique for dynamically eliminating clocks. Experiments using IMITATOR show a diminution of the number of states and of the computation time, and in some cases allow termination of the analysis of models that could not terminate otherwise. More surprisingly, even when the number of clocks remains constant, there is little noticeable overhead in applying the proposed clock elimination.
Cite as

Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 18-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{andre:OASIcs.FSFMA.2013.18,
  author =	{Andr\'{e}, \'{E}tienne},
  title =	{{Dynamic Clock Elimination in Parametric Timed Automata}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{18--31},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.18},
  URN =		{urn:nbn:de:0030-drops-40855},
  doi =		{10.4230/OASIcs.FSFMA.2013.18},
  annote =	{Keywords: Verification, Real-time systems, Parameter synthesis, State space reduction, Inverse Method}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact