Reachability preservation based parameter synthesis for timed automata

Étienne André, Giuseppe Lipari, Hoang Gia Nguyen, Youcheng Sun

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


The synthesis of timing parameters consists in deriving conditions on the timing constants of a concurrent system such that it meets its specification. Parametric timed automata are a powerful formalism for parameter synthesis, although most problems are undecidable. We first address here the following reachability preservation problem: given a reference parameter valuation and a (bad) control state, do there exist other parameter valuations that reach this control state iff the reference parameter valuation does? We show that this problem is undecidable, and introduce a procedure that outputs a possibly underapproximated answer. We then show that our procedure can efficiently replace the behavioral cartography to partition a bounded parameter subspace into good and bad subparts; furthermore, our procedure can even outperform the classical bad-state driven parameter synthesis semi-algorithm, especially when distributed on a cluster.

Original languageEnglish
Title of host publicationNASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings
EditorsKlaus Havelund, Gerard Holzmann, Rajeev Joshi
PublisherSpringer-Verlag Italia
Number of pages16
ISBN (Print)9783319175232
Publication statusPublished - 2015
Event7th International Symposium on NASA Formal Methods, NFM 2015 - Pasadena, United States
Duration: 27 Apr 201529 Apr 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference7th International Symposium on NASA Formal Methods, NFM 2015
Country/TerritoryUnited States


Dive into the research topics of 'Reachability preservation based parameter synthesis for timed automata'. Together they form a unique fingerprint.

Cite this