Name
Abstract | ||
|---|---|---|
We consider a general notion of timed automata with input-determined guards and show that they admit a robust logical framework along the lines of [6], in terms of a monadic second order logic characterisation and an expressively complete timed temporal logic. We then generalize these automata using the notion of recursive operators introduced by Henzinger, Raskin, and Schobbens [10], and show that they admit a similar logical framework. These results hold in the "pointwise" semantics. We finally use this framework to show that the real-time logic MITL of Alur et al [2] is expressively complete with respect to an MSO corresponding to an appropriate set of input- determined operators. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-30206-3_7 | LECTURE NOTES IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
monadic second-order logic,timed automata,real-time tem- poral logics,real time,temporal logic,logical framework | Conference | 3253 |
ISSN | Citations | PageRank |
0302-9743 | 20 | 1.13 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Deepak D'souza | 1 | 239 | 17.90 |
| Nicolas Tabareau | 2 | 241 | 23.63 |