Name
Abstract | ||
|---|---|---|
In this paper(1), 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 and in the property. 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. When equality is not allowed, we show that the model-checking and the parameter synthesis problems become decidable. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.2168/LMCS-3(1:7)2007 | LECTURE NOTES IN COMPUTER SCIENCE |
Keywords | Field | DocType |
Real-time,timed automata,timed temporal logics,parameters,decidability | Logic synthesis,Real time model,Computer science,Automaton,Algorithm,Decidability,Real-time operating system,Parametric statistics,Symbolic trajectory evaluation,Undecidable problem | Journal |
Volume | Issue | ISSN |
2914 | 1 | 0302-9743 |
Citations | PageRank | References |
26 | 0.92 | 6 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Véronique Bruyère | 1 | 429 | 43.59 |
| Jean-François Raskin | 2 | 1735 | 100.15 |