1: \documentclass{llncs}

2: \usepackage {amssymb,latexsym,graphicx,epic,eepic,stmaryrd}

3: 

4: % \input{IJFCS.sty}

5: % \newcommand {\qed} {\hfill \ensuremath{\Box} \\}

6: \newcommand {\implies} {\ensuremath{\, \Rightarrow \,}}

7: \newcommand {\ltl}[1] {\ensuremath{\mathrm{LTL}(#1)}}

8: \newcommand {\ltll} {\ensuremath{\mathrm{LTL}}}

9: \newcommand {\tltl}[1] {\ensuremath{\mathrm{TLTL}(#1)}}

10: \newcommand {\tltll} {\ensuremath{\mathrm{TLTL}}}

11: \newcommand {\tltler}[1] {\ensuremath{\mathrm{LTL}_{\mathit{er}}}(#1)}

12: \newcommand {\tltlec}[1] {\ensuremath{\mathrm{LTL}_{\mathit{ec}}}(#1)}

13: \newcommand {\tltlerl} {\ensuremath{\mathrm{LTL}_{\mathit{er}}}}

14: \newcommand {\tltlecl} {\ensuremath{\mathrm{LTL}_{\mathit{ec}}}}

15: \newcommand {\tltlp}[1] {\ensuremath{\mathrm{TLTL}^\otimes(\widetilde{#1})}}

16: \newcommand {\tltlpl} {\ensuremath{\mathrm{TLTL}^\otimes}}

17: \newcommand {\mitle}[1] {\ensuremath{\mathrm{MTL}(#1)}}

18: \newcommand {\mitlel} {\ensuremath{\mathrm{MTL}}}

19: \newcommand {\mitl}[1] {\ensuremath{\mathrm{MITL}(#1)}}

20: \newcommand {\mitll} {\ensuremath{\mathrm{MITL}}}

21: \newcommand {\mitlde}[1] {\ensuremath{\mathrm{MTL}^{\Fm}(#1)}}

22: \newcommand {\mitldel} {\ensuremath{\mathrm{MTL}^{\Fm}}}

23: \newcommand {\mitld}[1] {\ensuremath{\mathrm{MITL}^{\Fm}(#1)}}

24: \newcommand {\mitldl} {\ensuremath{\mathrm{MITL}^{\Fm}}}

25: \renewcommand {\O}{\ensuremath{O}}

26: % \newcommand {\Ominus}{\ensuremath{O^{-}}}

27: \newcommand {\Ominus}{\ensuremath{O\!\!\!{\raisebox{1.25pt}{-}}\,}}

28: \newcommand {\U}{\ensuremath{U}}

29: \renewcommand {\S}{\ensuremath{S}}

30: \newcommand {\true} {\ensuremath{\top}}

31: \newcommand {\false} {\ensuremath{\bot}}

32: \newcommand {\And} {\ensuremath{\wedge}}

33: \newcommand {\Or} {\ensuremath{\vee}}

34: \newcommand {\F} {\ensuremath{\mbox{\boldmath $\Diamond$}}}

35: \newcommand {\Fm} {\ensuremath{\Diamond}}

36: \newcommand {\Fp} {\ensuremath{\mbox{\boldmath

37:       $\Diamond\!\!\!{\raisebox{1.25pt}{-}}$ }}}

38: \newcommand {\Fpm} {\ensuremath{\Diamond\!\!\!{\raisebox{1.25pt}{-}}}}

39: \newcommand {\G}{\ensuremath{\Box}}

40: \newcommand {\notof} {\ensuremath{\neg}}

41: \newcommand {\emptyword}{\ensuremath{\epsilon}}

42: \newcommand {\nat}{\ensuremath{\mathbb{N}}}

43: \newcommand {\rplus}{\ensuremath{\mathbb{R}^{> 0}}}

44: \newcommand {\rnonneg}{\ensuremath{\mathbb{R}^{\geq 0}}}

45: \newcommand {\reals}{\ensuremath{\mathbb{R}}}

46: \newcommand {\rationals}{\ensuremath{\mathbb{Q}}}

47: \newcommand {\qplus}{\ensuremath{\mathbb{Q}^{> 0}}}

48: \newcommand {\qnonneg}{\ensuremath{\mathbb{Q}^{\geq 0}}}

49: \newcommand {\tw}[1] {\ensuremath{\mathit{tw}(#1)}}

50: \newcommand {\twp}[1] {\ensuremath{\mathit{tw}_p(#1)}}

51: \newcommand {\twfn} {\ensuremath{\mathit{tw}}}

52: \newcommand {\twpfn} {\ensuremath{\mathit{tw}_p}}

53: \newcommand {\twnp}[1] {\ensuremath{\mathit{tw}_{\mathit{np}}(#1)}}

54: \newcommand {\lsymb}[1] {\ensuremath{L_{\mathit{sym}}(#1)}}

55: \newcommand {\timefn} {\ensuremath{\mathit{time}}}

56: \newcommand {\timesub}[2] {\ensuremath{\mathit{time}_{#1}(#2)}}

57: \newcommand {\twf}[1] {\ensuremath{\mathit{T} #1^{*}}}

58: \newcommand {\two}[1] {\ensuremath{\mathit{T} #1^{\omega}}}

59: % \newcommand {\twi}[1] {\ensuremath{\mathit{T} #1^{\infty}}}

60: \newcommand {\twi}[1] {\ensuremath{\mathit{T} #1^{\infty}}}

61: \newcommand {\twind}[1] {\ensuremath{\mathit{T}_{\mathit{nd}} #1^{\infty}}}

62: \newcommand {\edge} {\ensuremath{\stackrel{}{\longrightarrow}}}

63: \newcommand {\aedge}[1] {\ensuremath{\stackrel{#1}{\longrightarrow}}}

64: \newcommand {\aedgesub}[2] {\ensuremath{\stackrel{#2}{\longrightarrow_{#1}}}}

65: \newcommand {\edgesub}[1] {\ensuremath{\longrightarrow_{#1}}}

66: \newcommand {\ttrans}[3] {\ensuremath{

67:         \renewcommand{\arraystretch}{0.5}

68:         {\begin{array}{c}

69:         \scriptstyle{#1, \, #3} \\ 

70:         \longrightarrow \\

71:         \scriptstyle{#2}

72:         \end{array}}}}

73: \newcommand {\union} {\ensuremath{\cup}}

74: \newcommand {\intersection} {\ensuremath{\cap}}

75: %\newcommand {\intervals} {\ensuremath{\mathcal{I}{\mathbb{R}}}}

76: \newcommand {\intervals} {\ensuremath{\mathcal{I}_{\mathbb{Q}}}}

77: \newcommand {\proper}[1] {\ensuremath{\mathit{prop}(#1)}}

78: \newcommand {\mso}[1] {\ensuremath{\mathrm{MSO}(#1)}}

79: \newcommand {\msol} {\ensuremath{\mathrm{MSO}}}

80: \newcommand {\msord}{\ensuremath{\mathcal{L}\raisebox{0ex}{\ensuremath{\scriptstyle{\stackrel{\leftrightarrow}{d}}}}}}

81: %\newcommand {\msord} {\ensuremath{\mathcal{L}\vec{d}}}

82: \newcommand {\tmsoer}[1] {\ensuremath{\mathrm{MSO}_{\mathit{er}}(#1)}}

83: \newcommand {\tmsoerl} {\ensuremath{\mathrm{MSO}_{\mathit{er}}}}

84: \newcommand {\tmso}[1] {\mathrm{TMSO}{(#1)}}

85: \newcommand {\tmsol} {\ensuremath{\mathrm{TMSO}}}

86: \newcommand {\rtmso}[1] {\mathrm{rec\textrm{-}TMSO}{(#1)}}

87: \newcommand {\rtmsol} {\ensuremath{\mathrm{rec\textrm{-}TMSO}}}

88: \newcommand {\rtltl}[1] {\ensuremath{\mathrm{rec\textrm{-}TLTL(#1)}}}

89: \newcommand {\rtltll} {\ensuremath{\mathrm{rec\textrm{-}TLTL}}}

90: \newcommand {\distec}[2] {\ensuremath{\Delta(#1, #2)}}

91: \newcommand {\dist}[2] {\ensuremath{\Delta_{#1}(#2)}}

92: \newcommand {\futdist}[2] {\ensuremath{\Delta_{#1}^{+}(#2)}}

93: \newcommand {\ldist}[1] {\ensuremath{\vartriangleleft_{#1}}}

94: \newcommand {\rdist}[1] {\ensuremath{\vartriangleright_{#1}}}

95: \newcommand {\ldistof}[2] {\ensuremath{\vartriangleleft_{#1}\!\!(#2)}}

96: \newcommand {\rdistof}[2] {\ensuremath{\vartriangleright_{#1}\!\!(#2)}}

97: \newcommand {\distpred}[3] {\ensuremath{\dist{#1}{#2} \in #3}}

98: \newcommand {\ttos}[1] {\ensuremath {\textit{t-s\/}(#1)}}

99: \newcommand {\ttosfn} {\ensuremath {\textit{t-s\/}}}

100: \newcommand {\stot}[1] {\ensuremath {\textit{s-t\/}(#1)}}

101: \newcommand {\stotfn} {\ensuremath {\textit{s-t\/}}}

102: \newcommand {\voc}[2] {\ensuremath{\mathit{voc}_{#1}(#2)}}

103: \newcommand {\ivoc}[1] {\ensuremath{\mathit{ivoc}(#1)}}

104: \newcommand {\cv}[2] {\ensuremath{v^{#1}_{#2}}}

105: \newcommand {\cvplus}[2] {\ensuremath{v^{+}_{#1,#2}}}

106: \newcommand {\ttoseca}[1] {\ensuremath {\textit{t-s\/}(#1)}}

107: \newcommand {\stoteca}[1] {\ensuremath {\textit{s-t\/}(#1)}}

108: \newcommand {\qeca} {\ensuremath{\mathrm{QECA}}}

109: \newcommand {\qecl} {\ensuremath{\mathrm{QECL}}}

110: \newcommand {\tfo}[1] {\ensuremath{\mathrm{TFO}}(#1)}

111: \newcommand {\tfol} {\ensuremath{\mathrm{TFO}}}

112: \newcommand {\fo}[1] {\ensuremath{\mathrm{FO}(#1)}}

113: \newcommand {\rtfo}[1] {\ensuremath{\mathrm{rec\textrm{-}TFO}}(#1)}

114: \newcommand {\rtfol} {\ensuremath{\mathrm{rec\textrm{-}TFO}}}

115: \newcommand {\sones} {\ensuremath{\mathrm{S1S}}}

116: \newcommand {\sem}[1] {\ensuremath{\llbracket #1 \rrbracket}}

117: \newcommand {\Op} {\ensuremath{\mathit{Op}}}

118: \newcommand {\Rop} {\ensuremath{\mathit{Rop}}}

119: \newcommand {\pos}[1] {\ensuremath{\mathit{pos}(#1)}}

120: \newcommand {\idta} {IDA}

121: \newcommand {\ridta} {rec-IDA}

122: \newcommand {\fridta} {frec-IDA}

123: \newcommand {\fw}[1] {\ensuremath{\mathit{fw}(#1)}}

124: \newcommand {\fwfn} {\ensuremath{\mathit{fw}}}

125: 

126: 

127: \renewcommand {\time}[3] {\ensuremath{\mathit{time}_{#1}^{#2}(#3)}}

128: 

129: 

130: \newtheorem {thm}{Theorem}[section]

131: % \newtheorem {lemma}[thm]{Lemma}

132: % \newtheorem {prop}[thm]{Proposition}

133: % \newtheorem {corollary}[thm]{Corollary}

134: % \newtheorem {claim}{Claim}

135: % \newtheorem {defn} {Definition}[section]

136: 

137: % \newenvironment {proof} {\noindent {\bf Proof }} {\qed \medskip}

138: \newenvironment {pfsketch} {\noindent {\bf Proof sketch }} {\qed \medskip}

139: \newenvironment {lemma*} {\noindent {\bf Lemma} \em} {\rm}

140: 

141: 

142: \newcommand\hvcite[1]{[\refcite{#1}]}

143: 

144: \begin{document}

145: \title{On timed automata with input-determined guards}

146: \author{Deepak D'Souza\inst{1} and Nicolas Tabareau\inst{2}}

147: \institute{Dept. of Computer Science \& Automation\\

148: Indian Institute of Science, Bangalore, India.\\

149: \email{deepakd@csa.iisc.ernet.in}

150: \and

151: \'Ecole Normale Superieure de Cachan, 

152: Cachan, France.\\

153: \email{Nicolas.Tabareau@dptmaths.ens-cachan.fr}}

154: 

155: \maketitle

156: 

157: %% abstract environment

158: \begin{abstract}

159: We consider a general notion of timed automata with

160: \emph{input-determined} guards and show that they admit a robust

161: logical framework along the lines of \cite{d03}, in terms of a monadic second order logic

162: characterisation and an expressively complete timed temporal

163: logic. 

164: We then generalise these automata using the notion of recursive

165: operators introduced by Henzinger, Raskin, and Schobbens \cite{hrs98}, and

166: show that they admit a similar logical framework.

167: These results hold in the ``pointwise'' semantics.

168: We finally use this framework to show that the

169: real-time logic MITL of Alur et al \cite{afh96} is expressively

170: complete with respect to an MSO corresponding to an appropriate

171: input-determined operator.

172: 

173: Keywords: {timed automata, monadic second-order logic,

174:   real-time temporal logics}

175: \end{abstract}

176: 

177: 

178: \section {Introduction}

179: 

180: The timed automata of Alur and Dill \cite{ad94} are a popular

181: model for describing timed behaviours.

182: While these automata have the plus point of being very expressive 

183: and having a decidable emptiness problem, they are 

184: neither determinisable nor closed under complementation.

185: This is a drawback from a couple of points of view.

186: Firstly, one cannot carry out model checking in the framework

187: where a system is modelled as a timed transition system

188: $\mathcal{T}$ and a specification of timed behaviours as a timed

189: automaton $\mathcal{A}$, and where one asks ``is

190: $L(\mathcal{T}) \subseteq L(\mathcal{A})$?''.

191: This would

192: normally involve \emph{complementing} $\mathcal{A}$ and then checking if

193: its intersection with $\mathcal{T}$ is non-empty.

194: One can get around this problem to some extent by using

195: determinisable specifications, or specifying directly the negation

196: of the required property.

197: A second reason why lack of closure properties may concern us is

198: that it precludes the existence of an unrestricted logical

199: characterisation of the class of languages accepted by timed

200: automata.

201: The existence of a monadic second order logic (MSO) characterisation of

202: a class of languages is a strong endorsement of the ``regularity''

203: of the class.

204: It also helps in identifying expressively complete

205: temporal logics, which are natural to use as specification

206: languages and have relatively efficient model checking algorithms.

207: 

208: The event clock automata of \cite{afh94} was one of the first

209: steps towards identifying a subclass of timed automata with the

210: required closure properties.

211: They were shown to be determinisable in \cite{afh94}, and later to

212: admit a robust logical framework in terms of an

213: MSO characterisation and an expressively complete timed temporal

214: logic \cite{d03}.

215: Similar results were shown in \cite{rs97}, \cite{hrs98} and

216: \cite{dt99}.

217: A common technique used in all these results was the idea

218: of ``implicit'' clocks, whose values are determined solely by

219: the timed word being read.

220: For example the event recording clock $x_a$ records the time since

221: the last $a$ action w.r.t.\@ the current position in a timed word,

222: and is thus implicitly reset with each $a$ action.

223: The truth of a guard over these clocks at a point in a timed

224: word is thus completely determined by the word itself, unlike in a

225: timed automaton where the value of a clock depends on 

226: the path taken in the automaton.

227: 

228: In this paper we generalise the notion of an implicit clock to that

229: of an \emph{input determined operator}.

230: An input determined operator $\Delta$ identifies

231: for a given timed word and position in it,

232: a set of intervals in which it is ``satisfied''.

233: The guard $I \in \Delta$ is then satisfied at a point in a timed

234: word if the set of intervals identified by $\Delta$ contains $I$.

235: For example, the event recording clock $x_a$ can be modelled as an

236: input determined operator $\ldist{a}$ which identifies at a given

237: point in a timed word, the (infinite) set of intervals containing

238: the distance to the last $a$ action.

239: The guard $(x_a \in I)$ now translates to $(I \in \ldist{a})$.

240: As an example to show that this framework is more general than

241: implicit clocks, consider the input determined operator $\F_a$

242: inspired by the Metric Temporal logic (MTL) of \cite{k90,ah93}.

243: This operator identifies the set of all intervals $I$ for

244: which there is a future occurrence of an $a$ at a distance which

245: lies in $I$.

246: The guard $I \in \F_a$ is now true iff there is a future occurrence

247: of an $a$ action, at a distance which lies in $I$.

248: 

249: Timed automata which use guards based on a set of input 

250: determined operators are

251: what we call \emph{input determined automata}.

252: We show that input determined automata form a robust class of

253: timed languages, in that they are (a) determinisable, (b)

254: effectively closed

255: under boolean operations, (c) admit a logical characterisation via

256: an unrestricted MSO, and (d) identify a

257: natural expressively complete timed temporal logic.

258: 

259: We then go over to a more expressive framework using the

260: idea of \emph{recursive} event clocks from \cite{hrs98}.

261: In the recursive version of our input determined operator, the

262: operators now expect a third parameter (apart from the timed word

263: and a position in it) which identifies a set of positions in the

264: timed word.

265: This argument could be (recursively) another input determined

266: automaton, or as is better illustrated, a temporal logic

267: formula $\theta$.

268: The formula $\theta$ naturally identifies a set of positions in a

269: timed word where the formula is satisfied.

270: Thus a recursive operator $\Delta$ along with the formula

271: $\theta$, written $\Delta_{\theta}$, behaves like an input

272: determined operator above, and the guard $I \in \Delta_{\theta}$

273: is true iff the set of intervals identified by $\Delta_{\theta}$

274: contains $I$.

275: These recursive input determined automata are also shown to admit

276: similar robust logical properties above.

277: 

278: We should be careful to point out here that, firstly, these results

279: hold in the \emph{pointwise} semantics, where formulas are

280: evaluated only at the ``action points'' in a timed word

281: (used e.g.\@ in \cite{w94}), and not at arbitrary points in between actions

282: in a timed word as allowed in the \emph{continuous} semantics

283: of \cite{afh96,hrs98}.

284: Secondly, we make no claims about the existence of

285: \emph{decision procedures} for these automata and logics.

286: In fact it can be seen the operator $\F_a$ above takes us out of

287: the class of timed automata as we can define the language of timed

288: sequences of $a$'s in which no two $a$'s are a distance 1 apart,

289: with a single state input determined automaton which has the guard

290: $\notof([1,1] \in \F_a)$.

291: Similar versions can be seen to have undecidable emptiness problems

292: and correspondingly undecidable logics \cite{ah93}.

293: Thus the contribution of this paper should be seen more in terms

294: of a general framework for displaying logical characterisations of

295: timed automata, and proving expressive completeness of temporal logics

296: related to these automata.

297: Many of the results along these lines from \cite{dt99,d03}

298: and some in the pointwise semantics from \cite{r99}

299: follow from the results in this paper.

300: 

301: As a new application of this framework, we provide an expressive

302: completeness result for MITL in the pointwise semantics, by

303: showing that it is expressively equivalent to the first order

304: fragment of an MSO based on recursive operators.

305: This answers an open question from \cite{r99}, apart from

306: identifying an interesting class of timed automata.

307: 

308: The techniques used in this paper essentially build on those from

309: \cite{dt99} and \cite{d03} which use the notion of \emph{proper}

310: symbolic alphabets and factor through the results of B\"uchi

311: \cite{b60} and Kamp \cite{k68}.

312: The idea of using recursive operators comes from \cite{hrs98}, who

313: show a variety of expressiveness results, including an expressive

314: completeness for MITL in the continuous semantics.

315: Their result for MITL is more interesting in that

316: it uses event-clock modalities, while we use essentially the same

317: modalities as MITL.

318: However, our MSO is more natural as unlike the MSO in \cite{hrs98}

319: it has unrestricted second order quantification.

320: 

321: 

322: \section{Input determined automata}

323: \label{section:idta}

324: 

325: We use $\nat$ to denote the set of natural numbers 

326: $\{0, 1, \ldots \}$, and $\rnonneg$ and $\qnonneg$ to

327: denote the set of non-negative reals and rationals

328: respectively.

329: The set of finite and infinite words over an

330: alphabet $A$ will be denoted by $A^{\ast}$ and $A^{\omega}$

331: respectively.

332: We use the notation $X \rightarrow Y$ to denote the set of

333: functions from $X$ to $Y$.

334: 

335: An \emph{(infinite) timed word} over an alphabet $\Sigma$ is an

336: element $\sigma$ of $(\Sigma \times \rnonneg)^\omega$ satisfying the

337: following conditions.

338: Let $\sigma = (a_0, t_0) (a_1, t_1) \cdots$.

339: Then:

340: \begin{enumerate}

341: \item

342: (\emph{monotonicity})

343: for each $i \in \nat$, $t_i \leq t_{i+1}$,

344: \item

345: (\emph{progressiveness})

346: for each $t \in \rnonneg$ there

347: exists $i \in \nat$ such that $t_i > t$.

348: \end{enumerate}

349: Let $\two{\Sigma}$ denote the set of 

350: infinite timed words over $\Sigma$.

351: Where convenient, we will use the representation

352: of $\sigma$ as $(\alpha, \tau)$ where 

353: $\alpha \in \Sigma^{\omega}$ and 

354: $\tau : \nat \rightarrow \rnonneg$ is a time sequence satisfying the

355: conditions above.

356: 

357: We will use rational bounded intervals

358: to specify timing constraints.

359: These intervals can be open or closed, and we allow

360: $\infty$ as an open right end.

361: These intervals denote a subset of reals in the usual manner --

362: for example $[2, \infty)$ denotes the set

363: $\{ t \in \rnonneg \ | \ 2 \leq t \}$.

364: The set of all such intervals is denoted $\intervals$.

365: 

366: Our input determined automata will use guards of the form ``$I \in

367: \Delta$'', where $I$ is an interval and $\Delta$ is an operator

368: which determines for a given timed word $\sigma$ and a position

369: $i$ in it, a set of intervals ``satisfying'' it at that point.

370: We then say that $\sigma$ at position $i$ satisfies the guard ``$I

371: \in \Delta$'' if $I$ belongs to the set of intervals

372: identified by $\Delta$.

373: By a ``position''

374: in the timed word we mean one of the ``action

375: points'' or instants given by the time-stamp sequence, and use

376: natural numbers $i$ (instead of the time $\tau(i)$) to denote these

377: positions.

378: %

379: More formally, an input determined operator $\Delta$ (w.r.t. the

380: alphabet $\Sigma$) has a

381: semantic function

382: $\sem{\Delta}: (\two{\Sigma} \times \nat) \rightarrow

383: 2^{\intervals}$.

384: The guard $I \in \Delta$ is satisfied at position $i$ in $\sigma

385: \in \two{\Sigma}$

386: iff $I \in \sem{\Delta}(\sigma, i)$.

387: 

388: The transitions of our input determined automata are

389: labelled by symbolic actions of the form $(a,g)$ where $a$ is an action, 

390: and $g$ is a guard which is a boolean combination of 

391: atomic guards of the form $I \in \Delta$.

392: The set of guards over a finite set of input determined operators

393: $\Op$ is denoted by $\mathcal{G}(\Op)$ and given by the syntax

394: $g ::= \true \ | \ I \in \Delta \ | \ \notof g \ | \ g \Or g \ | \ g \And g$.

395: The satisfaction of a guard $g$ in a timed word $\sigma$ at position

396: $i$, written $\sigma,i \models g$, is given in the expected way: we have 

397: $\sigma, i \models \true$ always, $\sigma, i \models I \in \Delta$

398: as above, and the boolean operators $\notof$, $\Or$, and $\And$ 

399: interpreted as usual.

400: % \[

401: % \begin{array}{lll}

402: % \sigma, i \models \true \\

403: % \sigma, i \models I \in \Delta & \mathrm{ \ iff \ } & I \in

404: % \sem{\Delta}(\sigma, i), % \\

405: % \sigma, i \models \notof g     & \mathrm{ \ iff \ } & \sigma, i

406: % \not\models g \\

407: % \sigma, i \models g \Or g'     & \mathrm{ \ iff \ } & \sigma, i

408: % \models g \mathrm{\ or \ } \sigma, i \models g' \\

409: % \sigma, i \models g \And g'     & \mathrm{ \ iff \ } & \sigma, i

410: % \models g \mathrm{\ and \ } \sigma, i \models g'.

411: % \end{array}

412: % \]

413: 

414: A \emph{symbolic alphabet} $\Gamma$ based on $(\Sigma, \Op)$ is a finite

415: subset of $\Sigma \times \mathcal{G}(\Op)$.

416: An infinite word $\gamma$ in $\Gamma^\omega$ specifies in a natural way a

417: subset of timed words $\tw{\gamma}$ defined as follows.

418: Let $\gamma(i) = (a_i, g_i)$ for each $i \in \nat$.

419: Let $\sigma \in \two{\Sigma}$ with $\sigma(i) = (b_i, t_i)$

420: for each $i \in \nat$.

421: Then $\sigma \in \tw{\gamma}$ iff for each $i \in

422: \nat$, $b_i = a_i$ and $\sigma, i \models g_i$.

423: We extend the map $\twfn$ to work on subsets of

424: $\Gamma^{\omega}$ in the natural way.

425: Thus, for $\widehat{L} \subseteq \Gamma^{\omega}$, we define

426: $\tw{\widehat{L}} = \bigcup_{\gamma \in

427: \widehat{L}} \tw{\gamma}$.

428: Finally, we denote the vocabulary of intervals mentioned in

429: $\Gamma$ by $\ivoc{\Gamma}$.

430: 

431: Recall that a B\"{u}chi automaton over an alphabet

432: $A$ is a structure

433: $\mathcal{A} = (Q, s, \edge, F)$

434: where $Q$ is a finite set of states,

435: $s \in Q$ is an initial state,

436: $\longrightarrow \subseteq

437: Q \times A \times Q$ is the transition relation, and

438: $F \subseteq Q$ is a set of accepting states.

439: Let $\alpha \in A^{\omega}$. 

440: A run of $\mathcal{A}$ over $\alpha$ is a map $\rho :

441: \nat \rightarrow Q$ which satisfies:

442: $\rho(0) = s$ and 

443: $\rho(i) \aedge{\alpha(i)} \rho(i+1)$ for every $i \in \nat$.

444: We say $\rho$ is an \emph{accepting} run of $\mathcal{A}$ on $\alpha$ if 

445: $\rho(i) \in F$ for infinitely many $i \in \nat$.

446: The set of words accepted by $\mathcal{A}$, denoted 

447: here as $\lsymb{\mathcal{A}}$ (for the ``symbolic'' language

448: accepted by $\mathcal{A}$), is defined to be

449: the set of words in $A^{\omega}$

450: on which $\mathcal{A}$ has an accepting run.

451: % We term a subset $L$ of 

452: % $A^{\omega}$ \emph{$\omega$-regular} if $L = \lsymb{\mathcal{A}}$

453: % for some B\"uchi automaton $\mathcal{A}$ over $A$.

454: 

455: We are now in a position to define an input determined

456: automaton.

457: An \emph{input determined automaton} (\idta\ for short)

458: over an alphabet

459: $\Sigma$ and a set of operators $\Op$, is simply

460: a B\"uchi automaton over a symbolic alphabet based on 

461: $(\Sigma,\Op)$.

462: Viewed as a

463: B\"uchi automaton over a symbolic alphabet $\Gamma$, 

464: an input determined automaton $\mathcal{A}$ accepts

465: the language $\lsymb{\mathcal{A}} \subseteq

466: \Gamma^{\omega}$ which we call the symbolic

467: language accepted by $\mathcal{A}$.

468: However, we will be more interested in the timed language

469: accepted by $\mathcal{A}$: this is denoted $L(\mathcal{A})$

470: and is defined to be $\tw{\lsymb{\mathcal{A}}}$.

471: %% We say that $L \subseteq \two{\Sigma}$ is a

472: %% \emph{$\omega$-regular event clock language} over $\Sigma$ if $L =

473: %% L(\mathcal{A})$ for some event clock automaton

474: %% $\mathcal{A}$ over $\Sigma$.

475: 

476: To give a concrete illustration of input determined automata,

477: we show how the event clock automata of \cite{afh94} can be

478: realized in the above framework.

479: Take $\Op$ to be the set of operators $\{\ldist{a}, \rdist{a} \ |

480: \ a \in \Sigma\}$, where the operators $\ldist{a}$ and $\rdist{a}$

481: essentially record the time since the last $a$ action, and the

482: time to the next $a$ action.

483: The operator $\ldist{a}$ (and similarly $\rdist{a}$) can be defined here

484: by setting $\sem{\ldist{a}}(\sigma, i)$ to be

485: \[

486: \{ I \in

487: \intervals \ | \ \exists j < i: \, \sigma(j) = a, \,

488: \tau(i) - \tau(j) \in I, 

489: \mathrm{\, and \, }

490: \forall k: \, j < k < i, \,\sigma(k) \neq a\}.

491: \]

492: 

493: As another example which we will use later in the paper,

494: consider the operator $\F_a$ related to MTL \cite{k90,ah93}.

495: The guard $\F_a \in I$ is meant to be true in a word $\sigma$ at

496: time $i$ iff there is a future

497: instant $j$ labelled $a$ and the distance to it lies in $I$ --

498: i.e. $\tau(j) - \tau(i) \in I$.

499: The guard $\Fp_a \in I$ makes a similar assertion about the

500: \emph{past} of $\sigma$ w.r.t. the current position.

501: An input determined automaton based on these operators can be

502: defined by taking

503: $\Op = \{\F_a, \Fp_a \ | \ a \in \Sigma\}$, and where, for example,

504: $\sem{\F_a}(\sigma, i) = \{ I \ | \ \exists j \geq i: \ \sigma(j)

505: = a, \mathrm{\ and \ } \tau(j) - \tau(i) \in I \}$.

506: 

507: We now want to show that the class of timed languages accepted by

508: input determined automata

509: (for a given choice of $\Sigma$ and $\Op$) is closed under

510: boolean operations.

511: The notion of a \emph{proper} symbolic alphabet will play an

512: important role here and subsequently.

513: A \emph{proper symbolic alphabet} based on $(\Sigma, \Op)$ is of

514: the form $\Gamma = \Sigma \times (\Op \rightarrow

515: 2^{\mathcal{I}})$ where $\mathcal{I}$ is a finite subset of

516: $\intervals$.

517: % The interval vocabulary of $\Gamma$, $\ivoc{\Gamma}$, is defined

518: % to be $\mathcal{I}$.

519: An element of $\Gamma$ is thus of the form $(a,h)$, where

520: the set of intervals specified by $h(\Delta)$ is interpreted

521: as the \emph{exact} subset of intervals in 

522: $\ivoc{\Gamma}$ 

523: which are satisfied by $\Delta$.

524: This is formalised in the following definition of $\twfn_{\Gamma}$ for a

525: proper symbolic alphabet $\Gamma$.

526: Let $\gamma \in \Gamma^{\omega}$ with $\gamma(i) = (a_i, h_i)$.

527: Let $\sigma \in \two{\Sigma}$ with $\sigma(i) = (b_i, t_i)$.

528: Then $\sigma \in \twfn_{\Gamma}(\gamma)$ iff for each $i \in

529: \nat$: $b_i = a_i$ and for each $\Delta \in \Op$, 

530: $h_i(\Delta) = \sem{\Delta}(\sigma, i) \intersection

531: \ivoc{\Gamma}$.

532: 

533: Let $\Gamma$ be a proper symbolic alphabet based on $(\Sigma, \Op)$.

534: Then a B\"uchi automaton $\mathcal{A}$ 

535: over $\Gamma$, which we call a \emph{proper} \idta\ over $(\Sigma,

536: \Op)$, determines a timed language

537: over $\Sigma$ given by $\twfn_{\Gamma}(\lsymb{\mathcal{A}})$.

538: 

539: The class of timed languages defined by \idta's and proper \idta's

540: over $(\Sigma, \Op)$ coincide.

541: An \idta\ over a symbolic alphabet

542: $\Gamma$ can be converted to an equivalent one (in terms of the

543: timed language they define) over a proper symbolic alphabet

544: $\Gamma' = \Sigma \times (\Op \rightarrow 2^{\ivoc{\Gamma}})$.

545: Firstly, each transition label $(a,g)$ in $\Gamma$ can be written

546: in a disjunctive normal form $(c_1 \And \cdots \And c_k)$, with each

547: $c_i$ being a conjunction of literals $I \in \Delta$ or $\notof (I

548: \in \Delta)$.

549: Thus each transition labelled $(a,g)$ can be replaced by a set of

550: transitions labelled $(a,c_i)$, one for each $i$.

551: Now each transition labelled $(a,c)$, with $c$ a conjunct

552: guard,

553: can be replaced by a set of transitions $(a,h)$, one for each $h$

554: ``consistent'' with $c$: i.e.\@ $h$ should satisfy the condition

555: that if $I \in \Delta$ is one of the conjuncts in

556: $c$ then $I \in h(\Delta)$, and if $\notof(I \in \Delta)$ 

557: is one of the conjuncts in $c$ then $I \not\in h(\Delta)$.

558: %

559: In the other direction, to go from a proper \idta\ to an \idta, 

560: a label $(a,h)$ of a proper symbolic

561: alphabet can be replaced by the guard 

562: \[

563: \bigwedge_{\Delta \in \Op} (\bigwedge_{I \in h(\Delta)} (I \in \Delta)

564: \ \And \ \bigwedge_{I \in \ivoc{\Gamma} - h(\Delta)} \notof(I \in \Delta)).

565: \]

566: 

567: The following property of proper symbolic alphabets will play a crucial

568: role.

569: 

570: 

571: \begin{lemma}

572: \label{lemma:proper1}

573: Let $\Gamma$ be a proper symbolic alphabet based on $\Sigma$.

574: Then for any $\sigma \in \two{\Sigma}$ there is a \emph{unique}

575: symbolic word $\gamma$ in $\Gamma^{\omega}$ such that $\sigma \in

576: \twfn_{\Gamma}(\gamma)$.

577: \end{lemma}

578: 

579: \begin{proof}

580: Let $\sigma(i) = (a_i, t_i)$.

581: Then the only possible symbolic word $\gamma$ we can use

582: must be given by $\gamma(i) = (a_i, h_i)$, where

583: $h_i(\Delta) = \sem{\Delta}(\sigma, i) \intersection

584:   \ivoc{\Gamma}$.

585: \qed

586: \end{proof}

587: 

588: % Example of idta and corresponding proper idta....?

589: 

590: In the light of lemma~\ref{lemma:proper1}, going from a symbolic

591: alphabet to a proper one can be viewed as a step towards

592: determinising the automaton with respect to its timed language.

593: From here one can simply use classical automata

594: theoretic techniques to determinise the automaton w.r.t. its

595: \emph{symbolic} language.

596: (Of course, since we deal with infinite words we will need to go

597: from a B\"uchi to 

598: a Muller or Rabin acceptance condition \cite{t90}).

599: 

600: 

601: \begin{theorem}

602: \label{thm:closure1}

603: The class of \idta's over $(\Sigma, \Op)$

604: are effectively closed under the

605: boolean operations of union, intersection, and complement.

606: \end{theorem}

607: 

608: \begin{proof}

609: It is sufficient to address union and complementation.

610: Given automata $\mathcal{A}$ and $\mathcal{B}$ over symbolic

611: alphabets $\Gamma$ and $\Lambda$ respectively, we can simply

612: construct an automaton over $\Gamma \union \Lambda$ 

613: which accepts the union of the two symbolic languages.

614: %

615: For complementing the timed language of $\mathcal{A}$, we can

616: go over to an equivalent proper \idta\ $\mathcal{A}'$ over a

617:  proper symbolic alphabet $\Gamma'$, and now simply

618: complement the symbolic language accepted by $\mathcal{A}'$ to get

619: an automaton $\mathcal{C}$.

620: It is easy to verify, using the uniqueness property of proper

621: alphabets given in Lemma~\ref{lemma:proper1}, 

622: that $L(\mathcal{C}) = \two{\Sigma} - L(\mathcal{A}')$.

623: %

624: In the constructions above we have made use of the 

625: closure properties of $\omega$-regular

626: languages \cite{t90}.

627: \qed

628: \end{proof}

629: 

630: 

631: \section{A logical characterisation of \idta's}

632: \label{section:tmso}

633: 

634: We now show that input determined automata admit a natural

635: characterisation via a timed MSO in the

636: spirit of \cite{b60}.

637: Recall that for an alphabet $A$, B\"uchi's monadic second

638: order logic (denoted here by $\mso{A}$) is given as follows:

639: \[

640: \varphi ::= Q_a(x) \ |\ x \in X \ | \ x < y \ | \ 

641:  \notof{\varphi} \ | \ (\varphi \Or \varphi)

642: \ | \ \exists x \varphi \ | \ \exists X \varphi. 

643: \]

644: The logic is interpreted over a word $\alpha \in A^{\omega}$,

645: along with an interpretation $\mathbb{I}$ which assigns individual

646: variables $x$ a position in $\alpha$ (i.e. an $i \in \nat$), and

647: to set variables $X$ a set of positions $S \subseteq \nat$.

648: The relation $<$ is interpreted as the usual ordering of natural

649: numbers, and the predicate $Q_a$ (one for each $a \in A$) as the

650: set of positions in $\alpha$ labelled $a$.

651: 

652: The formal semantics of the logic is given below.

653: For an interpretation $\mathbb{I}$ we use the notation

654: $\mathbb{I}[i/x]$ to denote the interpretation which sends $x$ to $i$

655: and agrees with $\mathbb{I}$ on all other variables.

656: Similarly, $\mathbb{I}[S/X]$ denotes the modification of $\mathbb{I}$

657: which maps the set variable $X$ to a subset $S$ of $\nat$.

658: Later we will also use the notation $[i/x]$ to denote the

659: interpretation with sends $x$ to $i$ when the rest of the

660: interpretation is irrelevant.

661: 

662: \[

663: \begin{array}{lll}

664: \alpha, \mathbb{I} \models Q_a(x) & \mathrm{\ iff \ } &

665: \alpha(\mathbb{I}(x)) = a.\\

666: \alpha, \mathbb{I} \models x \in X & \mathrm{\ iff \ } &

667: \mathbb{I}(x) \in \mathbb{I}(X). \\

668: \alpha, \mathbb{I} \models x < y & \mathrm{\ iff \ } &

669: \mathbb{I}(x) < \mathbb{I}(y). \\

670: % \alpha, \mathbb{I} \models \notof{\varphi} & \mathrm{\ iff \ } &

671: % \alpha, \mathbb{I} \not\models \varphi. \\

672: % \alpha, \mathbb{I} \models \varphi \Or \psi & \mathrm{\ iff \ } &

673: % \alpha, \mathbb{I} \models \varphi \Or \alpha, \mathbb{I} \models \psi. \\

674: \alpha, \mathbb{I} \models \exists x \varphi & \mathrm{\ iff \ } &

675: \mathrm{ there \ exists \ } i \in \nat \mathrm{ \

676: such \ that \ } \sigma,\mathbb{I}[i/x] \models \varphi.\\

677: \alpha, \mathbb{I} \models \exists X \varphi & \mathrm{\ iff \ } &

678: \mathrm{ there \ exists \ } S \subseteq \nat \mathrm{ \

679: such \ that \ } \sigma,\mathbb{I}[S/X] \models \varphi.

680: \end{array}

681: \]

682: 

683: For a sentence $\varphi$ (i.e. a formula without free variables) 

684: in $\mso{A}$ we set

685: \(

686: L(\varphi) = \{ \sigma \in A^{\omega} \ | \ \sigma \models

687: \varphi \}.

688: \)

689: B\"uchi's result then

690: states that a language $L \subseteq A^{\omega}$ 

691: is accepted by a B\"uchi automaton over $A$ 

692: iff $L = L(\varphi)$ for a sentence

693: $\varphi$ in $\mso{A}$.

694: 

695: We define a timed MSO called $\tmso{\Sigma,\Op}$, parameterised by

696: the alphabet $\Sigma$ and set of input determined operators $\Op$,

697: whose syntax is given by:

698: \[

699: \varphi ::= Q_a(x) \ | \ I \in \Delta(x) \ | \ 

700: x \in X \ | \ x < y \ | \ 

701: \notof{\varphi} \ | \ (\varphi \Or \varphi)

702: \ | \ \exists x \varphi \ | \ \exists X \varphi. 

703: \]

704: In the predicate ``$I \in \Delta(x)$'', $I$ is an interval in

705: $\intervals$, $\Delta \in \Op$, and $x$ is a variable.

706: 

707: The logic is interpreted in a similar manner to $\msol$, except

708: that models are now timed words over $\Sigma$.

709: In particular, for a timed word $\sigma = (\alpha, \tau)$, we have:

710: \[

711: \begin{array}{lll}

712: \sigma, \mathbb{I} \models Q_a(x) & \mathrm{iff} &

713:            \alpha(\mathbb{I}(x)) = a \\

714: \sigma, \mathbb{I} \models I \in \Delta(x) & \mathrm{iff} &

715: I \in \sem{\Delta}(\sigma, \mathbb{I}(x)).

716: \end{array}

717: \]

718: 

719: Given a sentence $\varphi$ in $\tmso{\Sigma}$ we define

720: $L(\varphi) = \{ \sigma \in \two{\Sigma} \ | \ \sigma

721: \models \varphi \}$.

722: 

723: \begin{theorem}

724: \label{thm:msoba1}

725: A timed language $L \subseteq \two{\Sigma}$ is accepted by an input

726: determined automaton over $(\Sigma, \Op)$ iff $L = L(\varphi)$ for

727: some sentence $\varphi$ in $\tmso{\Sigma, Op}$.

728: \end{theorem}

729: 

730: \begin{proof}

731: Given an \idta\ $\mathcal{A}$ 

732: over $(\Sigma, \Op)$ we can give

733: a $\tmsol$ sentence $\varphi$ which describes the existence of an accepting

734: run of $\mathcal{A}$ on a timed word.

735: Following \cite{t90}, for $\mathcal{A} = (Q, q_0, \edge, F)$ with

736: $Q = \{q_0, \ldots q_n\}$, we can take $\varphi$ to be the sentence

737: \begin{eqnarray*}

738: \lefteqn{\!\!\!\!\exists X_0 \cdots \exists X_n \ (\ 0 \in X_0 

739:              \ \And \ \displaystyle{\bigwedge_{i\neq j}} 

740:              \forall x (x \in X_i \implies \notof (x \in X_j)) } \\

741: (*)\ \ \ \ \      & & \And \ \forall x \displaystyle{\bigvee_{q_i \aedge{(a,g)} q_j}}

742: 	         (x \in X_i \ \And \ (x+1) \in X_j \ \And

743: %  \\

744: %          & & \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 

745:               Q_a(x) \And g') \\

746: % \ \And \displaystyle{\bigwedge_{\Delta \in \Op}}

747: %                  (\displaystyle{\bigwedge_{I \in g(\Delta)}}

748: %                    (I \in \Delta) \ \And 

749: %           \bigwedge_{I \not\in g(\Delta)} \notof(I \in \Delta))) \\

750:          & & \And \ \displaystyle{\bigvee_{q_i \in F}} \forall x \exists y 

751:               (x < y \And y \in X_i)).

752: \end{eqnarray*}

753: Here $g'$ denotes the formula obtained by replacing each $I \in

754: \Delta$ in $g$ by $I \in \Delta(x)$.

755: Further, ``$0\in X_0$'' abbreviates $\forall x\, (\mathit{zero}(x) \implies

756: x \in X_0)$ where $\mathit{zero}(x)$ in turn stands for

757: $\notof\exists y (y < x)$.

758: Similarly $x+1 \in X_j$ can be expressed via 

759: $\forall y (\mathit{succ}_x(y) \implies y \in X_j)$, where

760: $\mathit{succ}_x(y)$ is the formula $x < y \ \And \ \notof\exists

761: z (x < z \ \And \ z < y)$.

762: 

763: In the converse direction we take the route used in \cite{d03} as

764: it will be useful in the sequel.

765: Let $\varphi$ be a formula in $\tmso{\Sigma, \Op}$, and let

766: $\Gamma$ be a \emph{proper} symbolic alphabet with the same

767: interval vocabulary as $\varphi$.

768: We give a way of translating $\varphi$

769: to a formula $\ttos{\varphi}$ in

770: $\mso{\Gamma}$ in such a way that the timed languages are

771: preserved.

772: The translation $\ttosfn$ is done with respect to $\Gamma$ and

773: simply replaces each occurrence of 

774: \[Q_a(x) \mathrm{\ \ by \ }

775: \bigvee_{(b,h) \in \Gamma,\ b=a} Q_{(b,h)}(x)

776: \mathrm{\ \ and \ \ } I \in \Delta(x) \mathrm{\ \ by \ }

777: \bigvee_{(a,h) \in \Gamma, \ I \in h(\Delta)} Q_{(a,h)}(x).

778: \]

779: %

780: The translation preserves the timed models of a formula $\varphi$ in the

781: following sense:

782: \begin{lemma}

783: Let $\sigma \in \two{\Sigma}$, $\gamma \in \Gamma^{\omega}$, and

784: $\sigma \in \twfn_{\Gamma}(\gamma)$.

785: Let $\mathbb{I}$ be an interpretation for variables.

786: Then $\sigma, \mathbb{I} \models \varphi$ iff $\gamma, \mathbb{I}

787: \models \ttos{\varphi}$.

788: \qed

789: \end{lemma}

790: 

791: The lemma is easy to prove using induction on the structure of the

792: formula $\varphi$ and making use of the properties of proper symbolic

793: alphabets.

794: From the lemma it immediately follows now that for a sentence

795: $\varphi$ in $\tmso{\Sigma,\Op}$, we have $L(\varphi) =

796: \twfn_{\Gamma}(L(\ttos{\varphi}))$, 

797: and this is the sense in which the translation

798: preserves timed languages.

799: %% Let $\sigma \in \two{\Sigma}$ with $\sigma \models \varphi$.

800: %% Then, since $\Gamma$ is proper, by Lemma~\ref{lemma:proper1} we

801: %% know that there exists $\gamma \in \Gamma^{\omega}$ such that

802: %% $\sigma \in \tw{\gamma}$.

803: %% By Lemma~\ref{lemma:stot1} we now have that $\gamma \models \varphi

804: 

805: 

806: We can now argue the converse direction of

807: Theorem~\ref{thm:msoba1}

808: using this translation and

809: factoring through B\"uchi's theorem.

810: Let $\varphi$ be a sentence in $\tmso{\Sigma, \Op}$ and let

811: $\widehat{\varphi} = \ttos{\varphi}$.

812: Then by B\"uchi's theorem we have an automaton $\mathcal{A}$ 

813: over $\Gamma$ which recognises exactly $L(\widehat{\varphi})$.

814: Thus $\mathcal{A}$ is our required proper \idta\, since

815: $L(\mathcal{A}) = \twfn_{\Gamma}(\lsymb{\mathcal{A}}) =

816: \twfn_{\Gamma}(L(\widehat{\varphi})) = L(\varphi)$.

817: \qed

818: \end{proof}

819: 

820: 

821: \section{An expressively complete timed $\ltll$}

822: \label{section:tltl}

823: 

824: In this section we identify a

825: natural, expressively complete, timed temporal logic based on

826: input determined operators.

827: The logic is denoted $\tltl{\Sigma,\Op}$, parameterised by the

828: alphabet $\Sigma$ and set of input determined operators $\Op$.

829: The formulas of $\tltl{\Sigma,\Op}$ are given by:

830: \[

831: \theta ::= \ a \ | \

832: I \in \Delta \ | \

833: \O \theta \ | \ 

834: \Ominus \theta \ | \ 

835: (\theta \U \theta) \ | \

836: (\theta \S \theta) \ | \

837: \notof \theta \ | \

838: (\theta \Or \theta).

839: \]

840: Here we require $a \in \Sigma$, $I \in \intervals$, and $\Delta \in \Op$.

841: %

842: The models for $\tltl{\Sigma, \Op}$ formulas are

843: timed words over $\Sigma$.

844: Let $\sigma \in \two{\Sigma}$, with $\sigma = (\alpha, \tau)$,

845: and let $i \in \nat $.

846: Then the satisfaction relation $\sigma, i \models \varphi$

847: is given by

848: \[

849: \begin{array}{lll}

850: % \sigma, i \models \true \\

851: \sigma, i \models a & \mathrm{\ iff \ } & \alpha(i) = a \\

852: \sigma, i \models I \in \Delta & \mathrm{\ iff \ } &

853:      I \in \sem{\Delta}(\sigma, i) \\

854: \sigma, i \models \O \theta & \mathrm{\ iff \ } & 

855:      \sigma, i+1 \models \theta \\

856: \sigma, i \models \Ominus \theta & \mathrm{\ iff \ } & 

857:      i > 0 \mathrm{\ and \ } \sigma, i-1 \models \theta \\

858: \sigma, i \models \theta \U \eta & \mathrm{\ iff \ } &

859: \exists k \geq i:\, \sigma, k \models \eta \mathrm{\ and \ }

860: \forall j:\, i \leq j < k, \ \sigma, j \models \theta \\

861: \sigma, i \models \theta \S \eta & \mathrm{\ iff\ } &

862: \exists k < i:\, \sigma, k \models \eta \mathrm{\ and \ }

863: \forall j:\, k < j \leq i, \ \sigma, j \models \theta \\

864: %% \sigma, i \models \notof{\theta} & \mathrm{iff} & \sigma,

865: %% i \not\models \theta \\

866: %% \sigma, i \models \theta \Or \eta & \mathrm{iff} &

867: %% \sigma, i \models \theta 

868: %% \mathrm{ \ or \ } \sigma, i \models \eta \\

869: \end{array}

870: \]

871: %

872: We define $L(\theta) = 

873: \{ \sigma \in \two{\Sigma} \ | \ \sigma, 0 \models \varphi \}$.

874: 

875: Let us denote by $\tfo{\Sigma, \Op}$ the first-order fragment of

876: $\tmso{\Sigma, \Op}$ (i.e. the fragment we get by disallowing

877: quantification over set variables).

878: The logics $\tltll$ and $\tfol$ are \emph{expressively equivalent}

879: in the following sense:

880: 

881: \begin{theorem}

882: \label{thm:ltl1}

883: A timed language $L \subseteq \two{\Sigma}$ is definable

884: by a $\tltl{\Sigma, \Op}$ formula $\theta$ iff

885: it is definable by a sentence $\varphi$ in $\tfo{\Sigma,\Op}$.

886: \end{theorem}

887: 

888: \begin{proof}

889: Given a $\tltl{\Sigma, \Op}$ formula $\theta$ we can associate an

890: $\tfo{\Sigma, \Op}$ formula $\varphi$ which has a single free variable

891: $x$, and satisfies the property that $\sigma, i \models \theta$ iff 

892: $\sigma, [i/x] \models \varphi$.

893: This can be done in a straightforward inductive manner as follows.

894: For the atomic formulas $a$ and $I \in \Delta$ we can take $\varphi$ to be 

895: $Q_a(x)$ and $I \in \Delta(x)$ respectively.

896: In the inductive step, assuming we have already translated $\theta$

897: and $\eta$ into $\varphi$ and $\psi$ respectively, we can translate

898: $\theta \U \eta$ into 

899: \[

900: \exists y (x \leq y \And \psi[y/x] \And \forall z ((x \leq z \And z \leq

901: y) \implies \varphi[z/x])).

902: \]

903: Here $\psi[y/x]$ denotes the standard renaming of the free variable

904: $x$ to $y$ in $\psi$.

905: The remaining modalities are handled in a similar way, and we can

906: verify that if $\varphi$ is the above translation of $\theta$

907: then $\sigma, i \models \theta$ iff

908: $\sigma, [i/x] \models \varphi$.

909: It also follows that $\sigma,0$ satisfies $\theta$ iff

910: $\sigma$ satisfies the sentence $\varphi_0$ given by

911: $\forall x (\mathit{zero}(x) \implies \varphi)$.

912: Hence we have that $L(\theta) = L(\varphi_0)$.

913: 

914: In the converse direction a more transparent proof is

915: obtained by factoring through Kamp's result

916: for classical LTL.

917: Recall that the syntax of $\ltl{A}$ is given by:

918: \[

919: \theta ::= \ a \ | \

920: \O \theta \ | \

921: \Ominus \theta \ | \

922: (\theta \U \theta) \ | \

923: (\theta \S \theta) \ | \

924: \notof{\theta} \ | \

925: (\theta \Or \theta)

926: \]

927: where $a \in A$.

928: The semantics is given in a similar manner to $\tltll$, except that

929: models are words in $A^{\omega}$.

930: In particular the satisfaction relation $\alpha, i \models \theta$

931: for the atomic formula $a$ is given by:

932: $\sigma, i \models a$ iff $\alpha(i) = a$.

933: % \[

934: % \begin{array}{lll}

935: % \sigma, i \models a & \mathrm{iff} & \alpha(i) = a.

936: % \end{array}

937: % \]

938: Let $\fo{A}$ denote the first-order fragment of $\mso{A}$.

939: Then the result due to Kamp \cite {k68} states that:

940: \begin{theorem}[\cite{k68}]

941: \label{thm:kamp1}

942: $\ltl{A}$ is expressively equivalent to $\fo{A}$.

943: \qed

944: \end{theorem}

945: 

946: Consider now a proper symbolic alphabet $\Gamma$ based on $(\Sigma, \Op)$.

947: We can define a timed language preserving 

948: translation of an $\ltl{\Gamma}$ formula

949: $\widehat{\theta}$ to a formula $\stot{\widehat{\theta}}$ in

950: $\tltl{\Sigma, \Op}$.

951: In the translation $\stotfn$ we replace subformulas $(a,h)$ by

952: \[

953: a \And \bigwedge_{\Delta \in \Op}(\bigwedge_{I \in h(\Delta)} (I \in \Delta)

954: \ \And \ \bigwedge_{I \in \ivoc{\Gamma} - h(\Delta)} 

955:                               \notof{(I \in \Delta)}).

956: \]

957: %

958: It is easy to argue along the lines of Lemma~\ref{lemma:proper1} that

959: \begin{lemma}

960: \label{lemma:stot-ltl}

961: Let $\sigma \in \two{\Sigma}$ and $\gamma \in \Gamma^{\omega}$ with

962: $\sigma \in \twfn_{\Gamma}(\gamma)$.

963: Then $\sigma, i \models \stot{\widehat{\theta}}$ iff $\gamma, i \models

964: \widehat{\theta}$.

965: \qed

966: \end{lemma}

967: Hence we have $L(\stot{\widehat{\theta}}) = \twfn_{\Gamma}(L(\widehat{\theta}))$.

968: 

969: We can now translate a sentence $\varphi$ in $\tfo{\Sigma, \Op}$ to

970: an equivalent $\tltl{\Sigma, \Op}$ formula $\theta$ as follows.

971: Let $\Gamma$ be the proper symbolic alphabet based on $(\Sigma, \Op)$

972: with the same interval vocabulary as $\varphi$.

973: Let $\widehat{\varphi}$ be the $\fo{\Gamma}$ formula $\ttos{\varphi}$.

974: Note that the translation $\stotfn$ preserves first-orderness and

975: hence $\widehat{\varphi}$ belongs to $\fo{\Gamma}$.

976: Now by Theorem~\ref{thm:kamp1}, we have a formula $\widehat{\theta}$ in

977: $\ltl{\Gamma}$ which is equivalent to $\widehat{\varphi}$.

978: We now use the translation $\ttosfn$ on the formula $\widehat{\theta}$

979: to get a $\tltl{\Sigma, \Op}$ formula $\theta$.

980: $\theta$ is our required $\tltl{\Sigma, \Op}$ formula.

981: Observe that firstly

982: $L(\theta) = \twfn_{\Gamma}(L(\widehat{\theta}))$ by the property of the

983: translation $\stotfn$.

984: Next, by Kamp's theorem we have that $L(\widehat{\theta}) =

985: L(\widehat{\varphi})$ and hence

986: $\twfn_{\Gamma}(L(\widehat{\theta})) =

987: \twfn_{\Gamma}(L(\widehat{\varphi}))$.

988: But by the property of the translation $\ttosfn$ applied to

989: $\varphi$, we have 

990: $\twfn_{\Gamma}(L(\widehat{\varphi})) = L(\varphi)$, and hence we can

991: conclude that $L(\varphi) = L(\theta)$.

992: %

993: This completes the proof of Theorem~\ref{thm:ltl1}.

994: \qed

995: \end{proof}

996: 

997: We point out here that the past temporal operators of $\Ominus$

998: (``previous'') and $\S$ (``since'') can be dropped from

999: our logic without affecting the

1000: expressiveness of the logic.

1001: This follows since it is shown in \cite{gpss80} that

1002: Theorem~\ref{thm:kamp1} holds for the future fragment of $\ltll$.

1003: The reason we retain the past operators is because they are needed

1004: when we consider a recursive version of the logic in

1005: Section~\ref{section:rltl}.

1006: 

1007: 

1008: \section{Recursive input determined automata}

1009: 

1010: We now consider ``recursive'' input determined operators.

1011: The main motivation is to increase the expressive power of our

1012: automata, as well as to characterise the expressiveness of

1013: recursive temporal logics which occur naturally in the real-time

1014: setting.

1015: 

1016: To introduce recursion in our operators, we need to consider

1017: \emph{parameterised} (or \emph{recursive}) input determined operators.

1018: These operators, which we continue to denote by $\Delta$,

1019: have a semantic function $\sem{\Delta} : (2^{\nat} \times \two{\Sigma}

1020: \times \nat) \rightarrow 2^{\intervals}$, whose first argument

1021: is a subset of positions $X$.

1022: Thus $\Delta$ with the parameter $X$ determines 

1023: an input determined operator of

1024: the type introduced earlier, whose semantic function is given by

1025: the map $(\sigma, i) \mapsto \sem{\Delta}(X, \sigma, i)$.

1026: The set of positions $X$ will typically be specified by a

1027: temporal logic formula or a  ``floating'' automaton,

1028: in the sense

1029: that given a timed word $\sigma$, the formula (resp. automaton) will

1030: identify a set of positions in $\sigma$ where the formula is

1031: satisfied (resp. automaton accepts).

1032: These ideas will soon be made more precise.

1033: 

1034: We first recall the idea of a ``floating'' automaton introduced in

1035: \cite{hrs98}.

1036: These are automata which accept pairs of the form $(\sigma, i)$

1037: with $\sigma$ a timed word, and $i$ a position (i.e.\@ $i \in

1038: \nat)$.

1039: We will represent a ``floating'' word $(\sigma,i)$ as a timed

1040: word over $\Sigma \times \{0,1\}$.

1041: Thus a timed word $\nu$ over $\Sigma \times \{0,1\}$

1042: represents the floating word $(\sigma, i)$, iff

1043: $\nu = (\alpha, \beta, \tau)$, with $\beta \in \{0,1\}^{\omega}$ with a

1044: \emph{single} $1$ in the $i$-th position, 

1045: and $\sigma = (\alpha, \tau)$.

1046: We use $\fwfn$ to denote the (partial) map which given a timed word $\nu$

1047: over $\Sigma \times \{0,1\}$ returns the floating word $(\sigma,

1048: i)$ corresponding to $\nu$, and extend it to apply to timed languages

1049: over $\Sigma \times \{0,1\}$ in the natural way.

1050: 

1051: Let $\Op$ be a set of input determined operators w.r.t. $\Sigma$.

1052: Then a \emph{floating \idta} over $(\Sigma, \Op)$ is an \idta\

1053: over $(\Sigma \times \{0,1\}, \Op')$, where the set of operators

1054: $\Op'$ w.r.t. $\Sigma \times \{0,1\}$ is defined to be $\{ \Delta' \

1055: | \ \Delta \in \Op \}$, with the semantics

1056: \[

1057: \sem{\Delta'}(\sigma', i) = \sem{\Delta}(\sigma, i),

1058: \]

1059: where $\sigma'$ is a timed word over $\Sigma \times \{0,1\}$,

1060: with $\sigma' = (\alpha, \beta, \tau)$ and $\sigma = (\alpha,

1061:  \tau)$.

1062: Thus the operator $\Delta'$ simply ignores the $\{0,1\}$ component

1063: of $\sigma'$ and behaves like $\Delta$ on the $\Sigma$ component.

1064: A floating \idta\ $\mathcal{B}$ accepts the floating

1065: timed language $L^f(\mathcal{B}) = \fw{L(\mathcal{B})}$.

1066: 

1067: We now give a more precise definition of recursive input

1068: determined automata, denoted \ridta, and their floating

1069: counterparts \fridta.

1070: Let $\Rop$ be a finite set of recursive input determined

1071: operators.

1072: Then the class of \ridta's over $(\Sigma, \Rop)$, and the timed

1073: languages they accept, are defined as follows.

1074: \begin{itemize}

1075: \item

1076: Every \idta\ $\mathcal{A}$ over $\Sigma$ that uses only the guard

1077: $\true$ is a \ridta\ over $(\Sigma,\Rop)$, and

1078: accepts the timed language $L(\mathcal{A})$.

1079: 

1080: Similarly, every floating \idta\ $\mathcal{B}$ over $\Sigma$ which uses

1081: only the guard $\true$ is

1082: a \fridta\ over $(\Sigma, \Rop)$, and accepts the floating language

1083: $L^f(\mathcal{B})$.

1084: 

1085: \item

1086: Let $C$ be a finite collection of \fridta's over $(\Sigma, \Rop)$.

1087: Let $\Op$ be the set of input determined operators

1088: $\{\Delta_{\mathcal{B}} \ | \ \Delta \in \Rop, \ \mathcal{B} \in C

1089: \}$, where the semantic function of each $\Delta_{\mathcal{B}}$ is

1090: given as follows.

1091: Let $\pos{\sigma, \mathcal{B}}$ denote the set of positions $i$

1092: such that $(\sigma, i) \in L^f(\mathcal{B})$.

1093: Then $\sem{\Delta_{\mathcal{B}}}(\sigma, i) =

1094: \sem{\Delta}(\pos{\sigma, \mathcal{B}}, \sigma, i)$.

1095: 

1096: Then any \idta\ $\mathcal{A}$ over $(\Sigma, \Op)$

1097: is a \ridta\ over $(\Sigma, \Rop)$, and accepts the timed

1098: language $L(\mathcal{A})$ (defined in 

1099: Section~\ref{section:idta}).

1100: 

1101: Similarly every floating \idta\ $\mathcal{B}$ 

1102: over $(\Sigma, \Op)$ 

1103: is a \fridta\ over $(\Sigma, \Rop)$, and

1104: accepts the floating language $L^f(\mathcal{B})$.

1105: \end{itemize}

1106: 

1107: Recursive automata fall into a natural ``level'' based on the

1108: level of nesting of operators they use.

1109: A \ridta\ is of \emph{level} 0 if the only guard it uses is

1110: $\true$.

1111: Similarly a \fridta\ is of level 0, if the only guard it uses is

1112: $\true$.

1113: A \ridta\ is of \emph{level} (i+1) if it uses an operator

1114: $\Delta_{\mathcal{B}}$, with $\Delta \in \Rop$

1115: and $\mathcal{B}$ a \fridta\ of level $i$,

1116: and no operator $\Delta'_{\mathcal{C}}$ with $\Delta' \in \Rop$ and

1117: $\mathcal{C}$ of level greater than $i$.

1118: A similar definition of level applies to \fridta's.

1119: 

1120: As an example consider the level 1 \ridta\ $\mathcal{A}$ over the alphabet

1121: $\{a,b\}$ below.

1122: The floating automaton $\mathcal{B}$ accepts a floating word

1123: $(\sigma, i)$ iff the position $i$ is labelled $b$ and the

1124: previous and next positions are labelled $a$.

1125: The recursive input determined operator $\F$ is defined formally

1126: in Sec.~\ref{section:mitl}.

1127: The \ridta\ $\mathcal{A}$ thus recognises the set of timed words

1128: $\sigma$ over $\{a,b\}$ which begin with an $a$ and have an

1129: occurrence of $b$ -- with $a$'s on its left and right -- exactly 1

1130: time unit later.

1131: \begin{center}

1132:   \includegraphics[width=\textwidth]{ridta.eps}

1133: \end{center}

1134: %

1135: \begin{theorem}

1136: \label{thm:closure2}

1137: The class of \ridta's over $(\Sigma, \Rop)$ is closed under boolean

1138: operations.

1139: In fact, for each $i$, the class of level $i$ \ridta's is closed

1140: under boolean operations.

1141: \end{theorem}

1142: 

1143: \begin{proof}

1144: Let $\mathcal{A}$ and $\mathcal{A}'$ be two \ridta's of level $i$.

1145: Let $\Op$ be the union of operators used in $\mathcal{A}$ and

1146: $\mathcal{A}'$.

1147: Then both $\mathcal{A}$ and $\mathcal{A}'$ are \idta's

1148: over $(\Sigma, \Op)$, and hence by

1149: Theorem~\ref{thm:closure1} there exists an \idta\ 

1150: $\mathcal{B}$ over $(\Sigma, \Op)$ which accepts

1151: $L(\mathcal{A}) \union L(\mathcal{A}')$.

1152: Similarly there exists an \idta\ $\mathcal{C}$ over $(\Sigma, \Op)$,

1153: which accepts the

1154: language $\two{\Sigma} - L(\mathcal{A})$.

1155: Notice that $\mathcal{B}$ and $\mathcal{C}$ use the same set of

1156: operators $\Op$, and hence are also

1157: level $i$ automata.

1158: \qed

1159: \end{proof}

1160: 

1161: We note that \idta's over $(\Sigma, \Op)$ are a special case of level

1162: 1 \ridta's over $(\Sigma, \Rop)$, where the set of recursive

1163: operators $\Rop$ is taken to be $\{ \Delta' \ | \, \Delta \in

1164: \Op\}$ with $\sem{\Delta'}(X,\sigma,i) = 

1165: \sem{\Delta}(\sigma,i)$.

1166: Thus each guard $I \in \Delta$ in an \idta\ over $(\Sigma, \Op)$

1167: can be replaced by the guard $I \in

1168: \Delta'_{\mathcal{B}}$, for any ``dummy'' level 0

1169: \fridta\ $\mathcal{B}$.

1170: 

1171: 

1172: \section{MSO characterisation of \ridta's}

1173: \label{section:mso2}

1174: 

1175: We now introduce a recursive version of $\tmsol$ which will

1176: characterise the class of timed languages defined by \ridta's.

1177: The logic is parameterised by an alphabet $\Sigma$ and set of

1178: recursive input determined operators $\Rop$, and denoted

1179: $\rtmso{\Sigma, \Rop}$.

1180: The syntax of the logic is given by

1181: \[

1182: \varphi ::= Q_a(x) \ | \ I \in \Delta_{\psi}(x) \ | \ 

1183: x \in X \ | \ x < y \ | \ 

1184: \notof{\varphi} \ | \ (\varphi \Or \varphi)

1185: \ | \ \exists x \varphi \ | \ \exists X \varphi.

1186: \]

1187: In the predicate $I \in \Delta_{\psi}(x)$, 

1188: we have $I \in \intervals$, $\Delta

1189: \in \Rop$, and $\psi$ a $\rtmso{\Sigma, \Rop}$ formula with a

1190: single free variable $z$.

1191: 

1192: The logic is interpreted over timed words in $\two{\Sigma}$.

1193: Its semantics is similar to $\tmsol$ except for the predicate ``$I

1194: \in \Delta_{\psi}(x)$'' which is defined inductively as follows.

1195: If $\psi$ is a formula which uses no $\Delta$ predicates, then the

1196: satisfaction relation $\sigma, \mathbb{I} \models \psi$ is defined

1197: as for $\tmsol$.

1198: Inductively, assuming the semantics of $\psi$ has already been

1199: defined, $\Delta_{\psi}$ is interpreted as an input determined

1200: operator as follows.

1201: Let $\pos{\sigma, \psi}$ denote the set of interpretations for $z$

1202: that make $\psi$ true in the timed word $\sigma$ --

1203: i.e. $\pos{\sigma, \psi} = \{ i \ | \ \sigma, [i/z] \models

1204: \psi\}$.

1205: Then

1206: \[

1207: \sem{\Delta_{\psi}}(\sigma, i) = 

1208: \sem{\Delta}(\pos{\sigma, \psi}, \sigma, i).

1209: \]

1210: Thus we have

1211: \[

1212: \sigma, \mathbb{I} \models I \in \Delta_{\psi}(x) \mathrm{\ iff \

1213: } I \in \sem{\Delta}(\pos{\sigma, \psi}, \sigma, \mathbb{I}(x)).

1214: \]

1215: 

1216: Note that the variable $z$, which is free in $\psi$, 

1217: is \emph{not} free in the formula $I

1218: \in \Delta_{\psi}(x)$.

1219: A sentence $\varphi$ in $\rtmso{\Sigma, \Rop}$ defines the

1220: language $L(\varphi) = \{ \sigma \models \varphi \}$, and

1221: a $\rtmso{\Sigma, \Rop}$ formula $\psi$ with one free variable $z$

1222: defines a floating language $L^f(\psi) = \{ \sigma, i \ | \

1223: \sigma, [i/z] \models \psi \}$.

1224: 

1225: We note that each $\rtmso{\Sigma, \Rop}$ formula $\varphi$ 

1226: can be viewed

1227: as a $\tmso{\Sigma, \Op}$ formula, for a suitably defined set of

1228: input determined operators $\Op$.

1229: We say an operator $\Delta_{\psi}$ has a \emph{top-level}

1230: occurrence in $\varphi$ if there is an occurrence of $\Delta_{\psi}$

1231: in $\varphi$ which is \emph{not} in the scope of any

1232: $\Delta'$ operator.

1233: We can now take $\Op$ to be the set of all top-level operators

1234: $\Delta_\psi$ in $\varphi$.

1235: 

1236: Analogous to the notion of level for \ridta's we can define the

1237: \emph{level} of an $\rtmsol$ formula $\varphi$.

1238: The level of $\varphi$ is 0, if $\varphi$ uses no $\Delta$

1239: predicates.

1240: $\varphi$ has level $i+1$ if it uses a predicate of the form $I

1241: \in \Delta_{\psi}(x)$ with $\psi$ a level $i$ formula, and

1242: \emph{no} predicate of the form $I \in \Delta'_{\phi}(x)$ with

1243: $\phi$ of level greater than $i$.

1244: 

1245: As an example the level 1 sentence $\varphi$ below defines the same timed

1246: language as the level 1 \ridta\ $\mathcal{A}$ defined in

1247: Section~\ref{section:idta}.

1248: We can take $\varphi$ to be

1249: \(

1250: \forall x (\mathit{zero}(x) \implies (Q_a(x)

1251: \And ([1,1] \in \F_{\psi}(x)))),

1252: \)

1253: where $\psi$ is the level 0 formula

1254: $Q_b(z) \And Q_a(z-1) \And Q_a(z+1)$.

1255: 

1256: 

1257: \begin{theorem}

1258: \label{thm:msoba2}

1259: $L \subseteq \two{\Sigma}$ is accepted by a \ridta\ over $(\Sigma,

1260:   \Rop)$ iff $L$ is definable by a $\rtmso{\Sigma, \Rop}$ sentence.

1261: \end{theorem}

1262: 

1263: In fact, we will show that for each $i$, the class of \ridta's of level $i$

1264: correspond to the sentences of $\rtmso{\Sigma, \Rop}$ of level

1265: $i$.

1266: But first it will be useful to state a

1267: characterisation of floating languages along the lines of

1268: Theorem~\ref{thm:msoba1}.

1269: 

1270: \begin{theorem}

1271: \label{thm:msobaf1}

1272: Let $L$ be a a floating language over $\Sigma$.

1273: Then $L = L^f(\mathcal{B})$ for some floating \idta\ over

1274: $(\Sigma, \Op)$ iff $L = L^f(\psi)$, for some 

1275: $\tmso{\Sigma, \Op}$ formula $\psi$ with one free variable.

1276: \end{theorem}

1277: 

1278: \begin{proof}

1279: Let $\mathcal{B}$ be a floating \idta\ over $(\Sigma, \Op)$.

1280: Keeping in mind that $\mathcal{B}$ runs over the alphabet $\Sigma

1281: \times \{0,1\}$, we define a formula $\psi$ with one free variable

1282: $z$ as follows.

1283: $\psi$ is the formula $\varphi$ given in the proof

1284: of Theorem~\ref{thm:msoba1}, except for the clause (*) which we

1285: replace by

1286: 

1287: \begin{eqnarray*}

1288: %\lefteqn{  }

1289:               & & \And \ \forall x ((x = z) \implies

1290: \displaystyle{\bigvee_{q_i \aedge{((a,1),g)} q_j}}

1291: 	         (x \in X_i \ \And \ (x+1) \in X_j \ \And

1292:                   Q_a(x) \And g') \\

1293:                   & & \ \ \ \ \ \ \ \ \And \ (x \neq z) \implies

1294: \displaystyle{\bigvee_{q_i \aedge{((a,0),g)} q_j}}

1295: 	         (x \in X_i \ \And \ (x+1) \in X_j \ \And

1296:                   Q_a(x) \And g')).

1297: \end{eqnarray*}

1298: The formula $\psi$ satisfies $(\sigma,i) \in L^f(\mathcal{B})$ iff

1299: $\sigma, [i/z] \models \psi$.

1300: 

1301: In the converse direction, let $\varphi(m,n)$ denote a

1302: $\tmso{\Sigma, \Op}$ formula with free variables $x_1,\ldots,x_m,

1303: X_1 \ldots X_n$.

1304: An interpretation $\mathbb{I}$ for these variables is encoded

1305: (along with $\sigma$) as a timed word over $\Sigma \times

1306: \{0,1\}^{m+n}$.

1307: We extend the definition of a floating \idta\ to an \idta\ which

1308: works over such an alphabet, where, in particular, the $\Delta$ operators

1309: apply only to the $\Sigma$ component of the timed word.

1310: Then we can inductively associate with $\varphi(m,n)$ 

1311: a floating \idta\ $\mathcal{B}$

1312: over $\Sigma \times \{0,1\}$ such that $L^f(\mathcal{B}) =

1313: L^f(\varphi)$.

1314: In the inductive step for $\exists X_n(\varphi(m,n))$ we make use

1315: of the fact that the class of languages accepted by floating

1316: \idta's over $(\Sigma, \Op)$ are closed under the restricted

1317: renaming operation required in this case.

1318: The reader is referred to \cite{d03} for a similar argument.

1319: \qed

1320: \end{proof}

1321: 

1322: Returning now to the proof of Theorem~\ref{thm:msoba2}, we use

1323: induction on the level of automata and formulas to argue that

1324: \begin{enumerate}

1325: \item

1326: $L \subseteq \two{\Sigma}$ is accepted by a level $i$ \ridta\ over

1327:   $(\Sigma, \Rop)$ iff $L$ is definable by a level $i$

1328:   $\rtmso{\Sigma, \Rop}$ sentence $\varphi$. And

1329: \item

1330: \label{item:float}

1331: A floating language $L$ over $\Sigma$

1332: is accepted by a level $i$ \fridta\ over

1333:   $(\Sigma, \Rop)$ iff $L$ is definable by a level $i$

1334:   $\rtmso{\Sigma, \Rop}$ formula $\psi$ with one free variable.

1335: \end{enumerate}

1336: 

1337: For the base case we consider level 0 automata and sentences.

1338: Since level 0 automata only make use of the guard $\true$, they

1339: are simply B\"uchi automata over $\Sigma$.

1340: Similarly, level 0 sentences don't use any $\Delta$ predicates and

1341: hence they are simply $\mso{\Sigma}$ sentences.

1342: By B\"uchi's theorem, we have that level 0 automata and

1343: sentences are expressively equivalent.

1344: 

1345: For the base case for the second part of the claim, given a level

1346: 0 floating automaton $\mathcal{B}$ we can apply the construction

1347: in the proof of Theorem~\ref{thm:msobaf1} to get a $\tmso{\Sigma}$

1348: formula $\psi$ with one free variable.

1349: Since the construction preserves the guards used, $\psi$ has no

1350: $\Delta$ operators, and hence is a level 0 $\rtmso{\Sigma, \Rop}$

1351: formula.

1352: Conversely, for a level 0 formula $\psi$ we can apply the

1353: construction of Theorem~\ref{thm:msobaf1} to obtain a floating

1354: automaton $\mathcal{B}$ such that $L^f(\mathcal{B}) = L^f(\psi)$.

1355: The construction preserves the $\Delta$ operators used,

1356: and hence $\mathcal{B}$ is a level 0 automaton.

1357: 

1358: Turning now to the induction step, let $\mathcal{A}$ be a level

1359: $i+1$ automaton over $(\Sigma, \Rop)$.

1360: Let $\Op$ be the set of top-level $\Delta$ operators in

1361: $\mathcal{A}$.

1362: Now since $\mathcal{A}$ is an \idta\  over $(\Sigma, \Op)$, by

1363: Theorem~\ref{thm:msoba1}, we have a $\tmso{\Sigma, \Op}$ sentence

1364:   $\varphi$ such that $L(\mathcal{A}) = L(\varphi)$.

1365: Now for each $\Delta_{\mathcal{B}}$ in $\Op$, $\mathcal{B}$ is of

1366: level $i$ or lower, and by our induction hypothesis there is a

1367: corresponding $\rtmso{\Sigma, \Rop}$ formula

1368: $\psi$ with one free variable, of the same level as $\mathcal{B}$,

1369: with $L^f(\mathcal{B}) = L^f(\psi)$.

1370: Hence for each $\Delta_{\mathcal{B}}$ we have a

1371: semantically equivalent operator $\Delta_{\psi}$.

1372: This is because $L^f(\mathcal{B}) = L^f(\psi)$, which implies 

1373: $\pos{\sigma, \mathcal{B}} = \pos{\sigma, \psi}$, which in turn

1374: implies $\sem{\Delta_{\mathcal{B}}} = \sem{\Delta_{\psi}}$.

1375: We can now simply replace each occurrence of

1376: $\Delta_{\mathcal{B}}$ in $\varphi$ to get an equivalent sentence

1377: $\varphi'$ which is in $\rtmso{\Sigma, \Rop}$.

1378: Further, by construction it follows that $\varphi'$ is also of

1379: level $i+1$.

1380: 

1381: Conversely, let $\varphi$ be a level $i+1$ sentence in

1382: $\rtmso{\Sigma, \Rop}$.

1383: Let $\Op$ be the set of top level $\Delta$ operators in $\varphi$.

1384: Then $\varphi$ is a $\tmso{\Sigma, \Op}$ sentence, and hence by

1385: Theorem~\ref{thm:msoba1} we have an equivalent input determined

1386: automaton $\mathcal{A}$ over $(\Sigma, \Op)$.

1387: Once again, for each $\Delta_{\psi}$ in $\Op$, the formula $\psi$ is of level

1388: $i$ or lower, and hence by induction hypothesis we have a 

1389: \fridta\ $\mathcal{B}$ over $(\Sigma, \Rop)$, of the same level as

1390: $\psi$, and accepting the same floating language.

1391: The operators $\Delta_{\psi}$ and $\Delta_{\mathcal{B}}$ are now

1392: equivalent, and we can replace each $\Delta_{\psi}$ in

1393: $\mathcal{A}$ by the corresponding $\Delta_{\mathcal{B}}$ to get

1394: a language equivalent input determined automaton.

1395: This automaton is now the required level $i+1$ \ridta\ over

1396: $(\Sigma, \Rop)$ which accepts the same language as $L(\varphi)$.

1397: 

1398: The induction step for part~\ref{item:float} is proved

1399: similarly, making use of Theorem~\ref{thm:msobaf1} and the

1400: induction hypothesis.

1401: This completes the proof of Theorem~\ref{thm:msoba2}.

1402: \qed

1403: 

1404: 

1405: \section{Expressive completeness of \rtltll}

1406: \label{section:rltl}

1407: 

1408: We now define a recursive timed temporal logic along the lines of

1409: \cite{hrs98}.

1410: The logic is similar to the logic $\tltll$ defined in

1411: Sec.~\ref{section:tltl}.

1412: It is parameterised by an alphabet $\Sigma$ and a set of

1413: recursive input determined operators $\Rop$, and denoted

1414: $\rtltl{\Sigma, \Rop}$.

1415: The syntax of the logic is given by

1416: \[

1417: \theta ::= \ a \ | \

1418: I \in \Delta_{\theta} \ | \

1419: \O \theta \ | \ 

1420: \Ominus \theta \ | \ 

1421: (\theta \U \theta) \ | \

1422: (\theta \S \theta) \ | \

1423: \notof \theta \ | \

1424: (\theta \Or \theta),

1425: \]

1426: where $a \in \Sigma$, and $\Delta \in \Rop$.

1427: 

1428: The logic is interpreted over timed words in a similar manner to

1429: $\tltll$.

1430: The predicate $I \in \Delta_{\theta}$ is interpreted as follows.

1431: If $\theta$ does not use a $\Delta$ predicate, then the

1432: satisfaction relation $\sigma, i \models \theta$ is defined as for

1433: $\tltll$.

1434: Inductively assuming the semantics of a $\rtltl{\Sigma, \Rop}$

1435: formula $\theta$ has been defined, 

1436: and setting

1437: $\pos{\sigma, \theta} = \{ i \in \nat \ | \ \sigma, i \models

1438: \theta \}$,

1439: the operator $\Delta_{\theta}$

1440: is interpreted as an input determined operator with the semantic

1441: function

1442: \[

1443: \sem{\Delta_{\theta}}(\sigma, i) =

1444: \sem{\Delta}(\pos{\sigma, \theta}, \sigma, i).

1445: \]

1446: The satisfaction relation $\sigma, i \models I \in

1447: \Delta_{\theta}$ is then defined as in $\tltll$.

1448: % \[

1449: % \sigma, i \models I \in \Delta_{\theta} \mathrm{\ iff \ } I \in

1450: % \Delta(\pos{\sigma,\theta}, \sigma, i),

1451: % \]

1452: 

1453: Once again, since $\Delta_{\theta}$ behaves like an input determined

1454: operator, each $\rtltl{\Sigma, \Rop}$ formula is also a $\tltl{\Sigma,

1455: \Op}$ formula, for an appropriately chosen set of input determined

1456: operators $\Op$, containing operators of the form $\Delta_{\theta}$.

1457: %

1458: A $\rtltl{\Sigma, \Rop}$ formula $\theta$ naturally defines both 

1459: a timed language

1460: $L(\theta) = \{ \sigma \in \two{\Sigma} \ | \ \sigma, 0 \models \theta

1461: \}$ and 

1462: a floating language $L^f(\theta) = 

1463: \{(\sigma, i) \ | \ \sigma, i \models \theta \}$.

1464: 

1465: As an example, the formula $a \And ([1,1] \in \F_{\theta})$ where

1466: $\theta = b \And \Ominus a \And \O a$, 

1467: restates the property expressed by the $\rtmsol$ formula in

1468: Sec.~\ref{section:mso2}.

1469: 

1470: Let us denote by $\rtfo{\Sigma, \Rop}$ the first-order fragment of the

1471: logic $\rtmso{\Sigma, \Rop}$.

1472: Then we have the following expressive completeness result:

1473: 

1474: \begin{theorem}

1475: \label{thm:ltl2}

1476: $\rtltl{\Sigma, \Rop}$ is expressively equivalent to

1477: $\rtfo{\Sigma, \Rop}$.

1478: \end{theorem}

1479: 

1480: \begin{proof}

1481: As before we show that formulas in the logics are equivalent

1482: level-wise (the level of a $\rtltll$ formula 

1483: being defined analogous to $\rtmsol$).

1484: We show by induction on $i$ that

1485: \begin{enumerate}

1486: \item

1487: \label{item:ltl2:1}

1488: A timed language $L \subseteq \two{\Sigma}$ is definable by a level

1489: $i$ $\rtltl{\Sigma, \Rop}$ formula iff it is definable by a 

1490: level $i$ $\rtfo{\Sigma, \Rop}$ sentence.

1491: \item

1492: \label{item:ltl2:2}

1493: A floating timed language over $\Sigma$ is definable by a level $i$

1494: $\rtltl{\Sigma, \Rop}$ formula iff it is definable by a level $i$

1495: $\rtfo{\Sigma, \Rop}$ formula with one free variable.

1496: \end{enumerate}

1497: 

1498: The base case for part~\ref{item:ltl2:1} follows from

1499: Theorem~\ref{thm:kamp1}, since level 0 formulas are simply untimed

1500: $\ltl{\Sigma}$ and $\fo{\Sigma}$ formulas.

1501: %

1502: For the base case for part~\ref{item:ltl2:2}, a level 0

1503: $\rtltl{\Sigma, \Rop}$ formula $\theta$ can be translated to a level 0

1504: $\rtfo{\Sigma, \Rop}$ formula $\psi$ with one free variable $z$ using

1505: the translation given in the proof of Theorem~\ref{thm:ltl1}.

1506: The formula $\psi$ satisfies $\sigma, [i/z] \models \psi$ iff 

1507: $\sigma, i \models \theta$.

1508: %

1509: The converse direction follows immediately from the

1510: following version of Kamp's result:

1511: \begin{theorem}[\cite{k68}]

1512: \label{thm:kamp2}

1513: For any $\fo{A}$ formula $\psi$ with one free variable $z$, 

1514: there is a $\ltl{A}$ formula $\theta$ s.t. for each $\alpha \in

1515: A^{\omega}$ and $i \in \nat$, $\alpha, [i/z] \models

1516: \psi$ iff $\alpha, i \models \theta$.

1517: \end{theorem}

1518: 

1519: Turning now to the induction step, let $\theta$ be a level $i+1$

1520: $\rtltl{\Sigma, \Rop}$ formula.

1521: Let $\Op$ be the set of top-level $\Delta$ operators used in $\theta$.

1522: Then $\theta$ is a $\tltl{\Sigma, \Op}$ formula, and hence by

1523: Theorem~\ref{thm:ltl1} we have an equivalent $\tfo{\Sigma, \Op}$

1524: sentence $\varphi$ (i.e. with $L(\theta) = L(\varphi)$).

1525: Now each operator in $\Op$ is of the form $\Delta_{\eta}$ where $\eta$

1526: is a level $i$ or less $\rtltl{\Sigma, \Rop}$ formula, and hence by

1527: the induction hypothesis we have an equivalent $\rtfo{\Sigma, \Rop}$

1528: formula $\psi$ with one free variable, such that $L^f(\eta) =

1529: L^f(\psi)$.

1530: It now follows that the input determined operators $\Delta_{\eta}$ and

1531: $\Delta_{\psi}$ are semantically equivalent, and hence we can replace

1532: each $\Delta_{\eta}$ by $\Delta_{\psi}$ in $\varphi$ to get an equivalent

1533: $\rtfo{\Sigma, \Rop}$ sentence $\varphi'$.

1534: By construction, the sentence $\varphi'$ is also of level $i+1$.

1535: The converse direction is argued in a very similar manner, once again

1536: factoring through Theorem~\ref{thm:ltl1}.

1537: 

1538: For part~\ref{item:ltl2:2}, a level $i+1$ $\rtltl{\Sigma, \Rop}$ 

1539: formula $\theta$ is a $\tltl{\Sigma, \Op}$ formula, for the set of

1540: operators $\Op$ defined above.

1541: Now using the translation given in the proof of Theorem~\ref{thm:ltl1}

1542: we obtain a $\tfo{\Sigma, \Op}$ formula $\psi$ with a one free

1543: variable, satisfying $L^f(\theta) = L^f(\psi)$.

1544: Again, by the induction hypothesis, we can replace each

1545: $\Delta_{\eta}$ in $\Op$ with an equivalent $\Delta_{\phi}$, to get an

1546: equivalent $\rtfo{\Sigma, \Rop}$ with the required properties.

1547: 

1548: In the converse direction, let $\psi$ be a level $i+1$ 

1549: $\rtfo{\Sigma, \Rop}$ formula with one free variable $z$.

1550: Let $\Op$ be set of top-level $\Delta$ operators in $\psi$.

1551: Then $\psi$ is also a formula in $\tfo{\Sigma, \Op}$.

1552: Let $\Gamma$ be the proper symbolic alphabet induced by $\psi$.

1553: Then we can use the translation $\ttosfn$

1554: (cf. Sec~\ref{section:tmso}) on $\psi$ (w.r.t. $\Gamma$) to get a

1555: formula $\widehat{\psi}$ in $\fo{\Gamma}$ with one free variable

1556: $z$ which preserves timed models.

1557: By Kamp's theorem above, we have an equivalent $\ltl{\Gamma}$ formula

1558: $\widehat{\theta}$

1559: which preserves the floating language accepted.

1560: Finally we can apply the translation $\stotfn$ on $\widehat{\theta}$

1561: to get a $\tltl{\Sigma, \Op}$ formula $\theta$ which preserves timed

1562: models (cf. Sec.~\ref{section:tltl}).

1563: The formula $\theta$ satisfies the property that $L^f(\theta) =

1564: L^f(\psi)$.

1565: 

1566: Now using the induction hypothesis each operator $\Delta_{\phi}$ in

1567: $\theta$ can be replaced

1568:  by an equivalent $\Delta_{\eta}$ operator, with

1569: $\eta$ a $\tltl{\Sigma, \Op}$ formula,

1570: to get an equivalent level $i+1$ $\rtltl{\Sigma, \Rop}$ formula

1571: $\theta'$.

1572: This ends the proof of Theorem~\ref{thm:ltl2}.

1573: \qed

1574: \end{proof}

1575: 

1576: 

1577: \section{Expressive completeness of $\mitll$}

1578: \label{section:mitl}

1579: 

1580: As an application of the results in this paper we

1581: show that the logic $\mitll$ introduced

1582: in \cite{afh96} is expressively equivalent to $\rtfol$ for a

1583: suitably defined set of recursive input determined operators.

1584: We point out here that this result is shown for the pointwise

1585: semantics of $\mitll$ given below.

1586: %

1587: We begin with the logic $\mitle{\Sigma}$ which has the following

1588: syntax \cite{ah93}:

1589: \[

1590: \theta ::= \ a \ | \

1591: \O \theta \ | \ 

1592: \Ominus \theta \ | \ 

1593: (\theta \U_I \theta) \ | \

1594: (\theta \S_I \theta) \ | \

1595: \notof \theta \ | \

1596: (\theta \Or \theta).

1597: \]

1598: Here $I$ is an interval in $\intervals$.

1599: When $I$ is restricted to be \emph{non-singular} (i.e. not of the

1600: form $[r,r]$) then we get the logic $\mitl{\Sigma}$.

1601: The logic is interpreted over timed words in $\two{\Sigma}$

1602: similarly to $\tltll$.

1603: The modalities $\U_I$ and $\S_I$ are interpreted as follows, for a

1604: timed word $\sigma = (\alpha, \tau)$.

1605: \[

1606: \begin{array}{lll}

1607: \sigma, i \models \theta \U_I \eta & \mathrm{iff} & 

1608:        \exists k \geq i:\, \sigma, k \models \eta, 

1609:        \tau(k) - \tau(i) \in I \mathrm, {\ and \ }

1610: \forall j:\, i \leq j < k, \ \sigma, j \models \theta \\

1611: \sigma, i \models \theta \S_I \eta & \mathrm{iff} &

1612:         \exists k \leq i:\, \sigma, k \models \eta,

1613:         \tau(i) - \tau(k) \in I, \mathrm{\ and \ }

1614: \forall j:\, k < j \leq i, \ \sigma, j \models \theta.

1615: \end{array}

1616: \]

1617: 

1618: We first observe that $\mitle{\Sigma}$ is expressively equivalent

1619: to its sublogic $\mitlde{\Sigma}$ in which the modalities $U_I$

1620: and $S_I$ are replaced by the modalities $U$, $S$, $\Fm_I$ and

1621: $\Fpm_I$, where $U$ and $S$ are as usual and 

1622: $\Fm_I \theta = \true \U_I \theta$ and $\Fpm_I \theta = \true

1623: \S_I \theta$.

1624: This is because the formula $\theta \U_{I} \eta$ (and dually

1625: $\theta S_I \eta$) can be translated as follows.

1626: Here `$\rangle$' denotes either a `$]$' or `$)$' interval bracket.

1627: \[

1628: \begin{array}{lcl}

1629: \theta \U_{I} \eta & = & \left \{

1630: 		\begin{array}{ll}

1631: 	 \Fm_{I} \eta \And \G_{[0,a)}(\theta \U

1632:               (\theta \And \O{\eta})) & \mathrm{if \ } I = [a,b\rangle, a>0 \\

1633:          \Fm_{I} \eta \And \G_{[0,a]}(\theta \U

1634:               (\theta \And \O{\eta})) & \mathrm{if \ } I = (a,b\rangle, a>0 \\

1635:          \Fm_{I} \eta \And (\theta \U \eta)

1636:                                        & \mathrm{if \ }I = [0,b\rangle \\

1637:          \Fm_{I} \eta \And (\theta \U (\theta

1638:               \And \O{\eta})) & \mathrm{if \ }I = (0,b\rangle.

1639: 	        \end{array}

1640: 	                  \right.

1641: \end{array}

1642: \]

1643: 

1644: Next we consider the logic

1645: $\rtltl{\Sigma, \{\F,\Fp\}}$ where the semantics of the

1646: recursive input

1647: determined operators $\F$ and $\Fp$ are given below (as usual

1648: $\sigma \in \two{\Sigma}$ with $\sigma = (\alpha, \tau)$).

1649: \[

1650: \begin{array}{lcl}

1651: \sem{\F}(X,\sigma, i) & = \{ I \in \intervals \ | \ \exists j \in

1652: X:\ j \geq i, \mathrm{\ and \ } \tau_j - \tau_i \in I \}\\

1653: \sem{\Fp}(X,\sigma, i) & = \{ I \in \intervals \ | \ \exists j \in

1654: X:\ j \leq i, \mathrm{\ and \ } \tau_i - \tau_j \in I \}.

1655: \end{array}

1656: \]

1657: The logic $\mitlde{\Sigma}$ is clearly expressively equivalent

1658: to $\rtltl{\Sigma, \{\F, \Fp\}}$ since the predicates $\Fm_{I} \theta$

1659: and $I \in \F_{\theta}$ are equivalent.

1660: %

1661: Using Theorem~\ref{thm:ltl2} we can now conclude that

1662: \begin{theorem}

1663: \label{thm:mitl}

1664: $\mitle{\Sigma}$ is expressively equivalent to $\rtfo{\Sigma,

1665:     \{\F, \Fp \}}$.

1666: \end{theorem}

1667: 

1668: Let $\rtfol_{\neq}$ denote the restriction of $\rtfol$ to

1669: non-singular intervals.

1670: Then since the translation of $\mitlel$ to $\mitldel$ does not

1671: introduce any singular intervals, and the constructions in

1672: Theorem~\ref{thm:ltl2} preserve the interval vocabulary of the

1673: formulas, we conclude that the logics

1674: $\mitl{\Sigma}$ and $\rtfol_{\neq}(\Sigma, \{\F, \Fp\})$ are

1675: expressively equivalent.

1676: 

1677: \begin{thebibliography}{9}

1678: 

1679: \bibitem{ad94} {R.~Alur, D.~L.~Dill: 

1680: A theory of timed automata,  

1681: \emph{Theoretical Computer Science} \textbf{126}: 183--235

1682: (1994).}

1683: 

1684: \bibitem{afh96}{R.~Alur, T.~Feder, T.~A.~Henzinger:

1685: The benefits of relaxing punctuality,

1686: \emph{J. ACM} \textbf{43}, 116--146 (1996).}

1687: 

1688: \bibitem{afh94}{R.~Alur, L.~Fix, T.~A.~Henzinger: 

1689: Event-clock automata: a determinizable class of timed

1690: automata, {\em Proc. 6th International Conference on 

1691: Computer-aided Verification,}

1692: LNCS~\textbf{818}, 1--13, Springer-Verlag (1994).}

1693: 

1694: \bibitem{ah93}{R.~Alur, T.~A.~Henzinger: 

1695: Real-time logics: complexity and expressiveness,

1696: \emph{Information and Computation} \textbf{104}, 35--77 (1993).}

1697: 

1698: \bibitem{b60}{J.~R.~B\"uchi: Weak second-order

1699: arithmetic and finite automata, \emph{Zeitschrift f\"ur

1700: Math. Logik und Grundlagen der Mathematik}, \textbf{6}, 66--92 (1960).}

1701: 

1702: \bibitem{d03} {D.~D'Souza: 

1703: A Logical Characterisation of Event Clock Automata, in

1704: \emph{J. Foundations of Computer Science},

1705: \textbf{14}, No. 4,  World

1706: Scientific (2003).}

1707: 

1708: %% \bibitem{d00} {D.~D'Souza:

1709: %% A Logical Characterisation of Event Recording Automata, in

1710: %% \emph{Proc. International Symposium on Formal Methods in

1711: %% Real-Time and Fault Tolerance (FTRTFT)} 2000, LNCS \textbf{1926} (2000).}

1712: 

1713: \bibitem{dt99}{D. D'Souza, P.~S.~Thiagarajan: Product

1714: Interval Automata: A Subclass of Timed Automata,

1715: \emph{Proc. 19th Foundations of Software Technology and Theoretical

1716: Computer Science (FSTTCS)}, LNCS \textbf{1732} (1999).}

1717: 

1718: \bibitem{gpss80}{

1719: D.~Gabbay, A.~Pnueli, S.~Shelah, J.~Stavi:

1720: The Temporal Analysis of Fairness,

1721: \emph{Seventh ACM Symposium on Principles of

1722: Programming Languages,} 163--173 (1980).}

1723: 

1724: \bibitem{hrs98} {T.~A.~Henzinger, J.-F.~Raskin, and

1725: P.-Y.~Schobbens: The regular real-time languages,

1726: {\em Proc. 25th International Colloquium

1727: on Automata, Languages, and Programming 1998}, 

1728: LNCS~\textbf{1443}, 580--591 (1998).}

1729: 

1730: \bibitem{k68}{H.~Kamp: Tense Logic and the Theory of

1731: Linear Order, PhD Thesis, University of California (1968).}

1732: 

1733: \bibitem{k90}{R.~Koymans: Specifying real-time properties with

1734:   metric temporal logic, \emph{Real-time Systems}, \textbf{2}(4),

1735:   255--299 (1990).}

1736:  

1737: \bibitem{p77} {A.~Pnueli: The temporal logic of programs,

1738: \emph{Proc. 18th IEEE Symposium on Foundation of Computer

1739:   Science}, 46--57 (1977).}

1740: 

1741: \bibitem{r99} {J.~-F.~Raskin: Logics, Automata and

1742: Classical Theories for Deciding Real Time, Ph.D Thesis,

1743: FUNDP, Belgium (1999).}

1744: 

1745: \bibitem{rs97} {J.~-F.~Raskin, P.~-Y.~Schobbens:

1746: State-clock Logic: A Decidable Real-Time Logic, {\em

1747: Proc. HART '97: Hybrid and Real-Time Systems}, LNCS~\textbf{1201},

1748: 33--47 (1997).}

1749: 

1750: \bibitem{t90}

1751: {W.~Thomas: Automata on Infinite Objects, 

1752: in J.~V.~Leeuwen (Ed.), {\em Handbook of Theoretical

1753: Computer Science}, Vol. B, 133--191, 

1754: Elsevier (1990).}

1755: 

1756: \bibitem{w94} Th. Wilke:

1757: {Specifying Timed State Sequences in Powerful Decidable

1758: Logics and Timed Automata, in {\em Proc. Formal Techniques in

1759: Real-Time and Fault-Tolerant Systems}, LNCS~\textbf{863},

1760: 694--715 (1994).}

1761: 

1762: %% \bibitem{w99} Th. Wilke:

1763: %% {Classifying Discrete Temporal Properties, in

1764: %%   \emph{Proc. Sym. Theoretical Aspects of Computer Science (STACS)

1765: %%     1999}, LNCS~\textbf{1563}, 32--46 (1999).}

1766: 

1767: 

1768: \end{thebibliography}

1769: 

1770: \end{document}

1771: 

1772: