| |
VOLUME 3, ISSUE 1, PAPER 7
|
Real-Time Model-Checking: Parameters everywhere
|
©Véronique Bruyère, Université de Mons-Hainaut
©Jean-François Raskin, Université Libre de Bruxelles
|
Abstract
In this paper, we study the model-checking and parameter synthesis problems
of the logic TCTL over discrete-timed automata where parameters are allowed
both in the model (timed automaton) and in the property (temporal formula). Our
results are as follows. On the negative side, we show that the model-checking
problem of TCTL extended with parameters is undecidable over discrete-timed
automata with only one parametric clock. The undecidability result needs
equality in the logic. On the positive side, we show that the model-checking
and the parameter synthesis problems become decidable for a fragment of the
logic where equality is not allowed. Our method is based on automata theoretic
principles and an extension of our method to express durations of runs in timed
automata using Presburger arithmetic.
|
Publication date: February 27, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(1:7)2007
Hit Counts: 1782 |
 Creative Commons | |
