Name
Abstract | ||
|---|---|---|
We consider the problem of model-checking a parametric extension of the logic TCTL over timed automata and establish its decidability. Given a timed automaton, we show that the set of durations of runs starting from a region and ending in another region is definable in Presburger arithmetic (when the time domain is discrete) or in a real arithmetic (when the time domain is dense). Using this logical definition, we show that the parametric model-checking problem for the logic TCTL can be solved algorithmically; the proof of this result is simple. More generally, we are able to effectively characterize the values of the parameters that satisfy the parametric TCTL formula with respect to the given timed automaton. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1342991.1342996 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
parametric model,satisfiability,time domain,timed automaton,presburger arithmetic,model checking | Time domain,Discrete mathematics,Combinatorics,Parametric model,Model checking,Automaton,Algorithm,Presburger arithmetic,Decidability,Parametric statistics,Timed automaton,Mathematics | Journal |
Volume | Issue | ISSN |
9 | 2 | 1529-3785 |
Citations | PageRank | References |
8 | 0.50 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Véronique Bruyère | 1 | 429 | 43.59 |
| Emmanuel Dall'olio | 2 | 29 | 1.74 |
| Jean-François Raskin | 3 | 1735 | 100.15 |