1: \documentclass{tlp}

2: \usepackage{amssymb}

3: \usepackage{latexsym}

4: \usepackage{verbatim}

5: \usepackage{color}

6: \usepackage[dvips]{graphicx}

7: \input{macros}

8: \input epsf

9: 

10: \submitted{18 March 2002}

11: 

12: \revised{14 January 2003}

13: 

14: \accepted{5 September 2003}

15: 

16: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

17: %%% Document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

18: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

19: \title[Temporalized logics and automata for time granularity]{Temporalized logics and automata

20: \\ for time granularity}

21: 

22: \author[Massimo Franceschet and Angelo Montanari]{MASSIMO FRANCESCHET\\

23:           Department of Sciences, University of Chieti-Pescara,

24:           Italy \\

25:           \email{francesc@sci.unich.it}

26:           \and ANGELO MONTANARI\\

27:           Department of Mathematics and Computer Science, University of Udine,

28:           Italy \\

29:           \email{montana@dimi.uniud.it}}

30: 

31: \date{}

32: 

33: \begin{document}

34: 

35: \DeclareGraphicsExtensions{.pstex} %Estensioni dei file grafici postscript

36: 

37: \maketitle

38: \begin{abstract}

39: The ability of providing and relating temporal representations at

40: different `grain levels' of the same reality is an important

41: research theme in computer science and a major requirement for

42: many applications, including formal specification and

43: verification, temporal databases, data mining, problem solving,

44: and natural language understanding. In particular, the addition of

45: a granularity dimension to a temporal logic makes it possible to

46: specify in a concise way reactive systems whose behaviour can be

47: naturally modeled with respect to a (possibly infinite) set of

48: differently-grained temporal domains.

49: 

50: Suitable extensions of the monadic second-order theory of $k$

51: successors have been proposed in the literature to capture the

52: notion of time granularity. In this paper, we provide the monadic

53: second-order theories of downward unbounded layered structures,

54: which are infinitely refinable structures consisting of a coarsest

55: domain and an infinite number of finer and finer domains, and of

56: upward unbounded layered structures, which consist of a finest

57: domain and an infinite number of coarser and coarser domains, with

58: expressively complete and elementarily decidable temporal logic

59: counterparts.

60: 

61: We obtain such a result in two steps. First, we define a new class

62: of combined automata, called temporalized automata, which can be

63: proved to be the automata-theoretic counterpart of temporalized

64: logics, and show that relevant properties, such as closure under

65: Boolean operations, decidability, and expressive equivalence with

66: respect to temporal logics, transfer from component automata to

67: temporalized ones. Then, we exploit the correspondence between

68: temporalized logics and automata to reduce the task of finding the

69: temporal logic counterparts of the given theories of time

70: granularity to the easier one of finding temporalized automata

71: counterparts of them.

72: \end{abstract}

73: 

74: \section{Introduction}

75: \label{sec:int}

76: 

77: Time granularity is an important, but not always well-understood,

78: research theme in computer science. To acquaint the reader with

79: the basics of the subject, we start the paper with a gentle

80: introduction to research on time granularity. In

81: Section~\ref{sec:granularity}, we briefly illustrate the

82: intersection of research on time granularity with different areas

83: of computer science, ranging from system specification and

84: verification to natural language understanding, and we give a

85: high-level view of the logical approach to the problem of

86: representing and reasoning about time granularity that we follow

87: in the paper. In Section~\ref{sec:contr}, we focus on the topics

88: addressed in the paper, and we outline its main contributions. In

89: Section~\ref{sec:reliss}, we show that the considered topics

90: present interesting connections with a number of issues relevant

91: to various research directions in computer science logic,

92: including real-time logics, interval logics, and combined logics.

93: We conclude the introduction by a short description of the

94: organization of the rest of the paper.

95: 

96: \subsection{Representing and reasoning about time granularity}

97: \label{sec:granularity}

98: 

99: %Time granularity and its links

100: 

101: The ability of providing and relating temporal representations at

102: different `grain levels' of the same reality is an important

103: research theme in various fields of computer science, including

104: formal specification and verification, temporal databases, data

105: mining, problem solving, and natural language understanding. As

106: for {\em formal specifications\/}, there exists a large class of

107: reactive systems whose components have dynamic behavior regulated

108: by very different time constants (granular reactive systems). A

109: good specification language must enable one to specify and verify

110: the components of a granular reactive system and their

111: interactions in a simple and intuitively clear

112: way~\cite{CCMSP93,CCMMMPR91,CMR91b,FiMa94,Lam85,MPP02,MPP99,MPP00,MP96}.

113: As for {\em temporal databases\/}, the common way to represent

114: temporal information is to timestamp either attributes

115: (\emph{attribute timestamping}) or tuples/objects

116: (\emph{tuple-timestamping}). Timestamping is performed taking time

117: values over some fixed granularity. However, it may happen that

118: differently-grained timestamps are associated with different data.

119: This is the case, for instance, when information is collected from

120: distinct sources which are not under the same control. Moreover,

121: users and application programs may require the flexibility of

122: viewing and querying temporal data at different time

123: granularities.  To guarantee consistency either the data must be

124: converted into a uniform granularity-independent representation or

125: temporal database operations must be generalized to cope with data

126: associated with different temporal domains.  In both cases, a

127: precise semantics for time granularity is

128: needed~\cite{BBJW97,CSS93,CP01,DS95,JLW93,JSW95,MP93,NJW02,NS93,SC93,Wi98,W99}.

129: With regard to {\em data mining}, a huge amount of data is

130: collected every day in the form of event-time sequences. These

131: sequences represent valuable sources of information, not only for

132: what is explicitly recorded, but also for deriving implicit

133: information and predicting the future behavior of the monitored

134: process. This latter activity requires an analysis of the

135: frequency of certain events, the discovery of their regularity,

136: and the identification of sets of events that are linked by

137: particular temporal relationships. Such frequencies, regularity,

138: and relationships are often expressed in terms of multiple

139: granularities, and thus analysis and discovery tools must be able

140: to cope with them~\cite{AS95,BJLW98,BJW96b,DDS94,MTV95}. With

141: regard to {\em problem solving\/}, several problems in scheduling,

142: planning, and diagnosis can be formulated as temporal constraint

143: satisfaction problems provided with a time granularity dimension.

144: Variables are used to represent events occurring at different time

145: granularities and constraints are used to represent temporal

146: relations between events

147: ~\cite{BWJ96a,CD98,E95,L87,MMCR92,MR96,PB91,S96}. Finally, shifts

148: in the temporal perspective are common in natural language

149: communication, and thus the ability of supporting and relating a

150: variety of temporal models, at different grain sizes, is a

151: relevant feature for the task of {\em natural language

152: processing\/}~\cite{BB03,FLM86,FGMT89,KS01}.

153: 

154: %The logical approach

155: 

156: \medskip

157: 

158: According to a commonly accepted perspective, any time granularity

159: can be viewed as the partitioning of a temporal domain in groups

160: of elements, where each group is perceived as an indivisible unit

161: (a granule). A representation formalism can then use these

162: granules to provide facts, actions or events with a temporal

163: qualification, at the appropriate abstraction level. However,

164: adding the concept of time granularity to a formalism does not

165: merely mean that one can use different temporal units to represent

166: temporal quantities in a unique flat model, but it involves

167: semantic issues related to the problem of assigning a proper

168: meaning to the association of statements with the different

169: temporal domains of a layered model and of switching from one

170: domain to a coarser/finer one.

171: 

172: 

173: \begin{figure}

174: \centering

175: \input{nls.pstex_t} % Importa un file LaTeX, che a sua volta importa il postscript (.pstex)

176: \caption{\label{fig:fin} The $2$-refinable 4-layered structure.}

177: \end{figure}

178: 

179: Different approaches to represent and to reason about time

180: granularity have been proposed in the literature. In the

181: following, we introduce the distinctive features of the logical

182: approach to time granularity\footnote{In \cite{FM02b} we analyze

183: alternative approaches to time granularity, developed in the

184: context of temporal databases, and we compare them with the

185: logical one.}. In the {\em logical} setting, the different time

186: granularities and their interconnections are represented by means

187: of mathematical structures, called layered structures. A {\em

188: layered structure} consists of a possibly infinite set of related

189: differently-grained temporal domains. Such a structure identifies

190: the relevant temporal domains and defines the relations between

191: time points belonging to different domains. Suitable operators

192: make it possible to move horizontally {\em within} a given

193: temporal domain (displacement operators), and to move vertically

194: {\em across} temporal domains (projection operators). Both

195: classical and temporal logics can be interpreted over the layered

196: structure. Logical formulas allow one to specify properties

197: involving different time granularities in a single formula by

198: mixing displacement and projection operators. Algorithms are

199: provided to verify whether a given formula is consistent

200: (\emph{satisfiability checking}) as well as to check whether a

201: given formula is satisfied in a particular structure (\emph{model

202: checking}). The logical approach to represent time granularity has

203: been mostly applied in the field of formal specification and

204: verification of concurrent systems. An application of time

205: granularity logics to the specification of a supervisor that

206: automates the activities of a high voltage station, devoted to the

207: end user distribution of the energy generated by power plants, has

208: been accomplished in collaboration with Automation Research Center

209: of the Electricity Board of Italy (ENEL). A short account of this

210: work has been given in \cite{CCMSP93}. Logics for time granularity

211: have also been applied to the specification of real-time

212: monitoring systems \cite{CCMMMPR91}, mobile systems

213: \cite{FMdeR00}, and therapy plans in clinical medicine

214: \cite{CFP02}.

215: 

216: \begin{figure}

217: \centering

218: \input{duls.pstex_t} % Importa un file LaTeX, che a sua volta importa il postscript (.pstex)

219: \caption{\label{fig:down} The $2$-refinable downward unbounded

220: layered structure.}

221: \end{figure}

222: 

223: A systematic logical framework for time granularity, based on a

224: many-level view of temporal structures, with matching logics and

225: decidability results, has been proposed in~\cite{M96,MP96,MPP99}

226: and later extended in~\cite{F01,FM01b,FM01a,FM03}. Layered

227: structures with exactly $n \geq 1$ temporal domains such that each

228: time point can be refined into $k \geq 2$ time points of the

229: immediately finer temporal domain, if any, are called

230: $k$-refinable $n$-layered structures ($n$-LSs for short, see

231: Figure~\ref{fig:fin}). They have been investigated in~\cite{MP96},

232: where a classical second-order language, with second-order

233: quantification restricted to monadic predicates, has been

234: interpreted over them. The language includes a total order $<$ and

235: $k$ projection functions ${\downarrow}_0, \ldots,

236: {\downarrow}_{k-1}$ over the layered temporal universe such that,

237: for every point $x$, ${\downarrow}_0(x), \ldots, {\downarrow}_{k -

238: 1}(x)$ are the $k$ elements of the immediately finer temporal

239: domain, if any, into which $x$ is refined. The satisfiability

240: problem for the monadic second-order language over $n$-LSs has

241: been proved to be decidable by using a reduction to the emptiness

242: problem for B\"uchi sequence automata. Unfortunately, the decision

243: procedure has a nonelementary complexity.

244: 

245: Layered structures with an infinite number of temporal domains,

246: $\omega$-layered structures, have been studied in~\cite{MPP99}. In

247: particular, the authors investigated {\em $k$-refinable downward

248: unbounded layered structures} (DULSs), that is, $\omega$-layered

249: structures consisting of a coarsest domain together with an

250: infinite number of finer and finer domains (see

251: Figure~\ref{fig:down}), and {\em $k$-refinable upward unbounded

252: layered structures} (UULSs), that is, $\omega$-layered structures

253: consisting of a finest temporal domain together with an infinite

254: number of coarser and coarser domains (see Figure~\ref{fig:up}). A

255: classical monadic second-order language, including a total order

256: $<$ and $k$ projection functions ${\downarrow}_0, \ldots,

257: {\downarrow}_{k-1}$, has been interpreted over both UULSs and

258: DULSs. The decidability of the monadic second-order theories of

259: UULSs and DULSs has been proved by reducing the satisfiability

260: problem to the emptiness problem for systolic and Rabin tree

261: automata, respectively. In both cases the decision procedure has a

262: nonelementary complexity.

263: 

264: \begin{figure}

265: \centering

266: \input{uuls.pstex_t} % Importa un file LaTeX, che a sua volta importa il postscript (.pstex)

267: \caption{\label{fig:up} The $2$-refinable upward unbounded layered

268: structure.}

269: \end{figure}

270: 

271: \subsection{Our contributions}

272: \label{sec:contr}

273: 

274: Monadic logics for time granularity are quite expressive, but,

275: unfortunately, they have few computational appealing: their

276: decision problem is indeed \emph{nonelementary}. This roughly

277: means that it is possible to algorithmically check satisfiability,

278: but the complexity of the algorithm grows very rapidly and cannot

279: be bounded. Moreover, the corresponding automata (B\"uchi sequence

280: automata for the theory of finitely-layered structures, Rabin tree

281: automata for downward unbounded structures, and systolic tree

282: automata for upward unbounded ones) do not directly work over

283: layered structures, but rather over collapsed structures into

284: which layered structures can be encoded. Hence, they are not

285: natural and intuitive tools to specify and check properties of

286: time granularity.

287: 

288: In this paper, we follow a different approach. Taking inspiration

289: from combination methods for temporal logics, we start by studying

290: how to combine automata in such a way that properties of the

291: components are inherited by the combination. Then, we reinterpret

292: layered structures as \emph{combined structures}. This intuition

293: reveals to be the keystone of our endeavor. Indeed, it allows us

294: to define combined temporal logics and combined automata over

295: layered structures, and to study their expressive power and

296: computational properties by taking advantage of the transfer

297: theorems for combined logics and combined automata. The outcome is

298: appealing: the resulting combined temporal logics and automata

299: directly work over layered structures. Moreover, they are

300: expressively equivalent to monadic languages, and they are

301: elementarily decidable.

302: 

303: \begin{figure}[t]

304: \begin{center}

305: \begin{picture}(150,150)

306: \put(-35,90){{\bf Monadic}} \put(-35,80){{\bf Theories}}

307: \put(100,90){{\bf (Temporalized)}} \put(120,80){{\bf Logics}}

308: \put(15,16){{\bf (Temporalized)}} \put(25,6){{\bf Automata}}

309: \put(15,85){\vector(1,0){80}} \put(95,85){\vector(-1,0){80}}

310: \put(5,75){\vector(1,-1){45}} \put(5,75){\vector(-1,1){1}}

311: \put(100,75){\vector(-1,-1){45}} \put(100,75){\vector(1,1){1}}

312: \put(55,95){?}

313: \end{picture}

314: \caption{\label{fig:dia} From monadic theories to (temporalized)

315: logics via (temporalized) automata.}

316: \end{center}

317: \end{figure}

318: 

319: Finding the temporal logic counterpart of monadic theories is a

320: difficult task, involving a nonelementary blow up in the length of

321: formulas. Ehrenfeucht games have been successfully exploited to

322: deal with such a correspondence problem for first-order monadic

323: theories~\cite{IK89} and well-behaved fragments of second-order

324: ones, e.g. the path fragment of the monadic second-order theory of

325: infinite binary trees~\cite{HT87}. As for the theories of time

326: granularity, by means of suitable applications of Ehrenfeucht

327: games, we obtained an expressively complete and elementarily

328: decidable combined temporal logic counterpart of the path fragment

329: of the monadic second-order theory of DULSs~\cite{FM03}, while

330: Montanari et al. extended Kamp's theorem to deal with the

331: first-order fragment of the theory of UULSs~\cite{MPP02}.

332: Unfortunately, these techniques produce rather involved proofs and

333: do not naturally lift to the full second-order case.

334: 

335: In this paper, instead of trying to establish a direct

336: correspondence between monadic second-order theories for time

337: granularity and temporal logics, we connect them via automata

338: (cf.\ Figure~\ref{fig:dia}). Firstly, we define a new class of

339: combined automata, called temporalized automata, which can be

340: proved to be the automata-theoretic counterpart of temporalized

341: logics, and show that relevant properties, such as closure under

342: Boolean operations, decidability, and expressive equivalence with

343: respect to temporal logics, transfer from component automata to

344: temporalized ones. Then, on the basis of the established

345: correspondence between temporalized logics and automata, we reduce

346: the task of finding a temporal logic counterpart of the monadic

347: second-order theories of DULSs and UULSs to the easier one of

348: finding a temporalized automata counterpart of them. The mapping

349: of monadic formulas into automata (the difficult direction) can

350: indeed greatly benefit from automata closure properties.

351: 

352: As a by-product, the alternative characterization of temporalized

353: logics for time granularity as temporalized automata allows one to

354: reduce logical problems to automata ones. As it is well-known in

355: the area of automated system specification and verification, such

356: a reduction presents several advantages, including the possibility

357: of using automata for both system modeling and specification, and

358: the possibility of checking the system on-the-fly (a detailed

359: account of these advantages can be found in~\cite{FM01a}).

360: 

361: \subsection{Related fields}

362: \label{sec:reliss}

363: 

364: The original motivation of our research was the design of a

365: temporal logic embedding the notion of time granularity, suitable

366: for the specification of complex concurrent systems whose

367: components evolve according to different time units. However, we

368: soon established a fruitful complementary point of view on time

369: granularity: it can be regarded as a powerful setting to

370: investigate the definability of meaningful timing properties over

371: a \emph{single} time domain. Moreover, layered structures and

372: logics provide an interesting embedding framework for flat

373: \emph{real-time} structures and logics, as well as there exists a

374: natural link between structures and theories of time granularity

375: and those developed for representing and reasoning about

376: \emph{time intervals}. Finally, there are significant similarities

377: between the problems we encountered in studying time granularity,

378: and those addressed by current research on \emph{combining}

379: logics, theories, and structures. In the following, we briefly

380: explain all these connections.

381: 

382: \paragraph{Granular reactive systems.}

383: As pointed out above, we were originally motivated by the design

384: of a temporal logic embedding the notion of time granularity

385: suitable for the specification of granular reactive systems. A

386: {\em reactive system} is a concurrent program that maintains and

387: interaction with the external environment and that ideally runs

388: forever. Temporal logic has been successfully used for modeling

389: and analyzing the behavior of reactive systems \cite{E90}. It

390: supports semantic model checking, which can be used to check

391: specifications against system behaviors; it also supports pure

392: syntactic deduction, which may be used to verify the consistency

393: of specifications. Finite-state automata, such as B\"uchi sequence

394: automata and Rabin tree automata \cite{T90}, have been proved very

395: useful in order to provide clean and asymptotically optimal

396: satisfiability and model checking algorithms for temporal

397: logics~\cite{KVW00,VW94} as well as to cope with the {\em state

398: explosion problem} that frightens concurrent system

399: verification~\cite{CVWY91,JJ89,VW86}.

400: %Moreover, automata themselves can be directly used as a

401: %specification formalism, provided with a natural graphical

402: %interpretation~\cite{MP87}.

403: 

404: A {\em granular reactive systems} is a reactive system whose

405: components have dynamic behaviours regulated by very different

406: time constants~\cite{M96}. As an example, consider a pondage power

407: station consisting of a reservoir, with filling and emptying times

408: of days or weeks, generator units, possibly changing state in a

409: few seconds, and electronic control devices, evolving in

410: microseconds or even less. A complete specification of the power

411: station must include the description of these components and of

412: their interactions. A natural description of the temporal

413: evolution of the reservoir state will probably use days: ``During

414: rainy weeks, the level of the reservoir increases 1 meter a day'',

415: while the description of the control devices behaviour may use

416: microseconds: ``When an alarm comes from the level sensors, send

417: an acknowledge signal in 50 microseconds''. We say that systems of

418: such a type have {\em different time granularities}. It is

419: somewhat unnatural, and sometimes impossible, to compel the

420: specifier to use a unique time granularity, microseconds in the

421: previous example, to describe the behaviour of all the components.

422: A good language must indeed allow the specifier to easily describe

423: all simple and intuitively clear facts (naturalness of the

424: notation). Hence, a specification language for granular reactive

425: systems must support different time granularities to allow one (i)

426: to maintain the specifications of the dynamics of

427: differently-grained components as separate as possible (modular

428: specifications), (ii) to differentiate the refinement degree of

429: the specifications of different system components (flexible

430: specifications), and (iii) to write complex specifications in an

431: incremental way by refining higher-level predicates associated

432: with a given time granularity in terms of more detailed ones at a

433: finer granularity (incremental specifications).

434: 

435: \paragraph{Definability of meaningful timing properties.}

436: Time granularity can be viewed not only as an important feature of

437: a representation language, but also as a formal tool to

438: investigate the definability of meaningful timing properties, such

439: as density and exponential grow/decay, over a {\em single} time

440: domain~\cite{MPP99}. In this respect, the number of layers (single

441: vs.\ multiple, finite vs.\ infinite) of the underlying temporal

442: structure, as well as the nature of their interconnections, play a

443: major role: certain timing properties can be expressed using a

444: single layer; others using a finite number of layers; others only

445: exploiting an infinite number of layers. For instance, temporal

446: logics over binary $2$-layered structures suffice to deal with

447: conditions like ``$P$ holds at all even times of a given temporal

448: domain'' that cannot be expressed using flat propositional

449: temporal logics~\cite{W83}. Moreover, temporal logics over

450: $\omega$-layered structures allow one to express relevant

451: properties of infinite sequences of states over a single temporal

452: domain that cannot be captured by using flat or $n$-layered

453: temporal logics. For instance, temporal logics over $k$-refinable

454: UULSs allow one to express conditions like ``$P$ holds at all time

455: points $k^i$, for all natural numbers $i$, of a given temporal

456: domain'', which cannot be expressed by using  either propositional

457: or quantified temporal logics over a finite number of layers,

458: while temporal logics over DULSs allow one to constrain a given

459: property to hold true `densely' over a given time interval.

460: 

461: \paragraph{On the relationship with real-time logics.}

462: Layered structures and logics can be regarded as an embedding

463: framework for flat real-time structures and logics. A {\em

464: real-time system} is a reactive system with well-defined

465: fixed-time constraints. Systems that control scientific

466: experiments, industrial control systems, automobile-engine

467: fuel-injection systems, and weapon systems are examples of

468: real-time systems. Examples of quantitative timing properties

469: relevant to real-time systems are periodicity, bounded

470: responsiveness, and timing delays. Logics for real-time systems,

471: called real-time logics, are interpreted over {\em timed state

472: sequences}, that is, state sequences in which every state is

473: associated with a time instant.

474: 

475: Montanari et al.\ showed that the second-order theory of timed

476: state sequences can be {\em properly} embedded into the

477: second-order theory of binary UULSs as well as into the

478: second-order theory of binary DULSs~\cite{MPP00}. The increase in

479: expressive power of the embedding frameworks makes it possible to

480: express and check additional timing properties of real-time

481: systems, which cannot be dealt with by the classical theory. For

482: instance, in the theory of timed state sequences, saying that a

483: state $s$ holds true at time $i$ can be meant to be an abstraction

484: of the fact that state $s$ can be arbitrarily placed in the time

485: interval $[i,i+1)$.  The stratification of domains in layered

486: structures naturally supports such an interval interpretation and

487: gives means for reducing the uncertainty involved in the

488: abstraction process. For instance, it allows on to say that a

489: state $s$ belongs to the first (respectively, second) half of the

490: time interval $[i,i+1)$. More generally, the embedding of

491: real-time logics into the granularity framework allows one to deal

492: with {\em temporal indistinguishability} of states (two or more

493: states associated with the same time) and {\em temporal gaps}

494: between states (a nonempty time interval between the time

495: associated to two contiguous states). Temporal

496: indistinguishability and temporal gaps can indeed be interpreted

497: as phenomena due to the fact that real-time logics lack the

498: ability to express properties at the right (finer) level of

499: granularity: distinct states, associated with the same time, can

500: always be ordered at the right level of granularity; similarly,

501: time gaps represent intervals in which a state cannot be specified

502: at a finer level of granularity. A finite number of layers is

503: obviously not sufficient to capture timed state sequences: it is

504: not possible to fix a priori any bound on the granularity that a

505: domain must have to allow one to temporally order a given set of

506: states, and thus we need to have an infinite number of temporal

507: domains at our disposal.

508: 

509: \paragraph{On the relationship with interval logics.}

510: As pointed out in~\cite{M96}, there exists a natural link between

511: structures and theories of time granularity and those developed

512: for representing and reasoning about time intervals.

513: Differently-grained temporal domains can indeed be interpreted as

514: different ways of partitioning a given discrete/dense time axis

515: into consecutive disjoint intervals. According to this

516: interpretation, every time point can be viewed as a suitable

517: interval over the time axis and projection implements an

518: intervals-subintervals mapping. More precisely, let us define {\em

519: direct constituents} of a time point $x$, belonging to a given

520: domain, the time points of the immediately finer domain into which

521: $x$ can be refined, if any, and {\em indirect constituents} the

522: time points into which the direct constituents of $x$ can be

523: directly or indirectly refined, if any. The mapping of a given

524: time point into its direct or indirect constituents can be viewed

525: as a mapping of a given time interval into (a specific subset of)

526: its subintervals.

527: 

528: The existence of such a natural correspondence between interval

529: and granularity structures hints at the possibility of defining a

530: similar connection at the level of the corresponding theories. For

531: instance, according to such a connection, temporal logics over

532: DULSs allow one to constrain a given property to hold true densely

533: over a given time interval, where $P$ densely holds over a time

534: interval $w$ if $P$ holds over $w$ and there exists a direct

535: constituent of $w$ over which $P$ densely holds. In particular,

536: establishing a connection between structures and logics for time

537: granularity and those for time intervals would allow one to

538: transfer decidability results from the granularity setting to the

539: interval one. As a matter of fact, most interval temporal logics,

540: including Moszkowski's Interval Temporal Logic (ITL)~\cite{M83},

541: Halpern and Shoham's Modal Logic of Time Intervals

542: (HS)~\cite{HS91}, Venema's CDT Logic~\cite{V91}, and Chaochen and

543: Hansen's Neighborhood Logic (NL)~\cite{CH98}, are highly

544: undecidable. Decidable fragments of these logics have been

545: obtained by imposing severe restrictions on their expressive

546: power, e.g., the {\em locality} constraint in \cite{M83}.

547: 

548: Preliminary results can be found in~\cite{MSV02}, where the

549: authors propose a new interval temporal logic, called Split Logic

550: (SL for short), which is equipped with operators borrowed from HS

551: and CDT, but is interpreted over specific interval structures,

552: called {\em split-frames\/}. The distinctive feature of a

553: split-frame is that there is at most one way to chop an interval

554: into two adjacent subintervals, and consequently it does not

555: possess {\em all} the intervals. They prove the decidability of SL

556: with respect to particular classes of split-frames which can be

557: put in correspondence with the first-order fragments of the

558: monadic theories of time granularity. In particular, {\em

559: discrete} split-frames with maximal intervals correspond to

560: finitely layered structures, discrete split-frames (with unbounded

561: intervals) can be mapped into upward unbounded layered structures,

562: and {\em dense} split-frames with maximal intervals can be encoded

563: into downward unbounded layered structures.

564: 

565: \paragraph{The combining logic perspective.}

566: There are significant similarities between the problems we

567: addressed in the time granularity setting and those dealt with by

568: current research on logics that model changing contexts and

569: perspectives. The design of these types of logics is emerging as a

570: relevant research topic in the broader area of combination of

571: logics, theories, and structures, at the intersection of logic

572: with artificial intelligence, computer science, and computational

573: linguistics~\cite{GdR00}. The reason is that application domains

574: often require rather complex hybrid description and specification

575: languages, while theoretical results and implementable algorithms

576: are at hand only for simple basic components~\cite{GKWZ03}. As for

577: granular reactive systems, their operational behavior can be

578: naturally described as a suitable combination of temporal {\em

579: evolutions} (sequences of component states) and temporal {\em

580: refinements} (mapping of a component state into a finite sequence

581: of states belonging to a finer component). According to such a

582: point of view, the model describing the operational behavior of

583: the system and the specification language can be obtained by {\em

584: combining} simpler models and languages, respectively, and model

585: checking/satisfiability procedures for combined logics can be

586: used.

587: 

588: \bigskip \noindent

589: From the above discussion, it turns out that the time granularity

590: framework is expressive and flexible enough to be used to

591: investigate many interesting topics not explicitly related to time

592: granularity. The aim of this paper is to deepen our understanding

593: of time granularity. The rest of the paper is organized as

594: follows. In Section \ref{sec:tempaut}, we introduce temporalized

595: automata and we show that relevant logical properties, such as

596: closure under Boolean operations and decidability, transfer from

597: component automata to temporalized ones; furthermore, we prove

598: that temporalized automata are as expressive as temporalized

599: logics. In Section \ref{sec:timegran} we exploit temporalized

600: automata to find the temporal logic counterparts of the given

601: theories of time granularity. Temporalized automata for the

602: theories of DULSs and UULSs are obtained as combinations of

603: B\"uchi and Rabin automata and of B\"uchi and finite tree

604: automata, respectively. As a matter of fact, unlike the case of

605: DULSs, the combined model we use to encode an UULS differs from

606: that of pure temporalization since the innermost submodels are not

607: independent from the outermost top-level model. In Section

608: \ref{sec:exa}, we apply temporalized logics to a real-world case

609: study. Conclusive remarks provide an assessment of the work done

610: and outline some future research directions.

611: 

612: \section{Temporalized logics and automata}

613: \label{sec:tempaut}

614: 

615: In this section we recall the definition of temporalization and we

616: define temporalized automata\footnote{We assume the reader to be

617: familiar with basic concepts of modal and temporal logics, and

618: automata. If this is not the case, comprehensive surveys are given

619: in~\cite{E90} and~\cite{T90}, respectively.}. Moreover, we prove

620: the equivalence of temporalized automata and temporalized logics.

621: We will take into consideration the following well-known temporal

622: logics: {\em Propositional Linear Temporal Logic} ($\pltl$), {\em

623: Quantified Linear Temporal Logic} ($\qltl$), {\em Existentially

624: Quantified Linear Temporal Logic} ($\eqltl$), {\em Directed

625: Computational Tree Logic} ($\dctls$), {\em Quantified Directed

626: Computational Tree Logic} ($\qdctls$), and {\em Existentially

627: Quantified Directed Computational Tree Logic} ($\eqdctls$);

628: moreover, we will take advantage of the following well-known

629: finite-state automata classes: B\"uchi sequence automata, Rabin

630: tree automata, finite tree automata.

631: 

632: Let ${\cal P} = \{P,Q, \ldots\}$ be a set of proposition letters.

633: We consider {\em temporal logics} over the set of propositional

634: letters ${\cal P}$. Given a temporal logic $\logic{T}$, we use

635: ${\cal L}_{\logic{T}}$ and $\mathsf{K}_{\logic{T}}$ to denote the

636: language and the set of models of $\logic{T}$, respectively.

637: Furthermore, we write $\mathit{OP}(\logic{T})$ to denote the set

638: of temporal operators of $\logic{T}$.

639: 

640: {\em Temporalization} is a simple form of logic combination that

641: embeds one component logic into the other~\cite{FG92}. Let

642: $\logic{T}$ be a temporal logic and $\logic{L}$ an arbitrary

643: logic. For the sake of simplicity, we constrain $\logic{L}$ to be

644: an extension of propositional logic. We partition the set of

645: $\logic{L}$-formulas into {\em Boolean combinations}

646: $\mathit{BC}_{\logic{L}}$ and {\em monolithic formulas}

647: $\mathit{ML}_{\logic{L}}$: $\alpha$ belongs to

648: $\mathit{BC}_{\logic{L}}$ if its outermost operator is a Boolean

649: connective; otherwise it belongs to $\mathit{ML}_{\logic{L}}$.  We

650: assume that $\OP(\logic{T}) \cap \OP(\logic{L}) = \emptyset$.

651: 

652: \begin{definition} \thC{Temporalization -- Syntax}

653: \label{def:colog1} \noindent The language ${\cal L}_{\tl{T}{L}}$

654: of the \emph{temporalization} $\tl{T}{L}$ of $\logic{L}$ by means

655: of $\logic{T}$ over the set of proposition letters $\cal P$ is

656: obtained by taking the set of formation rules of ${\cal

657: L}_{\logic{T}}$ and by replacing the atomic formation rule:

658: ``every proposition letter $P \in {\cal P}$ is a formula'' by the

659: rule: ``every monolithic formula $\alpha \in

660: \mathcal{L}_{\logic{L}}$ is a formula''. \dqed

661: \end{definition}

662: 

663: \noindent As an example, let $\logic{T_1}$ and $\logic{T_2}$ be

664: two temporal logics, and let $\{\op{F_1}, \op{G_1}\}$ (resp.

665: $\{\op{F_2}, \op{G_2}\}$) be the temporal operators of

666: $\logic{T_1}$ (resp. $\logic{T_2}$). The formula ${\bf F_1 G_2} p$

667: is a $\tl{T_1}{T_2}$-formula, while the formula ${\bf F_1 G_2} p

668: \IImp {\bf G_2 F_1} p$ is not.

669: 

670: \medskip

671: 

672: A {\em model} for $\tl{T}{L}$ is a triple $(W,{\cal R},g)$, where

673: $(W,{\cal R})$ is a frame for $\logic{T}$ and $g \, : \, W \Imp

674: \mathsf{K}_{\logic{L}}$ a total function mapping worlds in $W$ to

675: models for $\logic{L}$.

676: 

677: \begin{definition} \thC{Temporalization -- Semantics}

678: \label{def:cosem1} \noindent Given a model ${\cal M} = (W,{\cal

679: R},g)$ and a state $w \in W$, the semantics of the temporalized

680: logic $\tl{T}{L}$ is obtained by taking the set of semantic

681: clauses of $\logic{T}$ and by replacing the clause for proposition

682: letters: ``${\cal M}, w \models P$ if and only if $P \in V(w)$,

683: whenever $P \in {\cal P}$'' by the clause: ``${\cal M}, w \models

684: \alpha$ if and only if $g(w) \models_{\logic{L}} \alpha$, whenever

685: $\alpha \in ML_{\logic{L}}$''. \dqed

686: \end{definition}

687: 

688: Hereafter, we will restrict our attention to temporalized logics

689: such that both the embedding and the embedded logics are temporal

690: logics.

691: 

692: \medskip

693: 

694: We now introduce a new class of combined automata, called

695: \emph{temporalized automata}, which can be viewed as the

696: automata-theoretic counterpart of temporalized logics, and show

697: that relevant properties, such as closure under Boolean

698: operations, decidability, and expressive equivalence with respect

699: to temporal logics, transfer from component automata to

700: temporalized ones. We first define automata and prove results over

701: sequence structures; then, we generalize definitions and results

702: to tree structures (as a matter of fact, we believe that our

703: machinery can actually be extended to cope with more general

704: structures, such as graphs). We will use the following general

705: definition of sequence automata. Let $\Sigma = \{a,b,\ldots\}$ be

706: a finite alphabet and let ${\cal S}(\Sigma)$ be the set of

707: $\Sigma$-labeled infinite sequences, that is, structures of the

708: form $(\mathbb{N},<,V)$, where $(\mathbb{N},<)$ is the set of

709: natural numbers, together with the usual ordering relation, and $V

710: \, : \, \mathbb{N} \Imp \Sigma$ is a valuation function mapping

711: natural numbers into symbols in $\Sigma$.

712: 

713: \begin{definition} \thC{Sequence automata} \label{def:SA}

714: \noindent A {\em sequence automaton} $A$ over $\Sigma$ consists of

715: (i) a Labeled Transition System $(Q,q_0,\Delta,$ $M,\Omega)$,

716: where $Q$ is a finite set of states, $q_0 \in Q$ is the initial

717: state, $\Delta \subseteq Q \times \Sigma \times Q$ is a transition

718: relation, $\Omega$ is a finite alphabet, and $M \subseteq Q \times

719: \Omega$ is a labeling of states, and (ii) an acceptance condition

720: $AC$. Given a $\Sigma$-labeled infinite sequence $w =

721: (\mathbb{N},<,V)$, a {\em run} of $A$ on $w$ is a function $\sigma

722: \, : \, \mathbb{N} \Imp Q$ such that $\sigma(0) = q_0$ and

723: $(\sigma(i),V(i), \sigma(i+1)) \in \Delta$, for every $i \geq 0$.

724: The automaton $A$ accepts $w$ if there is a run $\sigma$ of $A$ on

725: $w$ such that $AC(\sigma)$, i.e., the acceptance condition holds

726: on $\sigma$. The language accepted by $A$, denoted by ${\cal

727: L}(A)$, is the set of $\Sigma$-labeled infinite sequences accepted

728: by $A$.~\dqed

729: \end{definition}

730: 

731: A class of sequence automata $\cal A$ is a set of automata that

732: share the acceptance condition $AC$ (we do not explicitly specify

733: the acceptance condition for sequence automata since, as we will

734: see, all the achieved results do not rest on any specific

735: acceptance condition). An example of a class of sequence automata

736: is the class of B\"uchi automata.

737: 

738: \begin{example} \thC{B\"uchi automata} \label{exa:fsa}

739: \noindent A B\"uchi automaton is a sequence automaton $A = (Q,

740: q_0, \Delta, M, \Omega)$ such that $\Omega = \{{\tt final}\}$. We

741: call \emph{final} a state $q$ such that $(q,{\tt final}) \in M$.

742: The acceptance condition for $A$ states that $A$ accepts a

743: $\Sigma$-labeled infinite sequence $w$ if and only if there is a

744: run $\sigma$ of $A$ on $w$ such that some final state occurs

745: infinitely often in $\sigma$. \dqed

746: \end{example}

747: 

748: %Examples of sequence automata are B\"uchi and Rabin sequence

749: %automata~\cite{T90}. A B\"uchi sequence automaton $(Q, q_0,

750: %\Delta, F)$ corresponds to a sequence automaton $(Q, q_0, \Delta,

751: %M, \Omega)$ such that $\Omega = \{{\tt final}\}$ and $M =

752: %\{(q,{\tt final}) \sep q \in F\}$. A Rabin sequence automaton $(Q,

753: %q_0, \Delta, \{(L_1,U_1), \ldots (L_m,U_m)\})$ corresponds to a

754: %sequence automaton $(Q,q_0,\Delta, M,\Omega)$ such that $\Omega =

755: %\{{\tt fin}_i, {\tt inf}_i \sep 1 \leq i \leq m\}$, $M =

756: %\bigcup_{i=1}^{m} \{(q,{\tt fin}_i) \sep q \in L_i\} \cup

757: %\{(q,{\tt inf}_i) \sep q \in U_i\}$.

758: 

759: Temporalized automata over sequence structures can be defined as

760: follows. Let ${\cal A}_2$ be a class of sequence automata which

761: accept sequences in ${\cal S}(\Sigma)$; moreover, let

762: $\Gamma(\Sigma)$ be a finite alphabet whose symbols $A,B, \ldots$

763: denote automata in ${\cal A}_2$, and let ${\cal A}_1$ be a class

764: of sequence automata which accept ($\Gamma(\Sigma)$-labeled

765: infinite) sequences in ${\cal S}(\Gamma(\Sigma))$. Given ${\cal

766: A}_1$ and ${\cal A}_2$ as above, we define a class of temporalized

767: automata ${\cal A}_1({\cal A}_2)$ that combine the two component

768: classes of automata in a suitable way. Let ${\cal S}({\cal

769: S}(\Sigma))$ be the set of infinite sequences of $\Sigma$-labeled

770: infinite sequences, that is, temporalized models

771: $(\mathbb{N},<,g)$ where $g \, : \, \mathbb{N} \Imp {\cal

772: S}(\Sigma)$ is a total function mapping elements of $\mathbb{N}$

773: into sequences in ${\cal S}(\Sigma)$. Automata in ${\cal

774: A}_1({\cal A}_2)$ accept objects in ${\cal S}({\cal S}(\Sigma))$.

775: The class of temporalized automata ${\cal A}_1({\cal A}_2)$ is

776: formally defined as follows.

777: 

778: \begin{definition} \thC{Temporalized automata} \label{def:combaut}

779: \noindent A {\em temporalized automaton} $A$ over $\Gamma(\Sigma)$

780: is a quintuple $(Q,q_0,\Delta, M,\Omega)$ as for sequence automata

781: (Definition~\ref{def:SA}). The {\em combined acceptance condition}

782: for $A$ is defined as follows. Given $w = (\mathbb{N},<,g) \in

783: {\cal S}({\cal S}(\Sigma))$, a {\em run} of $A$ on $w$ is function

784: $\sigma \, : \, \mathbb{N} \Imp Q$ such that $\sigma(0) = q_0$

785: and, for every $i \geq 0$, $(\sigma(i),B,\sigma(i+1)) \in \Delta$

786: for some $B \in \Gamma(\Sigma)$ such that $g(i) \in {\cal L}(B)$.

787: The automaton $A$ accepts $w$ if there exists a run $\sigma$ of

788: $A$ on $w$ such that $AC(\sigma)$, where $AC$ is the acceptance

789: condition of ${\cal A}_1$. The language recognized by $A$, denoted

790: by ${\cal L}(A)$, is the set of elements in ${\cal S}({\cal

791: S}(\Sigma))$ accepted by $A$.

792: %We denote by ${\cal A}_1({\cal A}_2)$ the class of

793: %temporalized automata.

794: \dqed

795: \end{definition}

796: 

797: Given a temporalized automaton $A \in {\cal A}_1({\cal A}_2)$, we

798: denote by $A^\uparrow$ the automaton in ${\cal A}_1$ with the same

799: labeling transition system as $A$ and with the acceptance

800: condition of ${\cal A}_1$. While $A$ accepts in ${\cal S}({\cal

801: S}(\Sigma))$, its {\em abstraction} $A^\uparrow$ recognizes in

802: ${\cal S}(\Gamma(\Sigma))$.  Moreover, given an automaton $A \in

803: {\cal A}_1$, we denote by $A^\downarrow$ the automaton in ${\cal

804: A}_1({\cal A}_2)$ with the same labeling transition system  as $A$

805: and with the combined acceptance condition of ${\cal A}_1({\cal

806: A}_2)$. While $A$ accepts in ${\cal S}(\Gamma(\Sigma))$, its {\em

807: concretization} $A^\downarrow$ recognizes in ${\cal S}({\cal

808: S}(\Sigma))$. Taking advantage of these notions, the combined

809: acceptance condition for temporalized automata can be rewritten as

810: follows. Let $w = (\mathbb{N},<,g) \in {\cal S}({\cal

811: S}(\Sigma))$. A temporalized automaton $A$ accepts $w$ if and only

812: if there exists $v = (\mathbb{N},<,V) \in {\cal

813: S}(\Gamma(\Sigma))$ such that $v \in {\cal L}(A^\uparrow)$ and,

814: for every $i \in \mathbb{N}$, $g(i) \in {\cal L}(V(i))$. In the

815: following, we will often use this alternative, but equivalent,

816: formulation of the combined acceptance condition for temporalized

817: automata.

818: 

819: \medskip

820: 

821: We now show that relevant logical properties transfer from

822: component automata to temporalized ones. The following notation

823: will be used to express the relationships between automata and

824: temporal logics. We write ${\cal A} \rightarrow \logic{T}$ to

825: denote the fact that every automaton $A$ in $\cal A$ can be

826: converted into a formula $\varphi_A$ in $\logic{T}$ such that

827: ${\cal L}(A) = {\cal M}(\varphi_A)$, where ${\cal M}(\varphi_A)$

828: is the set of models of $\varphi_A$. Conversely, we write

829: $\logic{T} \rightarrow {\cal A}$ to denote the fact that every

830: formula $\varphi$ in $\logic{T}$ can be converted into an

831: equivalent automaton in $\cal A$. Finally, ${\cal A}

832: \leftrightarrows \logic{T}$ stands for ${\cal A} \rightarrow

833: \logic{T}$ and $\logic{T} \rightarrow {\cal A}$. The {\em transfer

834: problem} for temporalized automata can be stated as follows.

835: Assuming that the automata classes ${\cal A}_1$ and ${\cal A}_2$

836: enjoy a given logical property, does ${\cal A}_1( {\cal A}_2)$

837: enjoy that property?  We investigate the transfer problem with

838: respect to the following properties of automata:

839: 

840: \begin{enumerate}

841: \item

842: (Effective) {\em closure} under Boolean operations (union,

843: intersection, and complementation): if ${\cal A}_1$ and ${\cal

844: A}_2$ are (effectively) closed under Boolean operations, is ${\cal

845: A}_1({\cal A}_2)$ (effectively) closed under Boolean operations?

846: \item

847: {\em Decidability}: if ${\cal A}_1$ and ${\cal A}_2$ are

848: decidable, is ${\cal A}_1({\cal A}_2)$ decidable?

849: \item

850: {\em Expressive equivalence} with respect to temporal logic: if

851: ${\cal A}_1 \leftrightarrows \logic{T_1}$ and ${\cal

852: A}_2\leftrightarrows\logic{T_2}$, does ${\cal A}_1( {\cal

853: A}_2)\leftrightarrows\tl{\logic{T_1}}{\logic{T_2}}$?

854: \end{enumerate}

855: 

856: The following lemma plays a crucial role. It shows that every

857: temporalized automaton is equivalent to a temporalized automaton

858: whose transitions are labeled with automata that form a partition

859: of the set ${\cal S}(\Sigma)$ of $\Sigma$-labeled sequences.

860: Hence, {\em different} labels of the `partitioned automaton'

861: correspond to (automata accepting) {\em disjoint} sets of

862: $\Sigma$-labeled sequences. Moreover, the partitioned automaton

863: can be effectively constructed from the original one. We will see

864: that a similar partition lemma holds for temporalized logics (cf.\

865: Lemma~\ref{lm:part2} below).

866: 

867: \begin{lemma} \thC{Partition lemma for temporalized automata}

868: \label{lm:part} \noindent Let $A$ be a temporalized automaton in

869: ${\cal A}_1({\cal A}_2)$. If ${\cal A}_2$ is closed under Boolean

870: operations (union, intersection, and complementation), then there

871: exists a finite alphabet $\Gamma'(\Sigma) \subseteq {\cal A}_2$

872: and a temporalized automaton $A'$ over $\Gamma'(\Sigma)$ such that

873: ${\cal L}(A)={\cal L}(A')$ and the set $\{{\cal L}(X) \sep X \in

874: \Gamma'(\Sigma)\}$ is a partition of ${\cal S}(\Sigma)$. Moreover,

875: if ${\cal A}_2$ is effectively closed under Boolean operations and

876: it is decidable, then $A'$ can be effectively computed from $A$.

877: \end{lemma}

878: 

879: 

880: \begin{proof}

881: To construct $\Gamma'(\Sigma)$ and $A'$ we proceed as follows. Let

882: $A = (Q,q_0,\Delta,M,\Omega)$ be a temporalized automaton over

883: $\Gamma(\Sigma) = \{X_1, \ldots X_n\} \subseteq {\cal A}_2$ . For

884: every $1 \leq i \leq n$ and $j \in \{0,1\}$, let $X_{i}^{j} = X_i$

885: for $j=0$ and $X_{i}^{j} = {\cal S}(\Sigma) \setminus X_i$ for

886: $j=1$. Given $(j_1, \ldots, j_n) \in \{0,1\}^n$, let ${\tt

887: Cap}_{(j_1, \ldots, j_n)} = \bigcap_{i=1}^{n} X_{i}^{j_i}$. We

888: define $\Gamma_{1}(\Sigma)$ as the set of all and only ${\tt

889: Cap}_{(j_1, \ldots, j_n)}$ such that $(j_1, \ldots, j_n) \in

890: \{0,1\}^n$. Since ${\cal A}_2$ is closed under Boolean operations,

891: $\Gamma_{1}(\Sigma) \subseteq {\cal A}_2$. Moreover, let

892: $\Gamma_{2}(\Sigma) = \{X \in \Gamma_{1}(\Sigma) \sep {\cal L}(X)

893: \neq \emptyset\}$. We set $\Gamma'(\Sigma) = \Gamma_{2}(\Sigma)$,

894: and, for $1 \leq i \leq n$, $\Gamma_i'(\Sigma) = \{X \in

895: \Gamma'(\Sigma) \sep X \cap X_i \neq \emptyset\}$. Note that

896: $\{{\cal L}(X) \sep X \in \Gamma'(\Sigma)\}$ is a partition of

897: ${\cal S}(\Sigma)$. Moreover, for every $1 \leq i \leq n$,

898: $\{{\cal L}(X) \sep X \in \Gamma_i'(\Sigma)\}$ is a partition of

899: ${\cal L}(X_i)$. We define the temporalized automaton $A' =

900: (Q,q_0,\Delta',M,\Omega)$ over $\Gamma'(\Sigma)$, where $\Delta'$

901: contains all and only the triples $(q_1,X,q_2) \in Q \times

902: \Gamma'(\Sigma) \times Q$ such that $X \in \Gamma_i'(\Sigma)$ and

903: $(q_1,X_i,q_2) \in \Delta$ for some $1 \leq i \leq n$. It is not

904: difficult to see that ${\cal L}(A)={\cal L}(A')$.

905: \end{proof}

906: 

907: We now prove the first transfer theorem: closure under Boolean

908: operations transfers from component automata to temporalized ones.

909: 

910: \begin{theorem} \thC{Transfer of closure under Boolean operations}

911: \label{th:traclo} \noindent Closure under Boolean operations

912: (union, intersection, and complementation) transfers from

913: component automata to temporalized ones: given two classes ${\cal

914: A}_1$ and ${\cal A}_2$ of automata which are (effectively) closed

915: under Boolean operations, the class ${\cal A}_1( {\cal A}_2)$ of

916: temporalized automata is (effectively) closed under Boolean

917: operations.

918: \end{theorem}

919: 

920: \begin{proof}

921: 

922: Let $X,Y \in {\cal A}_1( {\cal A}_2)$.

923: 

924: \medskip \noindent {\bf Union} \ \ \ We must provide an automaton

925: $A \in {\cal A}_1( {\cal A}_2)$ that recognizes the language

926: ${\cal L}(X) \cup {\cal L}(Y)$. Define $A = (X^{\uparrow} \cup

927: Y^{\uparrow})^\downarrow$. We show that ${\cal L}(A) = {\cal L}(X)

928: \cup {\cal L}(Y)$. Let $x = (\mathbb{N},<,g) \in {\cal L}(A)$.

929: Hence, there is  $y = (\mathbb{N},<,V) \in {\cal L}(A^\uparrow) =

930: {\cal L}(X^\uparrow \cup Y^\uparrow) = {\cal L}(X^\uparrow) \cup

931: {\cal L}(Y^\uparrow)$ such that, for every $i \in \mathbb{N}$,

932: $g(i) \in {\cal L}(V(i))$. Suppose $y \in {\cal L}(X^\uparrow)$.

933: It follows that $x \in {\cal L}(X)$. Hence $x \in {\cal L}(X) \cup

934: {\cal L}(Y)$. Similarly if $y \in {\cal L}(Y^\uparrow)$.

935: Conversely, suppose that $x = (\mathbb{N}, <,g) \in {\cal L}(X)

936: \cup {\cal L}(Y)$. If $x \in {\cal L}(X)$, then there is $y =

937: (\mathbb{N},<,V) \in {\cal L}(X^\uparrow)$ such that, for every $i

938: \in \mathbb{N}$, $g(i) \in {\cal L}(V(i))$. Hence, $y \in {\cal

939: L}(X^\uparrow) \cup {\cal L}(Y^\uparrow) = {\cal L}(X^\uparrow

940: \cup Y^\uparrow) = {\cal L}(A^\uparrow)$. It follows that $x \in

941: {\cal L}(A)$. Similarly if $x \in {\cal L}(Y)$.

942: 

943: \medskip \noindent {\bf Complementation} \ \ \

944: We must provide an automaton $A \in {\cal A}_1( {\cal A}_2)$ that

945: recognizes the language ${\cal S}({\cal S}(\Sigma)) \setminus

946: {\cal L}(X)$. Given Lemma~\ref{lm:part}, we may assume that

947: $\{{\cal L}(Z) \sep Z \in \Gamma(\Sigma)\}$ forms a partition of

948: ${\cal S}(\Sigma)$. We define $A = ({\cal S}(\Gamma(\Sigma))

949: \setminus X^{\uparrow})^\downarrow$. We show that ${\cal L}(A) =

950: {\cal S}({\cal S}(\Sigma)) \setminus {\cal L}(X)$. Let $x =

951: (\mathbb{N},<,g) \in {\cal L}(A)$. Hence, there exists $y =

952: (\mathbb{N},<,V) \in {\cal L}(A^\uparrow) = {\cal

953: S}(\Gamma(\Sigma)) \setminus {\cal L}(X^{\uparrow})$ such that,

954: for every $i \in \mathbb{N}$, $g(i) \in {\cal L}(V(i))$. Suppose,

955: by contradiction, that $x \in {\cal L}(X)$. It follows that there

956: exists $z = (\mathbb{N},<,V') \in {\cal L}(X^{\uparrow})$ such

957: that, for every $i \in \mathbb{N}$, $g(i) \in {\cal L}(V'(i))$.

958: Hence, for every $i \in \mathbb{N}$, $g(i) \in {\cal L}(V(i)) \cap

959: {\cal L}(V'(i))$. Since, for every $i \in \mathbb{N}$, ${\cal

960: L}(V(i)) \cap {\cal L}(V'(i)) = \emptyset$ whenever $V(i) \not =

961: V'(i)$, we conclude that $V(i) = V'(i)$. Hence $V = V'$ and thus

962: $y=z$. This is a contradiction since $y$ and $z$ belong to

963: disjoint sets. It follows that $x \in {\cal S}({\cal S}(\Sigma))

964: \setminus {\cal L}(X)$.

965: 

966: We now prove the opposite direction. Let $x = (\mathbb{N},<,g) \in

967: {\cal S}({\cal S}(\Sigma)) \setminus {\cal L}(X)$. It follows

968: that, for every $y = (\mathbb{N},<,V) \in {\cal L}(X^\uparrow)$,

969: there exists $i \in \mathbb{N}$ such that $g(i) \not \in {\cal

970: L}(V(i))$. Suppose, by contradiction, that $x \in {\cal S}({\cal

971: S}(\Sigma)) \setminus {\cal L}(A)$. It follows that, for every $z

972: = (\mathbb{N},<,V) \in {\cal L}(A^\uparrow) = {\cal

973: S}(\Gamma(\Sigma)) \setminus {\cal L}(X^\uparrow)$, there exists

974: $i \in \mathbb{N}$ such that $g(i) \not \in {\cal L}(V(i))$. We

975: can conclude that, for every $v = (\mathbb{N},<,V) \in {\cal

976: S}(\Gamma(\Sigma))$, there exists $i \in \mathbb{N}$ such that

977: $g(i) \not \in {\cal L}(V(i))$. This is a contradiction: since

978: $\{{\cal L}(Z) \sep Z \in \Gamma(\Sigma)\}$ forms a partition of

979: ${\cal S}(\Sigma)$, for every $i \in \mathbb{N}$, there is $Y_i

980: \in \Gamma(\Sigma)$ such that $g(i) \in {\cal L}(Y_i)$. We have

981: that $(\mathbb{N},<,V')$, with $V'(i) = Y_i$, is an element of

982: ${\cal S}(\Gamma(\Sigma))$ and, for every $i \in \mathbb{N}$,

983: $g(i) \in {\cal L}(V'(i))$. We conclude that $x \in {\cal L}(A)$.

984: 

985: \medskip \noindent {\bf Intersection} \ \ \ It follows from

986: closure under union and complementation using De~Morgan's laws.

987: \end{proof}

988: 

989: It is worth noticing that if $A = (X^{\uparrow} \cap

990: Y^{\uparrow})^\downarrow$, then ${\cal L}(A) \subseteq {\cal L}(X)

991: \cap {\cal L}(Y)$, while the opposite inclusion ${\cal L}(X) \cap

992: {\cal L}(Y) \subseteq {\cal L}(A)$ does not hold in general. We

993: give a simple counterexample. Let $\Gamma(\Sigma) = \{B,C\}$,

994: $X^\uparrow$ be the automaton accepting sequences starting with

995: the symbol $B$, and $Y^\uparrow$ be the automaton accepting

996: strings starting with the symbol $C$. Then, ${\cal L}(

997: X^{\uparrow} \cap Y^{\uparrow}) = \emptyset$ and hence ${\cal

998: L}(A) = \emptyset$. Let $\Sigma = \{a,b\}$, $B$ be the automaton

999: accepting sequences with an odd number of symbols $a$, and $C$ be

1000: the automaton recognizing sequences with a prime number of symbols

1001: $a$. ${\cal L}(X) \cap {\cal L}(Y)$ contains, for instance, a

1002: combined structure starting with a sequence with exactly 13

1003: occurrences of symbol $a$, and hence it is not empty.

1004: 

1005: \medskip

1006: 

1007: We now focus on the problem of establishing whether decidability

1008: transfers from component automata to temporalized ones. Given $A

1009: \in {\cal A}_1( {\cal A}_2)$, it is easy to see that a sufficient

1010: condition for ${\cal L}(A) = \emptyset$ is that ${\cal

1011: L}(A^\uparrow) = \emptyset$. However, this condition is not

1012: necessary, since ${\cal L}(A) = \emptyset$ may depend on the fact

1013: that some ${\cal A}_2$-automata labeling $A$ accept the empty

1014: language. However, if we know that $A$ is labeled with ${\cal

1015: A}_2$-automata recognizing non-empty languages, then the condition

1016: ${\cal L}(A^\uparrow) = \emptyset$ is both necessary and

1017: sufficient for ${\cal L}(A) = \emptyset$. In the following

1018: theorem, we take advantage of these considerations to devise an

1019: algorithm that checks emptiness for temporalized automata.

1020: 

1021: \begin{theorem} \thC{Transfer of decidability} \label{th:tradec}

1022: \noindent Decidability transfers from component automata to

1023: temporalized ones: given two decidable classes  of automata ${\cal

1024: A}_1$ and ${\cal A}_2$, the class ${\cal A}_1( {\cal A}_2)$ of

1025: temporalized automata is decidable.

1026: \end{theorem}

1027: 

1028: \begin{proof} Let $A$ be a temporalized automaton in ${\cal

1029: A}_1( {\cal A}_2)$.  We describe an algorithm that returns $1$ if

1030: ${\cal L}(A) = \emptyset$ and $0$ otherwise.

1031: 

1032: \begin{description} \item{\bf Step 1} Verify whether ${\cal

1033: L}(A^\uparrow) = \emptyset$ using the algorithm that checks

1034: emptiness for ${\cal A}_1$. If ${\cal L}(A^\uparrow) = \emptyset$,

1035: then return $1$.

1036: \item{\bf Step 2} For every $X \in \Gamma(\Sigma)$, if ${\cal

1037: L}(X) = \emptyset$ (this test can be performed by exploiting the

1038: algorithm that checks emptiness for ${\cal A}_2$), then remove

1039: every transition of the form $(q_1,X,q_2)$ from the transition

1040: relation of $A$.

1041: \item{\bf Step 3} Let $B$ be the temporalized automaton obtained

1042: from $A$ after Step 2. Check, using the emptiness algorithm for

1043: ${\cal A}_1$, whether ${\cal L}(B^\uparrow) = \emptyset$. If

1044: ${\cal L}(B^\uparrow) = \emptyset$, then return $1$, else return

1045: $0$.

1046: \end{description}

1047: 

1048: The algorithm always terminates returning either $1$ or $0$. We

1049: prove that the algorithm returns $1$ if and only if ${\cal L}(A) =

1050: \emptyset$. Suppose that the algorithm returns $1$. If ${\cal

1051: L}(A^\uparrow) = \emptyset$, then ${\cal L}(A) = \emptyset$.

1052: Suppose now that ${\cal L}(A^\uparrow) \not = \emptyset$ and

1053: ${\cal L}(B^\uparrow) = \emptyset$. Note that ${\cal L}(A) = {\cal

1054: L}(B)$, since $B$ is obtained from $A$ by cutting off automata

1055: accepting the empty language. Assume, by contradiction, that there

1056: is $x \in {\cal L}(A)$. Since ${\cal L}(A) = {\cal L}(B)$, we have

1057: that $x \in {\cal L}(B)$. Hence ${\cal L}(B)$ in not empty. Since

1058: ${\cal L}(B^\uparrow) = \emptyset$, we have that ${\cal L}(B)$ is

1059: empty which is a contradiction. Hence ${\cal L}(A) = \emptyset$.

1060: Suppose now that the algorithm returns $0$. Then ${\cal

1061: L}(B^\uparrow)$ contains at least one element, say $x =

1062: (\mathbb{N},<,V)$. Since $B$ uses only non-empty ${\cal

1063: A}_2$-automata as alphabet symbols, we have that, for every $i \in

1064: \mathbb{N}$, ${\cal L}(V(i)) \neq \emptyset$. Hence $y =

1065: (\mathbb{N},<,g)$, with $g$ such that, for every $i \in

1066: \mathbb{N}$, $g(i)$ equals to some element of ${\cal L}(V(i))$, is

1067: an element of ${\cal L}(A)$. Hence ${\cal L}(A) \not = \emptyset$

1068: \end{proof}

1069: 

1070: Finally, we consider the problem of establishing whether

1071: expressive equivalence with respect to temporal logics transfers

1072: from component automata to temporalized ones. We first state a

1073: partition lemma for temporalized logics. The proof is similar to

1074: the one of Lemma~\ref{lm:part}, and thus omitted.

1075: 

1076: \begin{lemma} \thC{Partition Lemma for temporalized logics}

1077: \label{lm:part2} \noindent Let $\varphi$ be a temporalized formula

1078: of $\tl{T_1}{T_2}$ and $\alpha_1, \ldots, \alpha_n$ be the maximal

1079: $\logic{T_2}$-formulas of $\varphi$. Then, there exists a finite

1080: set $\Lambda$ of $\logic{T_2}$-formulas such that:

1081: \begin{enumerate}

1082: \item

1083: the set $\{{\cal M}(\alpha) \sep \alpha \in \Lambda\}$ is a

1084: partition of $\bigcup_{i=1}^{n} {\cal M}(\alpha_i)$, and

1085: \item

1086: the formula $\varphi'$ obtained by replacing every

1087: $\logic{T_2}$-formula $\alpha_i$ in $\varphi$ with $\bigvee

1088: \{\alpha \sep \alpha \in \Lambda \mbox{ and } {\cal M}(\alpha)

1089: \cap {\cal M}(\alpha_i) \neq \emptyset\}$ is equivalent to

1090: $\varphi$, i.e., ${\cal M}(\varphi) = {\cal M}(\varphi')$.

1091: \end{enumerate}

1092: \end{lemma}

1093: 

1094: The following theorem shows that expressive equivalence with

1095: respect to temporal logics transfers from component automata to

1096: temporalized ones.

1097: 

1098: 

1099: \begin{theorem} \thC{Transfer of expressive equivalence w.r.t.\

1100: temporal logic} \label{th:traexp} \noindent Expressive equivalence

1101: w.r.t.\ temporal logic transfers from component automata to

1102: temporalized ones: if ${\cal A}_1 \leftrightarrows \logic{T_1}$

1103: ${\cal A}_2 \leftrightarrows \logic{T_2}$, and ${\cal A}_2$ is

1104: closed under Boolean operations, then ${\cal A}_1( {\cal A}_2)

1105: \leftrightarrows \tl{T_1}{T_2}$.

1106: \end{theorem}

1107: 

1108: \begin{proof}

1109: We first prove that ${\cal A}_1( {\cal A}_2) \rightarrow

1110: \tl{T_1}{T_2}$. Let $A \in {\cal A}_1( {\cal A}_2)$ be a

1111: temporalized automaton over $\Gamma(\Sigma) = \{X_1, \ldots ,

1112: X_n\} \subseteq {\cal A}_2$. We have to find a temporalized

1113: formula $\varphi_A \in  \tl{T_1}{T_2}$ such that ${\cal L}(A) =

1114: {\cal M}(\varphi_A)$. Since ${\cal A}_2$ is closed under Boolean

1115: operations, by exploiting Lemma~\ref{lm:part}, we may assume that

1116: $\{{\cal L}(X_1), \ldots , {\cal L}(X_n)\}$ partitions ${\cal

1117: S}(\Sigma)$. Since ${\cal A}_1 \rightarrow \logic{T_1}$, there

1118: exists a translation $\tau_1$ from ${\cal A}_1$-automata to

1119: $\logic{T_1}$-formulas such that, for every $X \in {\cal A}_1$,

1120: ${\cal L}(X) = {\cal M}(\tau_1(X))$. Let $\varphi_{A^\uparrow} =

1121: \tau_1(A^\uparrow)$. The formula $\varphi_{A^\uparrow}$ uses

1122: proposition letters in $\{P_{X_1}, \ldots , P_{X_n}\}$. Moreover,

1123: since ${\cal A}_2 \rightarrow \logic{T_2}$, there exists a

1124: translation $\sigma_1$ from ${\cal A}_2$-automata to

1125: $\logic{T_2}$-formulas such that, for every $X \in {\cal A}_2$,

1126: ${\cal L}(X) = {\cal M}(\sigma_1(X))$. For every $1 \leq i \leq

1127: n$, let $\varphi_{X_i} = \sigma_1(X_i)$. For every proposition

1128: letter $P_{X_i}$ appearing in $\varphi_{A^\uparrow}$, replace

1129: $P_{X_i}$ by $\varphi_{X_i}$ in $\varphi_{A^\uparrow}$. Let

1130: $\varphi_A$ be the resulting formula. It is immediate to see that

1131: $\varphi_A \in \tl{T_1}{T_2}$. We prove that ${\cal L}(A) = {\cal

1132: M}(\varphi_A)$.

1133: 

1134: \medskip \noindent

1135: ($\subseteq$) \ \ \ Let $x = (\mathbb{N},<,g) \in {\cal L}(A)$.

1136: This implies that there exists $x^\uparrow = (\mathbb{N},<,V) \in

1137: {\cal S}(\Gamma(\Sigma))$ such that $x^\uparrow \in {\cal

1138: L}(A^\uparrow)$ and, for every $i \in \mathbb{N}$, $g(i) \in {\cal

1139: L}(V(i))$.  Since ${\cal L}(A^\uparrow) = {\cal

1140: M}(\varphi_{A^\uparrow})$, we have that $x^\uparrow \in {\cal

1141: M}(\varphi_{A^\uparrow})$.  We prove that, for every $i \in

1142: \mathbb{N}$ and $j \in \{1, \ldots , n\}$, $x^\uparrow, i \models

1143: P_{X_j}$ if and only if $x,i \models \varphi_{X_j}$. Let $i \in

1144: \mathbb{N}$ and $j \in \{1, \ldots , n\}$. We know that

1145: $x^\uparrow, i \models P_{X_j}$ if and only if $V(i) = X_j$. We

1146: first prove that $V(i) = X_j$ if and only if $g(i) \in {\cal

1147: L}(X_j)$. The left to right direction immediately follows since

1148: $g(i) \in {\cal L}(V(i))$. We prove the right to left direction by

1149: contradiction. Suppose $g(i) \in {\cal L}(X_j)$ and $V(i) = X_k

1150: \neq X_j$. Hence $g(i) \in {\cal L}(V(i)) = {\cal L}(X_k)$ and

1151: thus $g(i) \in {\cal L}(X_j) \cap {\cal L}(X_k)$, which is a

1152: contradiction, since ${\cal L}(X_j) \cap {\cal L}(X_k) =

1153: \emptyset$. Hence $V(i)  = X_j$. Finally, we have that $g(i) \in

1154: {\cal L}(X_j)$ if and only if $g(i) \in {\cal M}(\varphi_{X_j})$

1155: if and only if $x,i \models \varphi_{X_j}$. Summing up, we have

1156: that $x^\uparrow \in {\cal M}(\varphi_{A^\uparrow})$ and, for

1157: every $i \in \mathbb{N}$ and $j \in \{1, \ldots , n\}$,

1158: $x^\uparrow, i \models P_{X_j}$ if and only if $x,i \models

1159: \varphi_{X_j}$. It follows that $x \in {\cal M}(\varphi_A)$.

1160: 

1161: \medskip \noindent

1162: ($\supseteq$) \ \ \ Let $x = (\mathbb{N},<,g) \in {\cal

1163: M}(\varphi_A)$. We define $x^\uparrow = (\mathbb{N},<,V) \in {\cal

1164: S}(\Gamma(\Sigma))$ in such a way that, for every $i \in

1165: \mathbb{N}$, $V(i) = X_j$ if and only if $g(i) \in {\cal

1166: M}(\varphi_{X_j}) = {\cal L}(X_j)$. Notice that $V(i)$ is always

1167: and univocally defined, since $\{{\cal L}(X_1), \ldots , {\cal

1168: L}(X_n)\}$ partitions ${\cal S}(\Sigma)$. We prove that, for every

1169: $i \in \mathbb{N}$ and $j \in \{1, \ldots, n\}$, we have that

1170: $x^\uparrow, i \models P_{X_j}$ if and only if $x,i \models

1171: \varphi_{X_j}$. Let $i \in \mathbb{N}$ and $j \in \{1, \ldots ,

1172: n\}$. We know that $x^\uparrow, i \models P_{X_j}$ if and only if

1173: $V(i) = X_j$. We first prove that $V(i) = X_j$ if and only if

1174: $g(i) \in {\cal L}(X_j)$. The left to right direction immediately

1175: follows by definition of $x^\uparrow$.The right to left direction

1176: follows since ${\cal L}(X_j) \cap {\cal L}(X_k) = \emptyset$

1177: whenever $k \neq j$. Finally, $g(i) \in {\cal L}(X_j)$ if and only

1178: if $g(i) \in {\cal M}(\varphi_{X_j})$ if and only if $x,i \models

1179: \varphi_{X_j}$. Summing up, we have that $x^\uparrow \in {\cal

1180: M}(\varphi_{A^\uparrow}) = {\cal L}(A^\uparrow)$ and, for every $i

1181: \in \mathbb{N}$, $g(i) \in {\cal M}(\varphi_{X_j}) = {\cal

1182: M}(\varphi_{V(i)}) = {\cal L}(V(i))$. Therefore, $x \in {\cal

1183: L}(A)$.

1184: 

1185: \medskip

1186: \noindent We now prove that $\tl{T_1}{T_2} \rightarrow {\cal A}_1(

1187: {\cal A}_2)$. Let $\varphi \in \tl{T_1}{T_2}$ be a temporalized

1188: formula. We have to find a temporalized automaton $A_\varphi \in

1189: {\cal A}_1( {\cal A}_2)$ such that ${\cal M}(\varphi) = {\cal

1190: L}(A_\varphi)$. Let $\alpha_1, \ldots, \alpha_n$ be the maximal

1191: $\logic{T_2}$-formulas of $\varphi$.  By exploiting

1192: Lemma~\ref{lm:part2}, we may assume that there exists a finite set

1193: $\Lambda$ of $\logic{T_2}$-formulas such that the set $\{{\cal

1194: M}(\alpha) \sep \alpha \in \Lambda\}$ forms a partition of

1195: $\bigcup_{i=1}^{n} {\cal M}(\alpha_i)$, and every maximal

1196: $\logic{T_2}$-formula $\alpha_i$ in $\varphi$ has the form

1197: $\bigvee \{\alpha \sep \alpha \in \Lambda \mbox{ and } {\cal

1198: M}(\alpha) \cap {\cal M}(\alpha_i) \neq \emptyset\}$.

1199: 

1200: Let $\varphi^\uparrow$ be the formula obtained from $\varphi$ by

1201: replacing every $\logic{T_2}$-formula $\alpha \in \Lambda$

1202: appearing in $\varphi$ with proposition letter $P_\alpha$ and by

1203: adding to the resulting formula the conjunct $P_\beta \Or \neg

1204: P_\beta$, where $\beta$ is the $\logic{T_2}$-formula $\neg

1205: \bigvee_{i=1}^{n} \alpha_i$. Let ${\cal Q} = {\{P_{\alpha} \sep

1206: \alpha \in \Lambda \cup \{\beta\}\}}$ be the set of proposition

1207: letters of $\varphi^\uparrow$. Since $\logic{T_1}\rightarrow {\cal

1208: A}_1$, there exists a translation $\tau_2$ from

1209: $\logic{T_1}$-formulas to ${\cal A}_1$-automata such that, for

1210: every $\psi \in \logic{T_1}$, ${\cal M}(\psi) = {\cal

1211: L}(\tau_2(\psi))$. Let $A_{\varphi^\uparrow} =

1212: \tau_2(\varphi^\uparrow)$. The automaton $A_{\varphi^\uparrow}$

1213: labels its transitions with symbols in $2^{\cal Q}$. Moreover,

1214: since $\logic{T_2}\rightarrow {\cal A}_2 $, there exists a

1215: translation $\sigma_2$ from $\logic{T_2}$-formulas to ${\cal

1216: A}_2$-automata such that, for every $\psi \in \logic{T_2}$, ${\cal

1217: M}(\psi) = {\cal L}(\sigma_2(\psi))$. For every $\alpha \in

1218: \Lambda \cup \{\beta\}$, let $A_{\alpha} = \sigma_2(\alpha)$.

1219: Finally, let $A_\varphi$ be the automaton obtained by replacing

1220: every label $X \subseteq {\cal Q}$ on a transition of

1221: $A_{\varphi^\uparrow}$ with the ${\cal A}_2$-automaton

1222: $\bigcap_{P_\alpha \in X} A_{\alpha} =

1223: \sigma_2(\bigwedge_{P_\alpha \in X} \alpha)$. We have that

1224: $A_\varphi \in {\cal A}_1( {\cal A}_2)$ and ${\cal L}(A_\varphi) =

1225: {\cal M}(\varphi)$. The proof is similar to the case ${\cal L}(A)

1226: = {\cal M}(\varphi_A)$. Notice that to prove this direction we did

1227: not use the hypothesis of closure under Boolean operations of

1228: ${\cal A}_2$.

1229: \end{proof}

1230: 

1231: The following corollary shows that, whenever $\logic{T_1}

1232: \rightarrow {\cal A}_1$ and $\logic{T_2} \rightarrow {\cal A}_2$,

1233: the decidability problem for $\logic{T_1}(\logic{T_2})$ can be

1234: reduced to the decidability problems for ${\cal A}_1$ and ${\cal

1235: A}_2$.

1236: 

1237: \begin{corollary}\label{co:dec}

1238: If $\logic{T_1}  \rightarrow {\cal A}_1$, $\logic{T_2} \rightarrow

1239: {\cal A}_2$, and both ${\cal A}_1$ and ${\cal A}_2$ are decidable,

1240: then $\logic{T_1}(\logic{T_2})$ is decidable.

1241: \end{corollary}

1242: 

1243: Theorems~\ref{th:traclo},~\ref{th:tradec} and~\ref{th:traexp} hold

1244: for automata that operate on finite sequences as well; moreover,

1245: they can be immediately generalized to automata on finite and

1246: infinite trees (definitions of all these classes of automata can

1247: be found in~\cite{T90}). They remain valid for automata on

1248: temporalized structures that mix sequences and trees.

1249: 

1250: Corollary~\ref{co:dec} allows one to prove the decidability of

1251: many temporalized logics. For instance, it is well-known that

1252: $\qltl$ (and all its fragments) over infinite sequences can be

1253: embedded into B\"uchi sequence automata, $\qdctls$ (and all its

1254: fragments) over infinite $k$-ary trees can be embedded into Rabin

1255: $k$-ary tree automata, and both B\"uchi sequence and Rabin $k$-ary

1256: tree automata are decidable. Moreover, $\qltl$ (and all its

1257: fragments) over finite sequences can be embedded into finite

1258: sequence automata, $\qdctls$ (and all its fragments) over finite

1259: $k$-ary trees can be embedded into finite $k$-ary tree automata,

1260: and both finite sequence and finite $k$-ary tree automata are

1261: decidable. From Corollary~\ref{co:dec}, it follows that any

1262: temporalized logic $\tl{\logic{T_1}} {\logic{T_2}}$, where

1263: $\logic{T_1}$ and $\logic{T_2}$ are (fragments of) $\qltl$ or

1264: $\qdctls$, interpreted over either finite or infinite sequence or

1265: tree structures, are decidable. As a matter of fact, the

1266: decidability of $\tl{\ptl}{\ptl}$ over infinite sequences of

1267: infinite sequences was already proved in~\cite{FG92} following a

1268: different approach.

1269: 

1270: \section{Temporalized logics and automata for time granularity}

1271: \label{sec:timegran}

1272: 

1273: In the following, we use temporalized automata to find the

1274: (combined) temporal logic counterparts of the monadic second-order

1275: theories of downward and upward layered structures. Both results

1276: rest on an alternative view of DULSs and UULSs as infinite

1277: sequences of $k$-ary trees of a suitable form. More precisely,

1278: DULSs can be viewed as infinite sequences of infinite $k$-ary

1279: trees, while UULSs can be interpreted as infinite sequences of

1280: finite {\em increasing} $k$-ary trees. In Section~\ref{sec:DULS}

1281: we provide the monadic second-order theory of DULSs with an

1282: expressively complete and elementarily decidable temporalized

1283: logic counterpart by exploiting a temporalization of B\"uchi and

1284: Rabin automata. Then, in Section~\ref{sec:UULS}, we define a

1285: suitable combination of B\"uchi and finite tree automata and use

1286: it to obtain a combined temporal logic which is both elementarily

1287: decidable and expressively complete with respect to the monadic

1288: second-order theory of UULSs. It is worth remarking that, unlike

1289: the case of DULSs, the combined model we use to encode an UULS

1290: differs from that of temporalization since the innermost submodels

1291: are {\em not} independent from the outermost top-level model.

1292: 

1293: The monadic second-order language for time granularity ${\rm

1294: MSO}_{\cal P}[<, (\downarrow_i)_{i=0}^{k-1}]$ is defined as

1295: follows.

1296: 

1297: \begin{definition} \thC{Monadic second-order language}

1298: \noindent Let ${\rm MSO}_{\cal P}[<, (\downarrow_i)_{i=0}^{k-1}]$

1299: be the second-order language with equality  built up as follows:

1300: (i) {\em atomic formulas\/} are of the forms $x = y$, $x < y$,

1301: $\downarrow_i(x) = y$, $x \in X$ and $x \in P$, where $0 \leq i

1302: \leq k-1$, $x$, $y$ are individual variables, $X$ is a set

1303: variable, and $P \in {\cal P}$; (ii) {\em formulas\/} are built up

1304: starting from atomic formulas by means of the Boolean connectives

1305: $\neg$ and $\wedge$, and the quantifier $\exists$ ranging over

1306: both individual and set variables. \dqed

1307: \end{definition}

1308: 

1309: We interpret ${\rm MSO}_{\cal P}[<, (\downarrow_i)_{i=0}^{k-1}]$

1310: over DULSs and UULSs. For all $i \geq 0$, let $T^i = \{j_i \sep j

1311: \geq 0\}$. A $\cal P$-labeled $k$-refinable DULS is a tuple

1312: $\langle \bigcup_{i \geq 0} T^i, (\downarrow_i)_{i=0}^{k-1}, <,

1313: (P)_{P \in {\cal P}} \rangle$. Part of a $2$-refinable DULS is

1314: depicted in Figure~\ref{fig:down}. A DULS can be viewed as an

1315: infinite sequence of complete $k$-ary infinite trees, each one

1316: rooted at a point of $T^0$. The sets in $\{T^i\}_{i \geq 0}$ are

1317: the layers of the trees, $\downarrow_i$ is a projection function

1318: such that $\downarrow_i(a_b) = c_d$ if and only if $d = b+1$ and

1319: $c = a \cdot k + i$, with $i = 0, \ldots, k-1$, $<$ is a total

1320: ordering over $\bigcup_{i \geq 0} T^i$ given by the {\em preorder}

1321: (root-left-right) visit of the nodes (for elements belonging to

1322: the same tree) and by the total linear ordering of trees (for

1323: elements belonging to different trees), and, for all $P \in {\cal

1324: P}$, $P$ is the set of points in $\bigcup_{i \geq 0} T^i$ labeled

1325: with letter $P$. A $\cal P$-labeled $k$-refinable UULS is a tuple

1326: $\langle \bigcup_{i \geq 0} T^i, (\downarrow_i)_{i=0}^{k-1}, <,

1327: (P)_{P \in {\cal P}} \rangle$.  Part of a $2$-refinable UULS is

1328: depicted in Figure~\ref{fig:up}. An UULS can be viewed as a

1329: $k$-ary infinite tree generated from the leaves. The sets in

1330: $\{T^i\}_{i \geq 0}$ represent the layers of the tree,

1331: $\downarrow_i$ is a projection function such that

1332: $\downarrow_i(a_0) = \bot$, for all $a$, and $\downarrow_i(a_b) =

1333: c_d$ if and only if $b > 0$, $b = d+1$ and $c = a \cdot k + i$,

1334: with $i = 0, \ldots, k-1$, $<$ is the total ordering of

1335: $\bigcup_{i \geq 0} T^i$ given by the {\em inorder}

1336: (left-root-right) visit of the nodes, and, for all $P \in {\cal

1337: P}$, $P$ is the set of points in $\bigcup_{i \geq 0} T^i$ labeled

1338: with letter $P$. Given a formula $\varphi \in {\rm MSO}_{\cal

1339: P}[<, (\downarrow_i)_{i=0}^{k-1}]$, we denote by ${\cal

1340: M}(\varphi)$ the set of models of $\varphi$.

1341: 

1342: For technical reasons, it is convenient to work with a different,

1343: but equivalent, monadic second-order logic over DULSs that

1344: replaces the total ordering $<$ by two partial orderings $<_1$ and

1345: $<_2$ defined as follows. Let $t$ be a DULS. According to the

1346: interpretation of DULSs as tree sequences, we define $x <_1 y$ if

1347: and only if $x$ is the root of some tree $t_i$ of $t$, $y$ is the

1348: root of some tree $t_j$ of $t$, and $i<j$ over natural numbers.

1349: Moreover, $x <_2 y$ if and only if $y$ is different from $x$ and

1350: $y$ belongs to the tree rooted at $x$. In a similar way, it is

1351: convenient to work with a different, but equivalent, monadic

1352: second-order logic over UULSs that replaces the total ordering $<$

1353: with a partial ordering $<_{pre}$ such that $x <_{pre} y$ if and

1354: only if $y$ is different from $x$ and $y$ belongs to the tree

1355: rooted at $x$.

1356: 

1357: \subsection{Downward unbounded layered structures}

1358: \label{sec:DULS}

1359: 

1360: 

1361: We start with a formalization of the alternative characterization

1362: of DULSs as suitable tree sequences given above. Let ${\cal

1363: T}_k({\cal P})$ be the set of ${\cal P}$-labeled infinite $k$-ary

1364: trees. Let ${\cal S}({\cal T}_k({\cal P}))$ be the set of infinite

1365: sequences of ${\cal P}$-labeled infinite $k$-ary trees, that is,

1366: temporalized models $(\mathbb{N},<,g)$ where $g \, : \, \mathbb{N}

1367: \Imp {\cal T}_k({\cal P})$. ${\cal P}$-labeled DULSs correspond to

1368: tree sequences in ${\cal S}({\cal T}_k({\cal P}))$, and vice

1369: versa. On the one hand, ${\cal P}$-labeled DULS $t$ can be viewed

1370: as an infinite sequence of ${\cal P}$-labeled infinite $k$-ary

1371: trees, whose $i$-th tree, denoted by $t_i$, is the ${\cal

1372: P}$-labeled tree rooted at the $i$-th point $i_0$ of the coarsest

1373: domain $T^0$ of $t$ (cf.\ Figure~\ref{fig:treeseq1}). Such a

1374: sequence can be represented as the temporalized model

1375: $(\mathbb{N},<,g) \in {\cal S}({\cal T}_k({\cal P}))$ such that,

1376: for every $i \in \mathbb{N}$, $g(i) = t_i$. On the other hand, it

1377: is immediate to reinterpret infinite sequences of ${\cal

1378: P}$-labeled infinite $k$-ary trees in terms of ${\cal P}$-labeled

1379: DULSs.

1380: 

1381: 

1382: \begin{figure}[t]

1383: \begin{center}

1384: \begin{picture}(360,90)

1385: \put(-10,-10){\begin{picture}(170,90) \put(90,90){\circle*{3}}

1386: \put(90,90){\line(1,0){250}} %linea orizzontale

1387: \multiput(50,70)(80,0){2}{\circle*{3}}

1388: %\put(50,70){\line(1,0){290}} %linea orizzontale

1389: \put(50,70){\line(2,1){40}} \put(130,70){\line(-2,1){40}}

1390: \multiput(30,50)(40,0){4}{\circle*{3}}

1391: %\put(30,50){\line(1,0){310}} %linea orizzontale

1392: \multiput(30,50)(80,0){2}{\line(1,1){20}}

1393: \multiput(70,50)(80,0){2}{\line(-1,1){20}}

1394: \multiput(20,30)(20,0){8}{\circle*{3}}

1395: %\put(20,30){\line(1,0){320}} %linea orizzontale

1396: \multiput(20,30)(40,0){4}{\line(1,2){10}}

1397: \multiput(40,30)(40,0){4}{\line(-1,2){10}}

1398: \multiput(15,20)(20,0){8}{\line(1,2){5}}

1399: \multiput(25,20)(20,0){8}{\line(-1,2){5}}

1400: \multiput(14,10)(20,0){8}{$\ldots$} \put(90,100){$t_0$}

1401: \put(260,100){$t_1$}

1402: \end{picture}}

1403: %

1404: \put(160,-10){\begin{picture}(170,90) \put(90,90){\circle*{3}}

1405: \multiput(50,70)(80,0){2}{\circle*{3}} \put(50,70){\line(2,1){40}}

1406: \put(130,70){\line(-2,1){40}}

1407: \multiput(30,50)(40,0){4}{\circle*{3}} \put(175,30){$...$}

1408: \put(175,50){$...$} \put(175,70){$...$} \put(175,90){$...$}

1409: \multiput(30,50)(80,0){2}{\line(1,1){20}}

1410: \multiput(70,50)(80,0){2}{\line(-1,1){20}}

1411: \multiput(20,30)(20,0){8}{\circle*{3}}

1412: \multiput(20,30)(40,0){4}{\line(1,2){10}}

1413: \multiput(40,30)(40,0){4}{\line(-1,2){10}}

1414: \multiput(15,20)(20,0){8}{\line(1,2){5}}

1415: \multiput(25,20)(20,0){8}{\line(-1,2){5}}

1416: \multiput(14,10)(20,0){8}{$\ldots$} \put(175,10){$...$}

1417: \end{picture}}

1418: \end{picture}

1419: \caption{\label{fig:treeseq1} A tree sequence.}

1420: \end{center}

1421: \end{figure}

1422: 

1423: Such a correspondence between DULSs and temporalized models

1424: enables us to use temporalized logics

1425: $\tl{\logic{T_1}}{\logic{T_2}}$, where $\logic{T_1}$ is a linear

1426: time logic and $\logic{T_2}$ is a branching time logic, to express

1427: properties of DULSs. Furthermore, taking advantage of the

1428: correspondence between temporalized logic and automata, we can

1429: equivalently use temporalized automata $\tl{{\cal A}_1}{{\cal

1430: A}_2}$ over DULSs, where ${\cal A}_1$ is a class of sequence

1431: automata and ${\cal A}_2$ is a class of tree automata. In the

1432: following, we will focus on the class ${\cal B}({\cal R}_k)$ of

1433: temporalized automata embedding Rabin $k$-ary tree automata into

1434: B\"uchi sequence automata. We call automata in this class {\em

1435: infinite tree sequence automata}. Since both ${\cal B}$ and ${\cal

1436: R}_k$ are effectively closed under Boolean operations and

1437: decidable, Theorems~\ref{th:traclo} and~\ref{th:tradec} allow us

1438: to conclude that the class ${\cal B}({\cal R}_k)$ of infinite tree

1439: sequence automata is effectively closed under Boolean operations

1440: and decidable as well. The complexity of the emptiness problem for

1441: infinite tree sequence automata is given by the following theorem.

1442: 

1443: \begin{theorem}

1444: \thC{Complexity of infinite tree sequence automata}

1445: \label{th:compTSA} \noindent The emptiness problem for infinite

1446: tree sequence automata is decidable in polynomial time in the

1447: number of states, and exponential time in the number of accepting

1448: pairs.

1449: \end{theorem}

1450: 

1451: \begin{proof}

1452: For any given $A \in {\cal B}({\cal R}_k)$, let $n$ be the number

1453: of states of $A$ and $N$ (resp.\ $M$) be the maximum number of

1454: states (resp.\ accepting pairs) of a Rabin tree automaton labeling

1455: transitions in $A$. The emptiness of B\"uchi sequence automata can

1456: be checked in polynomial time in the number of states, while the

1457: emptiness of Rabin tree automata can be verified in polynomial

1458: time in the number of states, and exponential time in the number

1459: of accepting pairs. By applying the algorithm used to test the

1460: emptiness of temporalized automata in the proof of

1461: Theorem~\ref{th:tradec}, we have that the complexity of checking

1462: whether $A$ accepts the empty language is polynomial in $n$ and

1463: $N$, and exponential in $M$.

1464: \end{proof}

1465: 

1466: The following theorem relates infinite tree sequence automata to

1467: the monadic second-order theory of DULSs.

1468: 

1469: \begin{theorem}

1470: \thC{Expressiveness of infinite tree sequence automata}

1471: \label{th:expTSA} \noindent Infinite tree sequence automata are as

1472: expressive as the monadic second-order theory of DULSs.

1473: \end{theorem}

1474: 

1475: \begin{proof}

1476: 

1477: The proof can be accomplished following a proof strategy that

1478: closely resembles those adopted to prove classical results in the

1479: field, such as, for instance, the proof of B\"uchi's Theorem

1480: (cf.~\cite{T90}). We split it in two parts:

1481: 

1482: \begin{description}

1483: \item{(a)}

1484: we first show that, for every automaton $A \in {\cal B}({\cal

1485: R}_k)$ over $\Gamma(\Sigma)$, there exists a formula $\varphi_A

1486: \in {\rm MSO}_{{\cal P}_\Sigma}[<_1,<_2,

1487: (\downarrow_i)_{i=0}^{k-1}]$ over ${\cal P}_\Sigma = \{P_a \sep a

1488: \in \Sigma\}$ such that ${\cal L}(A) = {\cal M}(\varphi_A)$;

1489: \item{(b)}

1490: then, we show that, for every formula $\varphi \in {\rm MSO}_{\cal

1491: P}[<_1,<_2, (\downarrow_i)_{i=0}^{k-1}]$ over ${\cal P}$, there

1492: exists an automaton $A_\varphi \in {\cal B}({\cal R}_k)$ over some

1493: $\Gamma(2^{\cal P})$ such that ${\cal M}(\varphi) = {\cal

1494: L}(A_\varphi)$.

1495: \end{description}

1496: 

1497: We first introduce some auxiliary predicates that can be easily

1498: defined in the monadic second-order logic over DULSs. Let $+ 1$ be

1499: a binary predicate such that $+1(x,y)$ if and only if $x$ and $y$

1500: belong to the coarsest domain and $y$ is the immediate successor

1501: of $x$. We will write $x+1 \in X$ for $\E y (+1(x,y) \And y \in

1502: X)$. Moreover, let ${\tt T}^0(x)$ be a shorthand for ``x belongs

1503: to the coarsest domain'', $0_0 \in X$ be a shorthand for ``the

1504: first element of the coarsest domain belongs to $X$'', and ${\tt

1505: Path}(X,x)$ be a shorthand for the formula stating that ``$X$ is a

1506: path rooted at $x$''.

1507: 

1508: Let us prove part (a) for $k=2$. The generalization to $k > 2$ is

1509: straightforward. Let $A = (Q,q_0,\Delta,F)$ be a ${\cal B}({\cal

1510: R}_2)$-automaton over $\Gamma(\Sigma)$ (finite subset of ${\cal

1511: R}_2$) accepting tree sequences in ${\cal S}({\cal T}_2(\Sigma))$.

1512: We produce a sentence $\varphi_A \in {\rm MSO}_{{\cal

1513: P}_\Sigma}[<_1,<_2, \proj{0},\proj{1}]$, that involves monadic

1514: predicates in ${\cal P}_\Sigma = \{P_a \sep a \in \Sigma\}$ and is

1515: interpreted over ${\cal S}({\cal T}_2(\Sigma))$, such that ${\cal

1516: L}(A) = {\cal M}(\varphi_A)$. We assume $Q = \{0, \ldots m\}$ and

1517: $q_0 = 0$. For every $Z \in \Gamma(\Sigma)$, let $Z =

1518: (Q_Z,q_{Z}^{0},\Delta_Z,\Gamma_Z)$ over $\Sigma$, with $Q_Z = \{0,

1519: \ldots m_Z\}$, $q_{Z}^{0} = 0$, and $\Gamma_Z =

1520: \{(L_{i}^{Z},U_{i}^{Z}) \sep 1 \leq i \leq r_Z\}$.

1521: 

1522: The ${\rm MSO}_{{\cal P}_\Sigma}[<_1,<_2, \proj{0},

1523: \proj{1}]$-sentence $\varphi_A$  that corresponds to the automaton

1524: $A$ basically encodes the combined acceptance condition for ${\cal

1525: B}({\cal R}_2)$-automata. The outermost part of the sentence

1526: expresses the existence of an accepting run over the coarsest

1527: layer of the tree sequence for the B\"uchi sequence automaton

1528: $A^\uparrow$. For all $i \in Q$, the second-order variable $X_i$

1529: denotes the set of positions of the run which are associated with

1530: the state $i$, while, for all $Z \in \Gamma(\Sigma)$ the monadic

1531: predicate $Q_Z$ denotes the set of positions of the run that are

1532: labeled with the Rabin tree automaton $Z$. The innermost part

1533: ${\tt RAC}(x,Z)$ captures the existence of an accepting run over

1534: the tree rooted at $x$ for the Rabin tree automaton $Z$. For $i

1535: \in Q_Z$, the second-order variable $Y_i$ denotes the set of

1536: positions of the run that are associated with state $i$. The

1537: sentence $\varphi_A$ is defined as follows:

1538: 

1539: \medskip

1540: \noindent $\begin{array}{l} (\E Q_Z)_{Z \in \Gamma(\Sigma)} (\E

1541: X_i)_{i=0}^{m}  (\bigwedge_{i=0}^{m} \A x (x \in X_i \Imp {\tt

1542: T}^0(x)) \And \\ \bigwedge_{Z \in \Gamma(\Sigma)} \A x (x \in Q_Z

1543: \Imp {\tt T}^0(x)) \And 0_0 \in X_0 \And \bigwedge_{i \neq j} \neg

1544: \E y (y \in X_i \And y \in X_j) \And \\ \A x ({\tt T}^0(x) \Imp

1545: \bigvee_{(i,Z,j) \in \Delta}(x \in X_i \And x \in Q_Z \And x+1 \in

1546: X_j)) \And \\ \bigvee_{i \in F} \A x ({\tt T}^0(x) \Imp \E y ({\tt

1547: T}^0(y) \And x <_1 y \And y \in X_i)) \And \\ \bigwedge_{Z \in

1548: \Gamma(\Sigma)} \A x (x \in Q_Z \Imp {\tt RAC}(x,Z)),

1549: \end{array}$

1550: 

1551: \medskip

1552: \noindent where ${\tt RAC}(x,Z)$ stands for:

1553: 

1554: \medskip

1555: \noindent $\begin{array}{l} (\E Y_i)_{i=0}^{m_Z} (\bigwedge_{i=

1556: 0}^{m_Z} \A y (y \in Y_i \Imp x \leq_2 y) \And x \in Y_0 \And

1557: \bigwedge_{i \neq j} \neg \E y (y \in Y_i \And y \in Y_j) \And \\

1558: \A y (x \leq_2 y \Imp \bigvee_{(i,a,j_0,j_1) \in \Delta_Z}(y \in

1559: Y_i \And y \in P_a \And  \proj{0}(y) \in Y_{j_0} \And \proj{1}(y)

1560: \in Y_{j_1})) \And \\ \A W ({\tt Path}(W,x) \Imp

1561: \bigvee_{i=0}^{r_Z} (\bigwedge_{j \in L_{i}^{Z}} \E u (u \in W

1562: \And \A v (v \in W \And u <_2 v \Imp v \not \in Y_j)) \And \\

1563: \bigvee_{j \in U_{i}^{Z}} \A u (u \in W \Imp \E v (v \in W \And u

1564: <_2 v \And v \in Y_j))))).

1565: \end{array}$

1566: 

1567: \medskip

1568: 

1569: We now prove part (b). Let ${\cal P} = \{P_1, \ldots P_n\}$. To

1570: simplify things, we prove our result for the theory ${\rm

1571: MSO}_{{\cal P}}[<_1,<_2, (\downarrow_i)_{i=0}^{k-1},+1]$ which can

1572: be easily shown to be equivalent to ${\rm MSO}_{{\cal P}}[<_1,<_2,

1573: (\downarrow_i)_{i=0}^{k-1}]$. Given a formula $\varphi \in {\rm

1574: MSO}_{{\cal P}}[<_1,<_2, (\downarrow_i)_{i=0}^{k-1},+1]$, that

1575: involves monadic predicates in ${\cal P}$ and is interpreted over

1576: ${\cal P}$-labeled tree sequences in ${\cal S}({\cal T}_k({\cal

1577: P}))$, we build an automaton $A_\varphi \in {\cal B}({\cal R}_k)$

1578: over some $\Gamma(2^{\cal P})$ and accepting in ${\cal S}({\cal

1579: T}_k({\cal P}))$ such that ${\cal L}(A_\varphi) = {\cal

1580: M}(\varphi)$.

1581: 

1582: As a first step, we show that the ordering relations $<_1$ and

1583: $<_2$ can actually be removed without reducing the expressiveness.

1584: We replace $x <_1 y$ by $${\tt T}^{0}(x) \And {\tt T}^{0}(y) \And

1585: \A X (x + 1 \in X \And \A z (z \in X \Imp z + 1 \in X) \Imp y \in

1586: X)),$$ and $x <_2 y$ by $$\A X ( \bigwedge_{i =0}^{k-1}

1587: \proj{i}(x) \in X \And \A z(z \in X \Imp \bigwedge_{i=0}^{k-1}

1588: \proj{i}(z) \in X) \Imp y \in X).$$ Hence, ${\rm MSO}_{\cal

1589: P}[<_1, <_2, (\proj{i})_{i= 0}^{k-1}, +1]$ is as expressive as

1590: ${\rm MSO}_{\cal P}[(\proj{i})_{i=0}^{k-1}, +1]$. Next, we

1591: introduce an expressively equivalent variant of ${\rm MSO}_{\cal

1592: P}[(\proj{i})_{i=0}^{k-1}, +1]$, denoted by ${\rm

1593: MSO}[(\proj{i})_{i = 0}^{k-1}, +1]$, which uses free set variables

1594: $X_i$ in place of predicate symbols $P_i$ and is interpreted over

1595: $\{0,1\}^n$-labeled tree sequences in ${\cal S}({\cal

1596: T}_k(\{0,1\}^n))$. The idea is to encode a set $X \subseteq {\cal

1597: P}$ with the string $i_1 \ldots i_n \in \{0,1\}^n$ such that, for

1598: $j = 1,\ldots,n$,  $i_j = 1$ if and only if $P_j \in X$. We now

1599: reduce ${\rm MSO}[(\proj{i})_{i=0}^{k-1}, +1]$ to a simpler

1600: formalism ${\rm MSO}_{0}[(\proj{i})_{i=0}^{k-1}, +1]$, where {\em

1601: only} second-order variables $X_i$ occur and atomic formulas are

1602: of the forms $X_i \subseteq X_j$  ($X_i$ is a subset of $X_j$),

1603: ${\tt Proj}_m(X_i,X_j)$, with $m = 0, \ldots, k-1$ ($X_i$ and

1604: $X_j$ are the singletons $\{x\}$ and $\{y\}$, respectively, and

1605: $\proj{m}(x) = y$), and ${\tt Succ}(X_i,X_j)$  ($X_i$ and $X_j$

1606: are the singletons $\{x\}$ and $\{y\}$, respectively, and $x + 1 =

1607: y$). This step is performed as in the proof of B\"uchi's Theorem.

1608: %

1609: \begin{figure}[t]

1610: \epsfxsize=1.5in \centerline{\epsfbox {atomic.eps}}

1611: \caption{Temporalized automata for atomic formulas.}

1612: \label{fig:atomic}

1613: \end{figure}

1614: %

1615: Finally, given a ${\rm MSO}_{0}[(\proj{i})_{i=0}^{k-1},

1616: +1]$-formula $\varphi(X_1, \ldots , X_n)$, we prove, by induction

1617: on the structural complexity of $\varphi$, that there exists a

1618: temporalized automaton $A_\varphi$ accepting in ${\cal S}({\cal

1619: T}_k(\{0,1\}^n))$ such that $\mc{M}(\varphi) = \mc{L}(A_\varphi)$.

1620: A corresponding automaton accepting in ${\cal S}({\cal T}_k({\cal

1621: P}))$ can be obtained in the obvious way. As for atomic formulas,

1622: let $\alpha_{i,j}$ be the Rabin tree automaton over $\{0,1\}^n$

1623: for $X_i \subseteq X_j$. The temporalized automaton for $X_i

1624: \subseteq X_j$ is depicted in Figure~\ref{fig:atomic} (top).

1625: Moreover, let $\zeta$ be the Rabin tree automaton over $\{0,1\}^n$

1626: that accepts the singleton set containing a tree labeled with

1627: $0^n$ everywhere, and let $\alpha_{i,j}^{m}$ be the Rabin tree

1628: automaton over $\{0,1\}^n$ for ${\tt Proj}_m(X_i,X_j)$. The

1629: temporalized automaton for ${\tt Proj}_m(X_i,X_j)$ is depicted in

1630: Figure~\ref{fig:atomic} (middle). Finally, let $\alpha_i$ be the

1631: Rabin tree automaton over $\{0,1\}^n$ that accepts the singleton

1632: set containing a tree labeled with $0^{i-1}10^{n-i}$ at the root,

1633: and labeled with $0^n$ elsewhere. The combined automaton for ${\tt

1634: Succ}(X_i,X_j)$ is depicted in Figure~\ref{fig:atomic} (bottom).

1635: The induction step immediately follows from the closure of ${\cal

1636: B}({\cal R}_k)$ automata under Boolean operations and projection.

1637: Closure under Boolean operations has been already shown; closure

1638: under projection can be argued as follows: given a ${\cal B}({\cal

1639: R}_k)$-automaton $A$, the corresponding projected ${\cal B}({\cal

1640: R}_k)$-automaton is obtained by simply projecting every Rabin

1641: automaton that labels some transition of $A$.

1642: \end{proof}

1643: 

1644: We can exploit infinite tree sequence automata to provide the

1645: (full) second-order theory of DULSs with an expressively complete

1646: and elementarily decidable temporal logic counterpart. First of

1647: all, it is well-known that ${\cal B} \leftrightarrows \qltl$ and

1648: ${\cal B} \leftrightarrows \eqltl$, as well as ${\cal R}_k

1649: \leftrightarrows \qdctls$ and ${\cal R}_k \leftrightarrows

1650: \eqdctls$~\cite{E90}. Since Rabin tree automata are closed under

1651: Boolean operations, Theorem~\ref{th:traexp} allows us to conclude

1652: that both $\tl{\qltl}{\qdctls} \leftrightarrows {\cal B}({\cal

1653: R}_k)$ and $\tl{\eqltl}{\eqdctls} \leftrightarrows {\cal B}({\cal

1654: R}_k)$\footnote{It is worth pointing out that the application of

1655: the partition step of Theorem~\ref{th:traexp} to temporal formulas

1656: in $\eqdctls$ generates formulas of the form $\neg \E Q_1 \ldots

1657: \E Q_n \varphi$, where $\varphi$ is a $\dctls$-formula, which do

1658: not belong to the language of $\eqdctls$, because such a language

1659: is not closed under negation. Nevertheless, formulas of the form

1660: $\neg \E Q_1 \ldots \E Q_n \varphi$ can be embedded into Rabin

1661: tree automata as well. The Rabin tree automaton for $\neg \E Q_1

1662: \ldots \E Q_n \varphi$ can indeed be obtained by taking the

1663: complementation of the projection, with respect to $Q_1, \ldots

1664: Q_n$, of the Rabin tree automaton for $\varphi$.}. By applying

1665: Theorem~\ref{th:expTSA}, we have that both $\tl{\qltl}{\qdctls}

1666: \leftrightarrows {\rm MSO}_{\cal P}[<_1,<_2,

1667: (\downarrow_i)_{i=0}^{k-1}]$ and $\tl{\eqltl}{\eqdctls}

1668: \leftrightarrows {\rm MSO}_{\cal P}[<_1,<_2,

1669: (\downarrow_i)_{i=0}^{k-1}]$. Such a result is summarized by the

1670: following theorem.

1671: 

1672: \begin{theorem}

1673: \thC{Expressiveness of $\tl{\qltl}{\qdctls}$ and

1674: $\tl{\eqltl}{\eqdctls}$} \label{th:expQTL} \noindent

1675: $\tl{\qltl}{\qdctls}$ and $\tl{\eqltl}{\eqdctls}$ are as

1676: expressive as ${\rm MSO}_{\cal P}[<_1,<_2,

1677: (\downarrow_i)_{i=0}^{k-1}]$, when interpreted over DULSs.

1678: \end{theorem}

1679: 

1680: Furthermore, since ${\rm MSO}_{\cal P}[<_1,<_2,

1681: (\downarrow_i)_{i=0}^{k-1}]$ is decidable, both

1682: $\tl{\qltl}{\qdctls}$ and $\tl{\eqltl}{\eqdctls}$ are decidable.

1683: The next theorem shows that $\tl{\eqltl}{\eqdctls}$ is {\em

1684: elementarily} decidable.

1685: 

1686: \begin{theorem}

1687: \thC{Complexity of $\tl{\eqltl}{\eqdctls}$} \label{th:compQTL}

1688: \noindent The satisfiability problem for $\tl{\eqltl}{\eqdctls}$

1689: over DULSs is in ELEMENTARY.

1690: \end{theorem}

1691: 

1692: \begin{proof}

1693: $\tl{\eqltl}{\eqdctls}$ can be decided by embedding it into ${\cal

1694: B}({\cal R}_k)$ automata (such an embedding can be accomplished

1695: following the approach outlined in the proof of

1696: Theorem~\ref{th:traexp}). $\eqltl$ can be elementarily embedded

1697: into B\"uchi sequence automata. Indeed, given an $\eqltl$-formula

1698: $\E Q_1 \ldots \E Q_n \varphi$, the $\ptl$-formula $\varphi$ can

1699: be converted into a B\"uchi sequence automaton $A_\varphi$ of size

1700: $O(2^{|\varphi|})$. A B\"uchi sequence automaton for $\E Q_1

1701: \ldots \E Q_n \varphi$ can be obtained by taking the projection of

1702: $A_\varphi$ with respect to letters $Q_1, \ldots, Q_n$, that is,

1703: by deleting letters $Q_1, \ldots, Q_n$ from the transitions of

1704: $A_\varphi$. The size of the resulting automaton is

1705: $O(2^{|\varphi|})$. Similarly, $\eqdctls$ formulas can be embedded

1706: into Rabin tree automata with a doubly exponential number of

1707: states and a singly exponential number of accepting pairs in the

1708: length of the formula. In particular, as already pointed out, a

1709: Rabin tree automaton for formulas of the form $\neg \E Q_1 \ldots

1710: \E Q_n \varphi$, which are generated by applying the partition

1711: step of Theorem~\ref{th:traexp} to $\eqdctls$ formulas, can be

1712: obtained by taking the complementation of the projection, with

1713: respect to $Q_1, \ldots Q_n$, of the Rabin tree automaton for

1714: $\varphi$. The resulting automaton has elementary size. Hence, any

1715: $\tl{\eqltl}{\eqdctls}$ formula can be converted into an

1716: equivalent ${\cal B}({\cal R}_k)$ automaton of elementary size.

1717: Since ${\cal B}({\cal R}_k)$ automata are elementarily decidable,

1718: we have the thesis.

1719: \end{proof}

1720: 

1721: We conclude the section by giving some examples of meaningful

1722: timing properties that can be expressed in (fragments of)

1723: $\tl{\eqltl}{\eqdctls}$ interpreted over DULSs. As a first

1724: example, consider the property `$P$ densely holds at some node

1725: $x$' meaning that there exists a path rooted at $x$ such that $P$

1726: holds at each node of the path (notice that such a property

1727: implies that, for every $i \geq 0$, there exists $y \in

1728: \downarrow^i(x)$ such that $P$ holds at $y$, where, for $i \geq

1729: 0$, $\downarrow^i(x)$ is the $i$-th layer of the tree rooted at

1730: $x$, but not vice versa). This property can be expressed in

1731: $\tl{\ptl}{\dctls}$ by the formula: $$\Diamond \op{E F E G}P.$$ As

1732: another example, the property `$P$ holds at the origin of every

1733: layer' (or, equivalently, `$P$ holds along the leftmost path of

1734: the first tree of the sequence') can be expressed in

1735: $\tl{\ptl}{\dctls}$ as follows: $$\op{E}(P \And \op{GX_0}P).$$ As

1736: a third example, the property `$P$ holds everywhere on every even

1737: tree' can be encoded in $\tl{\eqltl}{\dctls}$ as follows: $$\E Q(Q

1738: \And \Next \neg Q \And \Box(Q \IImp \Next \Next Q) \And \Box(Q

1739: \Imp \op{AG} P)).$$ Notice that such a property cannot be

1740: expressed in $\tl{\ptl}{\dctls}$, since, as it is well-known,

1741: $\ptl$ cannot express the property `$P$ holds on every even

1742: point'~\cite{W83}. As a last example, the property `$P$ holds

1743: everywhere on every even layer' can be encoded in

1744: $\tl{\ptl}{\eqdctls}$ as follows: $$\Box \E Q(Q \And \op{AX} \neg

1745: Q \And \op{A G}(Q \IImp \op{AXAX} Q) \And \op{AG}(Q \Imp P)).$$

1746: Notice that also this property cannot be expressed in

1747: $\tl{\ptl}{\dctls}$.

1748: 

1749: Unfortunately, things are not always that easy. As an example, the

1750: property `$P$ holds at exactly one node' can be easily encoded in

1751: (the first-order fragment of) ${\rm MSO}_{\cal P}[<_1,$ $<_2,

1752: (\downarrow_i)_{i=0}^{k-1}]$ by the formula: $\E x (x \in P \And

1753: \A y(y \neq x \Imp y \not \in P))$, while it is not easy at all to

1754: express it in $\tl{\eqltl}{\eqdctls}$. Moreover, since ${\rm

1755: MSO}_{\cal P}[<_1,<_2, (\downarrow_i)_{i=0}^{k-1}]$ is

1756: nonelementarily decidable, while $\tl{\eqltl}{\eqdctls}$ is

1757: elementarily decidable, the translation $\tau$ of ${\rm MSO}_{\cal

1758: P}[<_1,$ $<_2, (\downarrow_i)_{i=0}^{k-1}]$ formulas into

1759: $\tl{\eqltl}{\eqdctls}$ formulas is nonelementary. This means

1760: that, for every $n \in \mathbb{N}$, there exists an ${\rm

1761: MSO}_{\cal P}[<_1,<_2, (\downarrow_i)_{i=0}^{k-1}]$-formula

1762: $\varphi$ such that the length of $\tau(\varphi)$ is greater than

1763: $\kappa(n, |\varphi|)$ (an exponential tower of height $n$).

1764: 

1765: \subsection{Upward unbounded layered structures}

1766: \label{sec:UULS}

1767: 

1768: \begin{figure}[t]

1769: \begin{center}

1770: {\begin{picture}(250,90) \multiput(0,50)(80,0){4}{\circle*{3}}

1771: \multiput(80,50)(80,0){3}{\line(0,-1){20}}

1772: \multiput(80,30)(80,0){3}{\circle*{3}}

1773: \multiput(160,30)(80,0){2}{\line(-1,-1){20}}

1774: \multiput(160,30)(80,0){2}{\line(1,-1){20}}

1775: \multiput(140,10)(40,0){4}{\circle*{3}}

1776: \multiput(220,10)(40,0){2}{\line(-1,-1){10}}

1777: \multiput(220,10)(40,0){2}{\line(1,-1){10}}

1778: \multiput(210,0)(20,0){4}{\circle*{3}} \put(0,50){\line(1,0){240}}

1779: \put(260,50){$\ldots$} \put(0,60){$0_0$} \put(80,60){$0_1$}

1780: \put(160,60){$0_2$} \put(240,60){$0_3$} \put(85,30){$1_0$}

1781: \put(165,30){$1_1$} \put(245,30){$1_2$} \put(148,10){$2_0$}

1782: \put(188,10){$3_0$} \put(228,10){$2_1$} \put(268,10){$3_1$}

1783: \put(208,-15){$4_0$} \put(228,-15){$5_0$} \put(248,-15){$6_0$}

1784: \put(268,-15){$7_0$}

1785: \end{picture}}

1786: \vspace{1cm} \caption{\label{fig:treeseq3} Mapping an UULS into an

1787: increasing tree sequence.}

1788: \end{center}

1789: \end{figure}

1790: 

1791: We start by giving an alternative characterization of UULSs in

1792: terms of tree sequences. To this end, we need to introduce the

1793: notions of almost $k$-ary tree and of increasing tree sequence. An

1794: {\em almost $k$-ary finite tree} is a complete finite tree whose

1795: root has exactly $k-1$ sons $0, \ldots, k-2$, each of them is the

1796: root of a complete finite $k$-ary tree. Let ${\cal H}_k({\cal P})$

1797: be the set of $\cal P$-labeled almost $k$-ary finite trees. A

1798: ${\cal P}$-labeled {\em increasing $k$-ary tree sequence} (ITS,

1799: for short) is a tree sequence such that, for every $i \in

1800: \mathbb{N}$, the $i$-th tree of the sequence is a ${\cal

1801: P}$-labeled almost $k$-ary tree of height $i$ (cf.\

1802: Figure~\ref{fig:treeseq3}). A ${\cal P}$-labeled ITS can be

1803: represented as a temporalized model $(\mathbb{N},<,g)$ such that,

1804: for every $i \in \mathbb{N}$, $g(i)$ is the $i$-th tree of the

1805: sequence. Let $ITS_k({\cal P})$ be the set of ${\cal P}$-labeled

1806: $k$-ary ITSs. It is worth noting that $ITS_k({\cal P})$ is {\em

1807: not} the class ${\cal H}_k({\cal P}$ of temporalized models

1808: embedding almost $k$-ary finite trees into infinite sequences: an

1809: increasing tree sequence is a particular sequence of almost

1810: $k$-ary finite trees, but a sequence of almost $k$-ary finite

1811: trees is not necessary increasing, and thus $ITS_k({\cal P})

1812: \subsetneq {\cal S}({\cal H}_k({\cal P}))$.

1813: 

1814: It is not difficult to show that a ${\cal P}$-labeled UULS

1815: corresponds to a ${\cal P}$-labeled ITS, and vice versa. As

1816: already pointed out, an UULS can be viewed as an infinite complete

1817: $k$-ary tree generated from the leaves. The corresponding tree

1818: sequence can be obtained starting from the first point of the

1819: finest layer of the UULS and climbing up along the leftmost path

1820: of the structure. The $i$-th tree in the sequence is obtained by

1821: taking the tree rooted at the $i$-th point of the leftmost path,

1822: and by deleting from it the subtree rooted at the leftmost son of

1823: its root. More precisely, let $t$ be a $k$-ary UULS. For every

1824: node $x$ in $t$, we define $t_x$ to be the finite complete $k$-ary

1825: tree rooted at $x$. For every $i \geq 0$, let $\hat{t}_{0_i}$ be

1826: the almost $k$-ary finite tree obtained from $t_{0_i}$ by

1827: deleting, whenever $i>0$, the subtree $t_{0_{i-1}}$ from it. The

1828: ITS $(\mathbb{N},<,g)$ associated with the UULS $t$ is obtained by

1829: defining, for every $i \geq 0$, $g(i) = \hat{t}_{0_i}$. The

1830: embedding of a binary UULS into a binary ITS is depicted in

1831: Figure~\ref{fig:treeseq3}. Similarly, ITSs can be reinterpreted in

1832: terms of UULSs.

1833: 

1834: On the basis of such a correspondence between UULSs and ITSs, we

1835: can use temporalized logics $\tl{\logic{T_1}}{\logic{T_2}}$, where

1836: $\logic{T_1}$ is a linear time logic and $\logic{T_2}$ is a

1837: branching time logic, to express properties of UULSs. More

1838: precisely, we interpret $\tl{\logic{T_1}}{\logic{T_2}}$ over

1839: ${\cal S}({\cal H}_k({\cal P}))$, but, since we are interested in

1840: increasing tree sequences, we study the logical properties of

1841: $\tl{\logic{T_1}}{\logic{T_2}}$, such as expressiveness and

1842: decidability, with respect to the proper subset $ITS_k({\cal P})$.

1843: Temporalized automata $\tl{{\cal A}_1}{{\cal A}_2}$ over UULSs can

1844: be defined in a similar way. Once again, we consider automata in

1845: $\tl{{\cal A}_1}{{\cal A}_2}$ accepting in ${\cal S}({\cal

1846: H}_k(\Sigma))$, but, since we are interested in increasing tree

1847: sequences, we study the relevant properties of $\tl{{\cal

1848: A}_1}{{\cal A}_2}$, such as closure under Boolean operations,

1849: expressiveness, and decidability, with respect to the proper

1850: subset $ITS_k(\Sigma)$. In the following, we will focus on the

1851: class ${\cal B}({\cal C}_k)$ of temporalized automata embedding

1852: almost $k$-ary finite tree automata into B\"uchi sequence

1853: automata. We call automata in ${\cal B}({\cal C}_k)$ {\em finite

1854: tree sequence automata}.

1855: 

1856: Since both ${\cal B}$ and ${\cal C}_k$ are effectively closed

1857: under Boolean operations and decidable, Theorems~\ref{th:traclo}

1858: and~\ref{th:tradec} allows us to conclude that ${\cal B}({\cal

1859: C}_k)$ is effectively closed under Boolean operations and

1860: decidable. We show that ${\cal B}({\cal C}_k)$-automata are closed

1861: under Boolean operations over the set $ITS_k(\Sigma)$ as well. Let

1862: $A,B \in {\cal B}({\cal C}_k)$. We show that:

1863: 

1864: \begin{itemize}

1865: \item

1866: there exists $C \in {\cal B}({\cal C}_k)$ such that $${\cal L}(C)

1867: \cap ITS_k(\Sigma) = ITS_k(\Sigma) \setminus {\cal L}(A) \ \

1868: (complementation);$$

1869: \item

1870: there exists $C \in {\cal B}({\cal C}_k)$ such that $${\cal L}(C)

1871: \cap ITS_k(\Sigma) = ({\cal L}(A) \cup {\cal L}(B)) \cap

1872: ITS_k(\Sigma) \ \ (union);$$

1873: \item

1874: there exists $C \in {\cal B}({\cal C}_k)$ such that $${\cal L}(C)

1875: \cap ITS_k(\Sigma) = ({\cal L}(A) \cap {\cal L}(B)) \cap

1876: ITS_k(\Sigma) \ \ (intersection).$$

1877: \end{itemize}

1878: 

1879: As it can be easily checked, it suffices to set $C = \overline{A}$

1880: in case of complementation, $C = A \cup B$ in the case of union,

1881: and $C = A \cap B$ in the case of intersection.

1882: 

1883: The following theorem relates finite tree sequence automata to the

1884: monadic second-order theory of UULSs.

1885: 

1886: \begin{theorem}

1887: \label{th:expkFTSA} \thC{Expressiveness of finite tree sequence

1888: automata} \noindent Finite tree sequence automata are as

1889: expressive as the monadic second-order theory of UULSs.

1890: \end{theorem}

1891: 

1892: 

1893: \begin{proof}

1894: 

1895: The proof is quite similar to that of Theorem~\ref{th:expTSA}, and

1896: thus we only sketch its main steps. We split the proof in two

1897: parts:

1898: 

1899: \begin{description}

1900: \item{(a)}

1901: we first show that, for every automaton $A \in {\cal B}({\cal

1902: C}_k)$ over $\Gamma(\Sigma)$, there exists a formula $\varphi_A

1903: \in {\rm MSO}_{{\cal P}_\Sigma}[<, (\downarrow_i)_{i=0}^{k-1}]$

1904: over ${\cal P}_\Sigma = \{P_a \sep a \in \Sigma\}$ such that

1905: ${\cal L}(A) \cap ITS_k(\Sigma) = {\cal M}(\varphi_A)$;

1906: \item{(b)}

1907: then we show that, for every formula $\varphi \in {\rm MSO}_{\cal

1908: P}[<, (\downarrow_i)_{i=0}^{k-1}]$, there exists an automaton

1909: $A_\varphi \in {\cal B}({\cal C}_k)$ over some $\Gamma(2^{\cal

1910: P})$ such that ${\cal M}(\varphi) = {\cal L}(A_\varphi) \cap

1911: ITS_k({\cal P})$.

1912: \end{description}

1913: 

1914: The embedding of automata into formulas is performed by encoding

1915: the combined acceptance condition for ${\cal B}({\cal

1916: C}_k)$-automata into ${\rm MSO}_{\cal P}[<,

1917: (\downarrow_i)_{i=0}^{k-1}]$. The B\"uchi acceptance condition

1918: have to be implemented over the leftmost path of the structure,

1919: and the finite tree automata acceptance condition have to be

1920: constrained to hold over almost $k$-ary trees rooted at nodes in

1921: the leftmost path of the structure. The embedding of formulas into

1922: automata takes advantage of the closure properties of ${\cal

1923: B}({\cal C}_k)$-automata over UULSs.

1924: \end{proof}

1925: 

1926: We can exploit finite tree sequence automata to provide the (full)

1927: second-order theory of UULSs with an expressively complete

1928: temporal logic counterpart. We know that ${\cal B}

1929: \leftrightarrows \qltl$ and ${\cal B} \leftrightarrows \eqltl$,

1930: and that ${\cal C}_k \leftrightarrows \qdctls$ and ${\cal C}_k

1931: \leftrightarrows \eqdctls$. Since almost $k$-ary finite tree

1932: automata are closed under Boolean operations,

1933: Theorem~\ref{th:traexp} allows us to conclude that that

1934: $\tl{\qltl}{\qdctls} \leftrightarrows {\cal B}({\cal C}_k)$ and

1935: $\tl{\eqltl}{\eqdctls} \leftrightarrows {\cal B}({\cal C}_k)$ over

1936: infinite sequences of almost $k$-ary finite trees. Since

1937: increasing $k$-ary tree sequences are infinite sequences of almost

1938: $k$-ary trees, the above equivalences hold over increasing $k$-ary

1939: tree sequences as well. From Theorem~\ref{th:expkFTSA}, we have

1940: that $\tl{\qltl}{\qdctls} \leftrightarrows {\rm MSO}_{\cal

1941: P}[<_{pre}, (\downarrow_i)_{i=0}^{k-1}]$ and

1942: $\tl{\eqltl}{\eqdctls} \leftrightarrows {\rm MSO}_{\cal

1943: P}[<_{pre}, (\downarrow_i)_{i=0}^{k-1}]$. Such a result is

1944: summarized by the following theorem.

1945: 

1946: \begin{theorem}

1947: \thC{Expressiveness of $\tl{\qltl}{\qdctls}$ and

1948: $\tl{\eqltl}{\eqdctls}$} \label{th:expQTL-UULS} \noindent

1949: $\tl{\qltl}{\qdctls}$ and $\tl{\eqltl}{\eqdctls}$ are as

1950: expressive as ${\rm MSO}_{\cal P}[<_{pre}, (\downarrow_i)_{i =

1951: 0}^{k-1}]$, when interpreted over UULSs.

1952: \end{theorem}

1953: 

1954: The (nonelementary) decidability of $\tl{\qltl}{\qdctls}$ and

1955: $\tl{\eqltl}{\eqdctls}$ immediately follows from that of ${\rm

1956: MSO}_{\cal P}[<_{pre}, (\downarrow_i)_{i = 0}^{k - 1}]$ over

1957: UULSs. A natural question arises at this point: is

1958: $\tl{\eqltl}{\eqdctls}$ elementary decidable as in the case of

1959: DULSs? In order to answer this question, we study the decidability

1960: and complexity of the emptiness problem for finite tree sequence

1961: automata over increasing $k$-ary tree sequences. Such a problem

1962: can be formulated as follows: given an automaton $A \in {\cal

1963: B}({\cal C}_k)$, is there an increasing $k$-ary tree sequence

1964: accepted by $A$? (Equivalently, does ${\cal L}(A) \cap

1965: ITS_k(\Sigma) \neq \emptyset$?) The (nonelementary) decidability

1966: of such a problem immediately follows from

1967: Theorem~\ref{th:expkFTSA}, since, given an automaton $A$, we can

1968: build an equivalent monadic formula $\varphi_A$ and check its

1969: satisfiability over UULSs. In the following, we give a necessary

1970: and sufficient condition that solves the problem in {\em

1971: elementary} time.

1972: 

1973: \medskip

1974: 

1975: Let $A = (Q,q_0,\Delta,F)$ be an automaton in ${\cal B}({\cal

1976: C}_k)$ over the alphabet $\Gamma(\Sigma)$ (finite subset of ${\cal

1977: C}_k$). Clearly, ${\cal L}(A) \neq \emptyset$ is necessary for

1978: ${\cal L}(A) \cap ITS_k(\Sigma) \neq \emptyset$. However, it is

1979: not sufficient. By definition of combined acceptance condition for

1980: $A$, we have that ${\cal L}(A) \neq \emptyset$ if and only if

1981: there is a finite sequence $q_0, q_1, \ldots q_m$ of distinct

1982: states in $Q$, a finite sequence $X_0, X_1, \ldots X_m$ of ${\cal

1983: C}_k$-automata and $j \in \{0, \ldots m\}$ such that:

1984: 

1985: \begin{enumerate}

1986: \item $\Delta(q_i,X_i,q_{i+1})$, for every $i=0, \ldots m-1$,

1987: and $\Delta(q_m,X_m,q_j)$;

1988: \item $q_j \in F$;

1989: \item ${\cal L}(X_i) \neq \emptyset$, for every $i=0, \ldots m$

1990: \end{enumerate}

1991: 

1992: To obtain a necessary and sufficient condition for ${\cal L}(A)

1993: \cap ITS_k(\Sigma) \neq \emptyset$, we have to strengthen

1994: condition (3) as follows. Let $T^{i}_{k}(\Sigma)$ be the set of

1995: almost $k$-ary finite trees of height $i$:

1996: 

1997: \begin{description}

1998: \item{3'.}

1999: (3'a) ${\cal L}(X_i) \cap T^{i}_{k}(\Sigma) \neq \emptyset$, for

2000: every $i=0, \ldots j-1$, and (3'b) ${\cal L}(X_i) \cap T^{i + y

2001: \cdot l }_{k}(\Sigma) \neq \emptyset$, for every $i=j, \ldots m$

2002: and $y \geq 0$, where $l = m-j+1$.

2003: \end{description}

2004: 

2005: The conjunction of conditions (1,2,3') is a necessary and

2006: sufficient condition for ${\cal L}(A) \cap ITS_k(\Sigma) \neq

2007: \emptyset$.  We show that conditions (1,2,3') are elementarily

2008: decidable. Clearly, there are elementarily many runs in $A$

2009: satisfying conditions (1,2).  The following nontrivial

2010: Lemma~\ref{lm:cond4} shows that condition 3' is elementarily

2011: decidable.

2012: 

2013: \begin{lemma}\label{lm:cond4}

2014: \noindent Let $X$ be a almost $k$-ary finite tree automaton, and

2015: $a,l \geq 0$. Then, the problem ${\cal L}(X) \cap T^{a + y \cdot l

2016: }_{k}(\Sigma) \neq \emptyset$, for every $y \geq 0$, is

2017: elementarily decidable.

2018: \end{lemma}

2019: 

2020: \begin{proof}

2021: 

2022: Let $X = (Q,q_0,\Delta,F)$ over $\Gamma(\Sigma)$. If $l=0$, then

2023: the problem reduces to checking ${\cal L}(X) \cap

2024: T^{a}_{k}(\Sigma) \neq \emptyset$, for some $a \geq 0$. For every

2025: $a \geq 0$, the set $T^{a}_{k}$ is finite and hence regular. Since

2026: almost $k$-ary finite tree automata are elementarily closed under

2027: Boolean operations and elementarily decidable, we conclude that in

2028: this case the condition is elementarily effective.

2029: 

2030: Suppose now  $l > 0$. For the sake of simplicity, we first give

2031: the proof for finite {\em sequence} automata, and then we discuss

2032: how to modify it to cope with the case of almost $k$-ary finite

2033: tree automata. Hence, let $X$ be a finite sequence automaton. We

2034: have to give an elementarily effective procedure that checks

2035: whether $X$ recognizes at least one sequence of length $a$, at

2036: least one of length $a+l$, at least one of length $a+2l$, and so

2037: on. Without loss of generality, we may assume that the set of

2038: final states of $X$ is the singleton containing $q_{fin} \in Q$.

2039: Hence, the problem reduces to check, for every $y \geq 0$, the

2040: existence of a path from $q_0$ to $q_{fin}$ of length $a + y \cdot

2041: l$ in the state-transition graph associated with $X$. We thus need

2042: to solve the following problem of Graph Theory, which we call the

2043: {\em Periodic Path Problem} (PPP for short):

2044: 

2045: \begin{quote}

2046: Given a finite directed graph $G = (N,E)$, two nodes $q_1,q_2 \in

2047: N$, and two natural numbers $a,l \geq 0$, the question is: for

2048: every $y \geq 0$, is there a path in $G$ from $q_1$ to $q_2$ of

2049: length $a + y \cdot l$?

2050: \end{quote}

2051: 

2052: In the following, we further reduce the PPP to a problem of Number

2053: Theory. Let $\Pi_{q_1,q_2}(G)$ be the set of paths from $q_1$ to

2054: $q_2$ in the graph $G$. Given $\pi \in \Pi_{q_1,q_2}(G)$, we

2055: denote by $\pi^\circlearrowleft$ the path obtained by eliminating

2056: cyclic subpaths from $\pi$. That is, if $\pi$ is acyclic, then

2057: $\pi^\circlearrowleft = \pi$. Else, if $\pi = \alpha q' \beta q'

2058: \gamma$, then $\pi^\circlearrowleft = \alpha^\circlearrowleft q'

2059: \gamma^\circlearrowleft$. Let $\sim_{q_1,q_2}$ be the relation on

2060: $\Pi_{q_1,q_2}(G)$ such that $\pi_1 \sim_{q_1,q_2} \pi_2$ if and

2061: only if $\pi_{1}^{\circlearrowleft} = \pi_{2}^{\circlearrowleft}$.

2062: Note that $\sim_{q_1,q_2}$ is an equivalence relation of finite

2063: index. For every equivalence class $[\pi]_{\sim_{q_1,q_2}}$, we

2064: need a formula expressing the length of a generic path in the

2065: class. Note that every path in $[\pi]_{\sim_{q_1,q_2}}$ differs

2066: from any other path in the same class only for the presence of

2067: some cyclic subpaths. More precisely, let $\mu$ be the shortest

2068: path in $[\pi]_{\sim_{q_1,q_2}}$, let $C_1, \ldots C_n$ be the

2069: cycles intersecting $\pi$, and let $w_1, \ldots w_n$ be their

2070: respective lengths. Note that $\mu$ does not cycle through any

2071: $C_i$. Every path in $[\pi]_{\sim_{q_1,q_2}}$ starts from $q_1$,

2072: cycles an arbitrary number of times (possibly zero) through every

2073: $C_i$, and reaches $q_2$. It is easy to see that the length of an

2074: arbitrary path $\sigma \in [\pi]_{\sim_{q_1,q_2}}$ is given by the

2075: parametric formula: $$ |\sigma| = |\mu| + \sum_{i=1}^{n} x_i \cdot

2076: w_i,$$ where $x_i \geq 0$ in the number of times the path $\sigma$

2077: cycles through $C_i$.

2078: 

2079: \noindent Let $[\pi_1]_{\sim_{q_1,q_2}}, \ldots,

2080: [\pi_m]_{\sim_{q_1,q_2}}$ be the equivalence classes of

2081: $\sim_{q_1,q_2}$. For every $j = 1, \ldots m$, let $\mu_j$ be the

2082: shortest path in $[\pi_j]_{\sim_{q_1,q_2}}$, let $C_{1}^{j},

2083: \ldots C_{n}^{j}$ be the the cycles intersecting $\pi_j$, and let

2084: $w_{1}^{j}, \ldots w_{n}^{j}$ be their respective lengths.

2085: Moreover, let $$Y_j = \{y \geq 0 \sep \E x_{1}, \ldots x_{n} \geq

2086: 0 \, (|\mu_j| + \sum_{i=1}^{n} x_i \cdot w_{i}^{j} = a + y \cdot

2087: l)\}.$$ The PPP reduces to the following problem of Number Theory:

2088: 

2089: \begin{quote}

2090: Do the sets $Y_1, \ldots Y_m$ cover the natural numbers? That is,

2091: does $\bigcup_{j=1}^{m} Y_j = \mathbb{N}$?

2092: \end{quote}

2093: 

2094: We now solve the latter problem.  Let $w_i \geq 0$, for $i = 1,

2095: \ldots n$. We are interested in the form of the set $S =

2096: \{\sum_{i=1}^{n} x_i \cdot w_i \sep x_i \geq 0\}$. Let $W = (w_1,

2097: \ldots w_n)$ and let $d = GCD(W)$ (the greatest common divisor of

2098: $\{w_1, \ldots, w_n\}$). We distinguish the cases $d = 1$ and $d

2099: \neq 1$. If $d = 1$, then it is easy to see that: $$S = E \cup \{j

2100: \sep j \geq k\},$$ where $E$ is a finite set of {\em exceptions}

2101: such that $max(E) < k$, and $k = (w_r-1) \cdot (w_s-1)$, with $w_r

2102: = min(W)$ (the minimum of $\{w_1, \ldots w_n\}$) and $w_s = min(W

2103: \setminus w_{r})$. If $d \neq 1$, then consider the set $S' =

2104: \{\sum_{i=1}^{n} x_i \cdot w_i/d \sep x_i \geq 0\}$. Clearly,

2105: $GCD(w_1/d, \ldots w_n/d) = 1$ and hence, as above, $S' = E' \cup

2106: \{j \sep j \geq k'\}$ for some finite set $E'$ and some $k' \in

2107: \mathbb{N}$. Therefore, in this case, $$S = E' \cdot d \cup \{j

2108: \sep j \geq k' \cdot d \And d \ \tt{DIV} \ j\},$$ where $d \

2109: \tt{DIV} \ j$ means that $d$ is a divisor of $j$.

2110: 

2111: Summing up, in any case, the set $S$ can be described as follows:

2112: $$S = E \cup \{k + j \cdot d \sep j \in \mathbb{N}\},$$ for some

2113: finite (computable) set $E$, some (computable) $k \in \mathbb{N}$,

2114: and $d = GCD(W)$. In other words, the set $S$ is the union of a

2115: finite and computable set of exceptions and an arithmetic

2116: progression.

2117: 

2118: Now we consider the equation $\sum_{i=1}^{n} x_{i} \cdot w_i = y

2119: \cdot l$. Our aim is to describe the set $Y = \{y \geq 0 \sep \E

2120: x_{1}, \ldots x_{n} \geq 0 \, (\sum_{i=1}^{n} x_{i} \cdot w_i = y

2121: \cdot l)\}$ in a similar way. Let $e = GCD(d,l)$, $l = l' \cdot e$

2122: and $d = d' \cdot e$. We have that:

2123: 

2124: \medskip

2125: 

2126: $\begin{array}{lll} y \in Y & \mbox{ iff } & \\ y \cdot l \in S &

2127: \mbox{ iff } & \\ y \cdot l \in E \Or y \cdot l \geq k \And d \

2128: \tt{DIV} \ y \cdot l & \mbox{ iff } & \\ y \cdot l \in E \Or y

2129: \geq \lceil k/l \rceil \And d' \cdot e \ \tt{DIV} \ y \cdot l'

2130: \cdot e  & \mbox{ iff } & \\ y \cdot l \in E \Or  y \geq \lceil

2131: k/l \rceil \And d' \ \tt{DIV} \ y

2132: \end{array}$

2133: 

2134: \medskip

2135: 

2136: Therefore, the set $Y$ is the union of a finite and computable set

2137: and an arithmetic progression, i.e., $$Y = E' \cup \{k' + j \cdot

2138: d' \sep j \in \mathbb{N}\},$$ for some finite (computable) set

2139: $E'$, some (computable) $k' \in \mathbb{N}$, and $d' = d / GCD(d,$

2140: $l)$. The set $Y = \{y \geq 0 \sep \E x_{1}, \ldots x_{n} \geq 0

2141: \, (\sum_{i=1}^{n} x_{i} \cdot w_i = a + y \cdot l)\}$, with $a

2142: \in \mathbb{N}$, can be described in the same way.

2143: 

2144: We have shown that, for $i = 1, \ldots, m$, every $Y_i$ has the

2145: form $E_i \cup \{k_i + y \cdot d_i \sep y \geq 0\}$ for some

2146: finite $E_i$, and some $k_i,d_i \in \mathbb{N}$. We now give a

2147: solution to the problem $\bigcup_{i=1}^{m} Y_i = \mathbb{N}$. Let

2148: $k_r = min \{k_1, \ldots, k_m\}$ and $D = LCM(d_1, \ldots, d_m)$

2149: (the least common multiple of $\{d_1, \ldots, d_m\}$). The

2150: algorithm works as follows: for every $k < k_r$, we check whether

2151: $k \in Y_i$ for some $i = 1, \ldots, m$. If this is not the case,

2152: the problem has no solution. Otherwise, we verify whether, for

2153: every $j = 0, \ldots, D-1$, $k_r + j \in Y_i$ for some $i = 1,

2154: \ldots, m$. If this is the case, then we have a solution,

2155: otherwise, there is no solution. Note that a solution can be

2156: described in terms of an ultimately periodic word $w = uv^\omega$,

2157: with $u,v \in \{1, \ldots m\}^*$, such that, for every $i \geq 0$,

2158: $w(i) = j$ means that a path from $q_1$ to $q_2$ in the graph $G$

2159: belongs to the $j$-th equivalence class

2160: $[\pi_j]_{\sim_{q_1,q_2}}$.

2161: 

2162: The above algorithm solves the periodic path problem in doubly

2163: exponential time in the number $n$ of nodes of the graph $G$. The

2164: number of equivalence classes of the relation $\sim_{q_{1},q_{2}}$

2165: over the set of paths from $q_{1}$ to $q_{2}$ in $G$ may be

2166: exponential in $n$. Thus, we have $m$ sets $Y_1, \ldots, Y_m$,

2167: each one associated with a relevant equivalence class, and $m =

2168: {\cal O}(2^n)$. Every set $Y_i$ can be represented in polynomial

2169: time as $E_i \cup \{k_i + y \cdot d_i \sep y \geq 0\}$ for some

2170: finite $E_i$, and some $k_i,d_i \in \mathbb{N}$. Note that the

2171: cardinality of $E_i$ is bounded by $k_i$, $k_i = {\cal O}(n^2)$,

2172: and $d_i = {\cal O}(n)$. The final step of the procedure makes

2173: $k_0 + D$ membership tests with respect to some set $Y_i$, where

2174: $k_0 = min \{d_1, \ldots d_m\}$, and $D =  LCM(d_1, \dots d_m)$.

2175: Each test is performed in ${\cal O}(1)$. Moreover, $D$ is bounded

2176: by ${d_{0}}^{m}$, where $d_0 = max \{d_1, \ldots d_m\}$, and hence

2177: $D = {\cal O}(2^{2^n})$. Hence, the procedure works in doubly

2178: exponential time.

2179: 

2180: The general case of finite trees is similar. Let $X$ be a finite

2181: almost $k$-ary tree automaton. A path from $q_1$ to $q_2$

2182: corresponds to a run of $X$ such that the run tree is complete and

2183: $k$-ary, the root of the run tree is labeled with state $q_1$ and

2184: the leaves of the run tree are labeled with state $q_2$. A cycle

2185: is a path from $q$ to $q$. The problem is to find, for every $y

2186: \geq 0$, a path from the initial state $q_0$ to the final state

2187: $q_{fin}$ of length $a + y \cdot l$. The rest of the proof follows

2188: the same reasoning path of the proof for sequence automata.

2189: \end{proof}

2190: 

2191: From Lemma \ref{lm:cond4}, it follows that, given a ${\cal

2192: B}({\cal C}_k)$-automaton $A$, we have an algorithm to solve the

2193: problem ${\cal L}(A) \cap ITS_k(\Sigma) \neq \emptyset$ in doubly

2194: exponential time in the size of $A$.

2195: 

2196: 

2197: \begin{theorem}

2198: \label{th:deckFTSA} \noindent The emptiness problem for finite

2199: tree sequence automata over UULSs is in 2EXPTIME.

2200: \end{theorem}

2201: 

2202: Since $\tl{\eqltl}{\eqdctls}$ formulas can be elementarily

2203: converted into ${\cal B}({\cal C}_k)$ automata, we have the

2204: desired result.

2205: 

2206: \begin{theorem}

2207: \label{th:compTL-UULS} \thC{Complexity of $\tl{\eqltl}{\eqdctls}$}

2208: \noindent The satisfiability problem for $\tl{\eqltl}{\eqdctls}$

2209: over UULSs is in ELEMENTARY.

2210: \end{theorem}

2211: 

2212: We conclude the section by giving some examples of meaningful

2213: timing properties that can be expressed in (fragments of)

2214: $\tl{\eqltl}{\eqdctls}$ interpreted over UULSs. As a first

2215: example, consider the property `$P$ holds at every point of the

2216: finest layer $T^0$ whose distance from the origin of the layer

2217: $0_0$ is a power of two ($1_0, 2_0, 4_0, 8_0$, and so on)' over a

2218: binary UULS. Such a property can be expressed in

2219: $\tl{\ptl}{\dctls}$ as follows: $$\Next \Box \, \op{E X_1}

2220: \op{G}((\op{X} {\tt true} \Imp \op{X_0} {\tt true}) \And (\neg

2221: \op{X} {\tt true} \Imp P)).$$ Notice that the property `$P$ holds

2222: on every point $2^i$, with $i \in \mathbb{N}$' cannot be expressed

2223: in $\qltl$. As a second example, the property `$P$ holds on every

2224: even point of the leftmost path' can be expressed in

2225: $\tl{\eqltl}{\dctls}$ as follows: $$\E Q(Q \And \Next \neg Q \And

2226: \Box(Q \IImp \Next \Next Q) \And \Box(Q \Imp P)).$$ As already

2227: pointed out, this property cannot be expressed in

2228: $\tl{\ptl}{\dctls}$, since $\ptl$ cannot express the property `$P$

2229: holds on every even point'~\cite{W83}.

2230: 

2231: As in the case of DULSs, there are some natural properties of

2232: UULSs that cannot be easily captured in $\tl{\eqltl}{\eqdctls}$.

2233: As an example, it is not easy to express the property `$P$ holds

2234: on every even point of the finest domain $T^0$'.

2235: 

2236: \section{The specification of a high voltage station}

2237: \label{sec:exa}

2238: 

2239: In this section, we exemplify the concrete use of temporalized

2240: logics as specification formalisms by providing (an excerpt of)

2241: the specification of a supervisor that automates the activities of

2242: a High Voltage (HV) station devoted to the end user distribution

2243: of energy generated by power plants \cite{M96}. We first show how

2244: relevant timing properties of such a system can be expressed in

2245: monadic second-order languages, and then we give their simpler

2246: temporalized logic formulations.

2247: 

2248: Each HV station is composed of bays, connecting generation units

2249: to the distribution line. A bay consists of circuit breakers and

2250: insulators. They are both switches, but an expensive circuit

2251: breaker can interrupt current in a very short time (50 millisecond

2252: or even less), while a cheap insulator is not able to interrupt a

2253: flowing current and it has a switching time of a few seconds. Let

2254: us consider a simple HV station consisting of two bars {\tt b1}

2255: and {\tt b2} connected to different power units, a distribution

2256: line {\tt l}, and two bays {\tt pb} (parallel bay) and {\tt lb}

2257: (line bay). The parallel bay shorts circuit between the two bars

2258: {\tt b1} and {\tt b2}. It consists of two insulators {\tt ip1} and

2259: {\tt ip2}, and one circuit breaker {\tt cbp}. It is in the state

2260: {\tt closed} if all its switches are closed; otherwise it is {\tt

2261: open}. The line bay connects the distribution line with either the

2262: first bar or the second one. It consists of three insulators {\tt

2263: ilb1}, {\tt ilb2}, and {\tt il1}, and one circuit breaker {\tt

2264: cbl}. It is in the state {\tt closed\_on\_b1} if {\tt ilb1}, {\tt

2265: cbl},  and {\tt il1} are closed, and in the state {\tt

2266: closed\_on\_b2} if {\tt ilb2}, {\tt cbl},  and {\tt il1} are

2267: closed.

2268: 

2269: We focus on the specification of the change of the bar connected

2270: to the line from {\tt b1} to {\tt b2}. The supervisor starts its

2271: operation by closing the parallel bay, an action that takes about

2272: $10$ \emph{seconds}; then, it first closes the insulator {\tt

2273: ilb2}, an action that takes about $5$ \emph{seconds} and then it

2274: opens the insulator {\tt ilb1}, and action that takes $5$

2275: \emph{seconds} as well; finally, it opens the parallel bay, an

2276: action that takes other $10$ \emph{seconds}.

2277: %

2278: To model the behavior of the system, we use the predicates {\tt

2279: change\_b1\_b2}, {\tt change\_b2\_b1}, {\tt close\_pb}, {\tt

2280: open\_pb}, {\tt close\_ilb1}, {\tt open\_ilb1}, {\tt close\_ilb2},

2281: and so on to denote the corresponding commands sent by the

2282: supervisor to the various devices. Furthermore, for every system

2283: action we identify the time granularity with respect to which it

2284: can be considered as an instantaneous action. The change of the

2285: bar takes about $30$ seconds, opening and closing the parallel bay

2286: $10$ seconds, switching insulators $5$ seconds, and switching

2287: circuit breakers $50$ milliseconds. Accordingly, we assume a

2288: $4$-layered structure whose $4$ layers correspond to the $4$

2289: involved time granularities, namely, {\tt 30secs}, {\tt 10secs},

2290: {\tt 5secs}, and {\tt 50millisecs} (in \cite{FM03} we show how to

2291: tailor temporal logics for time granularity over downward

2292: unbounded layered structures to deal with $n$-layered structures).

2293: 

2294: In the monadic second-order language, the change of the bar is

2295: described by the following formula, which specifies the sequence

2296: of actions taken by the supervisor:

2297: 

2298: $$\begin{array}{ll}

2299:   \A x.\ (T^{30secs}(x) \And change\_b1\_b2(x) \Imp &

2300:   \E y_1.\ {\da_0}(x) = y_1 \And close\_pb(y_1) \And \\

2301:   & \E y_2.\ {+1}_{10secs}(y_1,y_2) \And \\

2302:   & \E y_3.\ {\da_0}(y_2) = y_3 \And close\_ilb2(y_3) \And \\

2303:   & \E y_4.\ {+1}_{5secs}(y_3,y_4) \And open\_ilb1(y_4) \And \\

2304:   & \E y_5.\ {+1}_{5secs}(y_4,y_5) \And \\

2305:   & \E y_6.\ {\da_0}(y_6) = y_5 \And open\_pb(y_6)),

2306: \end{array}$$

2307: 

2308: \noindent where the definable predicate ${+1}_{g}(x,y)$ states

2309: that both $x$ and $y$ belong to the layer $g$ and $y$ is the

2310: successor $x$ with respect to $g$. Such a condition can be

2311: expressed in temporalized logic in a much more compact and

2312: readable way:

2313: 

2314: $$\begin{array}{ll} \op{G}(change\_b1\_b2 \Imp & \op{EX_0}

2315: close\_pb \And \op{EX_1X_0}close\_ilb2  \And \\ & \op{EX_1X_1}

2316: open\_ilb1 \And \op{EX_2} open\_pb)

2317: \end{array}$$

2318: 

2319: As for the compound operation {\tt close\_pb}, let us assume that

2320: the supervisor starts in parallel the closure of the circuit

2321: breaker, which is completed in 50 milliseconds, and of the first

2322: insulator, that takes about 5 seconds; then, once the first

2323: insulator is closed, it closes the second one. Such an operation

2324: can be specified by the following classical formula:

2325: 

2326: $$\begin{array}{ll}

2327:   \A x.\ (T^{10secs}(x) \And close\_pb(x) \Imp &

2328:   \E y_1.\ {\da_0}(x) = y_1 \And close\_ip1(y_1) \And \\

2329:   & \E y_2.\ {\da_0}(y_1,y_2) \And close\_cbp(y_2) \And \\

2330:   & \E y_3.\ {+1}_{5secs}(y_1,y_3) \And close\_ip2(y_3),

2331: \end{array}$$

2332: 

2333: while its temporalized version is structured as follows:

2334: 

2335: $$\begin{array}{ll} \op{G}(&(\op{EX_0} close\_pb \Imp

2336: \op{EX_0}(\op{EX_0}(close\_ip1 \And \op{X_0} close\_cpb) \And

2337: \op{EX_1} close\_ip2)) \And \\ & (\op{EX_1} close\_pb \Imp

2338: \op{EX_1}(\op{EX_0}(close\_ip1 \And \op{X_0} close\_cpb) \And

2339: \op{EX_1} close\_ip2)) \And \\ & (\op{EX_2} close\_pb \Imp

2340: \op{EX_2}(\op{EX_0}(close\_ip1 \And \op{X_0} close\_cpb) \And

2341: \op{EX_1} close\_ip2))).

2342: \end{array}$$

2343: 

2344: 

2345: \section{Conclusions and future work}

2346: \label{sec:cfw}

2347: 

2348: In this paper, we provided the monadic second-order theories of

2349: DULSs and UULSs with expressively complete and elementarily

2350: decidable temporal logic counterparts. To this end, we defined

2351: temporalized automata, which can be seen as the

2352: automaton-theoretic counterpart of temporalized logics, and showed

2353: that relevant properties, such as closure under Boolean

2354: operations, decidability, and expressive equivalence with respect

2355: to temporal logics, transfer from component automata to

2356: temporalized ones. Then, we exploited temporalized automata to

2357: successfully solve the problem of finding the temporal logic

2358: counterparts of the given theories of time granularity.

2359: 

2360: As a matter of fact, some forms of automaton combination, which

2361: differ from temporalization in various respects, have been

2362: proposed in the literature to increase the expressive power of

2363: temporal logics. As an example, extensions of PLTL with

2364: connectives defined by means of finite automata over

2365: $\omega$-strings are investigated in \cite{VW94}. To gain the

2366: expressive power of the full monadic second-order theory of

2367: $(\omega,<)$, Vardi and Wolper's Extended Temporal Logic (ETL)

2368: replaces the until operator of PLTL by an infinite bunch of

2369: automata connectives, that is, ETL allows formulas to occur as

2370: arguments of an automaton connective (as many formulas as the

2371: symbols of the automaton alphabet are). Given the well-known

2372: correspondence between formulas and automata, the application of

2373: automata connectives to formulas can be viewed as a form of

2374: automata combination. An extension of $\ctls$ that substitutes ETL

2375: operators for PLTL ones is given in \cite{Da94}. However, the

2376: switch from PLTL to ETL does not involve any change in the domain

2377: of interpretation ($\omega$-structures in the first case, binary

2378: trees in the latter). On the contrary, in the case of temporalized

2379: automata/logics, component automata/temporal logics refer to

2380: different temporal structures, and thus their combination is

2381: paired with a combination of the underlying temporal structures.

2382: 

2383: We are developing our research on temporalized logics and automata

2384: for time granularity in various directions. First of all, we are

2385: trying to improve the complexity bound for the satisfiability

2386: problem for $\tl{\eqltl}{\eqdctls}$ over UULSs. Second, we are

2387: investigating the relationships between temporalized and classical

2388: automata. On the one hand, the languages recognized by

2389: temporalized automata are structurally different from those

2390: recognized by classical automata, e.g., {\tt B\"uchi(B\"uchi)}

2391: automata recognize infinite strings of infinite strings. On the

2392: other hand, this fact does not imply that language problems for

2393: temporalized automata cannot be reduced to the corresponding

2394: problems  for classical automata. As an example, the emptiness

2395: problem for {\tt B\"uchi(B\"uchi)} automata can actually be

2396: reduced to the emptiness problem for {\tt B\"uchi} automata. We

2397: are exploring the possibility of defining similar reductions for

2398: more complex temporalized automata. Finally, we are exploring the

2399: possibility of extending our correspondence results to other forms

2400: of logic combination, such as independent combination and join

2401: \cite{GKWZ03}.

2402: 

2403: \section*{Acknowledgements}

2404: We would like to thank the anonymous reviewers for their comments

2405: and criticisms, that helped us to improve the paper, as well as

2406: Johan van Benthem, Ahmed Bouajjani, Marcelo Finger, Valentin

2407: Goranko, Maarten de Rijke, and Wolfgang Thomas for their positive

2408: feedback on the work reported in the paper. Thanks also to Pietro

2409: Corvaia, Alberto Policriti, and Franca Rinaldi for the useful

2410: discussions about the proof of Lemma \ref{lm:cond4}.

2411: 

2412: 

2413: \bibliographystyle{acmtrans}

2414: %\bibliography{main}

2415: 

2416: \begin{thebibliography}{}

2417: 

2418: \bibitem[\protect\citeauthoryear{Agrawal and Srikant}{Agrawal and

2419:   Srikant}{1995}]{AS95}

2420: {\sc Agrawal, R.} {\sc and} {\sc Srikant, R.} 1995.

2421: \newblock Mining sequential patterns.

2422: \newblock In {\em Proceedings of the International Conference on Data

2423:   Engineering}. IEEE Computer Society Press, 3--14.

2424: 

2425: \bibitem[\protect\citeauthoryear{Bettini, Brodsky, Jajodia, and Wang}{Bettini

2426:   et~al\mbox{.}}{1997}]{BBJW97}

2427: {\sc Bettini, C.}, {\sc Brodsky, A.}, {\sc Jajodia, S.}, {\sc and} {\sc Wang,

2428:   X.~S.} 1997.

2429: \newblock Logical design for temporal databases with multiple granularities.

2430: \newblock {\em {ACM} Transactions on Database Systems\/}~{\em 22,\/}~2,

2431:   115--170.

2432: 

2433: \bibitem[\protect\citeauthoryear{Bettini, Jajodia, Lin, and Wang}{Bettini

2434:   et~al\mbox{.}}{1998}]{BJLW98}

2435: {\sc Bettini, C.}, {\sc Jajodia, S.}, {\sc Lin, J.}, {\sc and} {\sc Wang,

2436:   X.~S.} 1998.

2437: \newblock Discovering frequent event patterns with multiple granularities in

2438:   time sequences.

2439: \newblock {\em {IEEE} Transactions on Knowledge and Data Engineering\/}~{\em

2440:   10,\/}~2, 222--237.

2441: 

2442: \bibitem[\protect\citeauthoryear{Bettini, Jajodia, and Wang}{Bettini

2443:   et~al\mbox{.}}{1996a}]{BWJ96a}

2444: {\sc Bettini, C.}, {\sc Jajodia, S.}, {\sc and} {\sc Wang, X.} 1996a.

2445: \newblock A general framework and reasoning models for time granularity.

2446: \newblock In {\em Proceedings of the International Workshop on Temporal

2447:   Representation and Reasoning}. IEEE Computer Society Press, 104--111.

2448: 

2449: \bibitem[\protect\citeauthoryear{Bettini, Jajodia, and Wang}{Bettini

2450:   et~al\mbox{.}}{1996b}]{BJW96b}

2451: {\sc Bettini, C.}, {\sc Jajodia, S.}, {\sc and} {\sc Wang, X.~S.} 1996b.

2452: \newblock Testing complex temporal relationships involving multiple

2453:   granularities and its application to data mining.

2454: \newblock In {\em Proceedings of the {ACM} {SIGACT}-{SIGMOD}-{SIGART} Symposium

2455:   on Principles of Database Systems}. Vol.~15. ACM Press, 68--78.

2456: 

2457: \bibitem[\protect\citeauthoryear{Blackburn and Bos}{Blackburn and

2458:   Bos}{2003}]{BB03}

2459: {\sc Blackburn, P.} {\sc and} {\sc Bos, J.} 2003.

2460: \newblock {\em Representation and Inference for Natural Language}.

2461: \newblock Studies in Logic, Language, and Information. CSLI Press.

2462: \newblock Forthcoming.

2463: 

2464: \bibitem[\protect\citeauthoryear{Chandra, Segev, and Stonebraker}{Chandra

2465:   et~al\mbox{.}}{1994}]{CSS93}

2466: {\sc Chandra, R.}, {\sc Segev, A.}, {\sc and} {\sc Stonebraker, M.} 1994.

2467: \newblock Implementing calendars and temporal rules in next generation

2468:   databases.

2469: \newblock In {\em Proceedings of the International Conference on Data

2470:   Engineering}. IEEE Computer Society Press, Houston, TX, 264--273.

2471: 

2472: \bibitem[\protect\citeauthoryear{Ciapessoni, Corsetti, Montanari, and

2473:   San~Pietro}{Ciapessoni et~al\mbox{.}}{1993}]{CCMSP93}

2474: {\sc Ciapessoni, E.}, {\sc Corsetti, E.}, {\sc Montanari, A.}, {\sc and} {\sc

2475:   San~Pietro, P.} 1993.

2476: \newblock Embedding time granularity in a logical specification language for

2477:   synchronous real-time systems.

2478: \newblock {\em Science of Computer Programming\/}~{\em 20}, 141--171.

2479: 

2480: \bibitem[\protect\citeauthoryear{Combi, Franceschet, and Peron}{Combi

2481:   et~al\mbox{.}}{2002}]{CFP02}

2482: {\sc Combi, C.}, {\sc Franceschet, M.}, {\sc and} {\sc Peron, A.} 2002.

2483: \newblock A logical approach to represent and reason about calendars.

2484: \newblock In {\em Proceedings of the International Symposium on Temporal

2485:   Representation and Reasoning}. IEEE Computer Society Press, 134--140.

2486: 

2487: \bibitem[\protect\citeauthoryear{Combi and Pozzi}{Combi and Pozzi}{2001}]{CP01}

2488: {\sc Combi, C.} {\sc and} {\sc Pozzi, G.} 2001.

2489: \newblock {A temporal data model managing intervals with different

2490:   granularities and indeterminacy from natural language sentences}.

2491: \newblock {\em The {VLDB} Journal\/}~{\em 9}, 294--311.

2492: 

2493: \bibitem[\protect\citeauthoryear{Corsetti, Crivelli, Mandrioli, Montanari,

2494:   Morzenti, Pietro, and Ratto}{Corsetti et~al\mbox{.}}{1991}]{CCMMMPR91}

2495: {\sc Corsetti, E.}, {\sc Crivelli, E.}, {\sc Mandrioli, D.}, {\sc Montanari,

2496:   A.}, {\sc Morzenti, A.}, {\sc Pietro, P.~S.}, {\sc and} {\sc Ratto, E.} 1991.

2497: \newblock Dealing with different time scales in formal specifications.

2498: \newblock In {\em Proceedings of the International Workshop on Software

2499:   Specification and Design}. IEEE Computer Society Press, 92--101.

2500: 

2501: \bibitem[\protect\citeauthoryear{Corsetti, Montanari, and Ratto}{Corsetti

2502:   et~al\mbox{.}}{1991}]{CMR91b}

2503: {\sc Corsetti, E.}, {\sc Montanari, A.}, {\sc and} {\sc Ratto, E.} 1991.

2504: \newblock Dealing with different time granularities in formal specifications of

2505:   real-time systems.

2506: \newblock {\em The Journal of Real-Time Systems\/}~{\em 3}, 191--215.

2507: 

2508: \bibitem[\protect\citeauthoryear{Courcoubetis, Vardi, Wolper, and

2509:   Yannakakis}{Courcoubetis et~al\mbox{.}}{1991}]{CVWY91}

2510: {\sc Courcoubetis, C.}, {\sc Vardi, M.}, {\sc Wolper, P.}, {\sc and} {\sc

2511:   Yannakakis, M.} 1991.

2512: \newblock Memory efficient algorithms for the verification of temporal

2513:   properties.

2514: \newblock In {\em Proceedings of Computer-Aided Verification}. Lecture Notes in

2515:   Computer Science, vol. 531. Springer, Berlin, Germany, 233--242.

2516: 

2517: \bibitem[\protect\citeauthoryear{Cukierman and Delgrande}{Cukierman and

2518:   Delgrande}{1998}]{CD98}

2519: {\sc Cukierman, D.} {\sc and} {\sc Delgrande, J.} 1998.

2520: \newblock Expressing time intervals and repetition within a formalization of

2521:   calendars.

2522: \newblock {\em Computational Intelligence\/}~{\em 14,\/}~4, 563--597.

2523: 

2524: \bibitem[\protect\citeauthoryear{Dam}{Dam}{1994}]{Da94}

2525: {\sc Dam, M.} 1994.

2526: \newblock {CTL}$^*$ and {ECTL}$^*$ as fragments of the modal $\mu$-calculus.

2527: \newblock {\em Theoretical Computer Science\/}~{\em 126}, 77--96.

2528: 

2529: \bibitem[\protect\citeauthoryear{Dreyer, Dittrich, and Schmidt}{Dreyer

2530:   et~al\mbox{.}}{1994}]{DDS94}

2531: {\sc Dreyer, W.}, {\sc Dittrich, A.~K.}, {\sc and} {\sc Schmidt, D.} 1994.

2532: \newblock Research perspectives for time series management systems.

2533: \newblock {\em {SIGMOD} Record\/}~{\em 23,\/}~1, 10--15.

2534: 

2535: \bibitem[\protect\citeauthoryear{Dyreson and Snodgrass}{Dyreson and

2536:   Snodgrass}{1995}]{DS95}

2537: {\sc Dyreson, C.~E.} {\sc and} {\sc Snodgrass, R.~T.} 1995.

2538: \newblock Temporal granularity.

2539: \newblock In {\em The {TSQL2} Temporal Query Language}, {R.~T. Snodgrass}, Ed.

2540:   Kluwer Academic Press, 347--385.

2541: 

2542: \bibitem[\protect\citeauthoryear{Emerson}{Emerson}{1990}]{E90}

2543: {\sc Emerson, E.} 1990.

2544: \newblock Temporal and modal logic.

2545: \newblock In {\em Handbook of Theoretical Computer Science, Vol. B}, {J.~van

2546:   Leeuwen}, Ed. Elsevier Science Publishers B.V., 995--1072.

2547: 

2548: \bibitem[\protect\citeauthoryear{Euzenat}{Euzenat}{1995}]{E95}

2549: {\sc Euzenat, J.} 1995.

2550: \newblock An algebraic approach for granularity in qualitative space and time

2551:   representation.

2552: \newblock In {\em Proceedings of the International Joint Conference on

2553:   Artificial Intelligence}. Morgan Kaufmann, 894--900.

2554: 

2555: \bibitem[\protect\citeauthoryear{Fiadeiro and Maibaum}{Fiadeiro and

2556:   Maibaum}{1994}]{FiMa94}

2557: {\sc Fiadeiro, J.~L.} {\sc and} {\sc Maibaum, T.} 1994.

2558: \newblock Sometimes {"}tomorrow{"} is {"}sometime{"}: Action refinement in a

2559:   temporal logic of objects.

2560: \newblock In {\em Proceedings of the International Conference on Temporal

2561:   Logic}. Lectures Notes on Artificial Intelligence, vol. 827. Springer,

2562:   48--66.

2563: 

2564: \bibitem[\protect\citeauthoryear{Finger and Gabbay}{Finger and

2565:   Gabbay}{1992}]{FG92}

2566: {\sc Finger, M.} {\sc and} {\sc Gabbay, D.~M.} 1992.

2567: \newblock Adding a temporal dimension to a logic system.

2568: \newblock {\em Journal of Logic Language and Information\/}~{\em 1}, 203--233.

2569: 

2570: \bibitem[\protect\citeauthoryear{Foster, Leban, and McDonald}{Foster

2571:   et~al\mbox{.}}{1986}]{FLM86}

2572: {\sc Foster, D.}, {\sc Leban, B.}, {\sc and} {\sc McDonald, D.} 1986.

2573: \newblock A representation for collections of temporal intervals.

2574: \newblock In {\em Proceedings of the National Conference on Artificial

2575:   Intelligence}. 367--371.

2576: 

2577: \bibitem[\protect\citeauthoryear{Franceschet}{Franceschet}{2002}]{F01}

2578: {\sc Franceschet, M.} 2002.

2579: \newblock Dividing and conquering the layered land.

2580: \newblock Ph.D. thesis, Department of Mathematics and Computer Science,

2581:   University of Udine.

2582: 

2583: \bibitem[\protect\citeauthoryear{Franceschet and Montanari}{Franceschet and

2584:   Montanari}{2001a}]{FM01b}

2585: {\sc Franceschet, M.} {\sc and} {\sc Montanari, A.} 2001a.

2586: \newblock A combined approach to temporal logics for time granularity.

2587: \newblock In {\em Proceedings of the International Workshop on Methods for

2588:   Modalities (M4M)}.

2589: 

2590: \bibitem[\protect\citeauthoryear{Franceschet and Montanari}{Franceschet and

2591:   Montanari}{2001b}]{FM01a}

2592: {\sc Franceschet, M.} {\sc and} {\sc Montanari, A.} 2001b.

2593: \newblock Towards an automata-theoretic counterpart of combined temporal

2594:   logics.

2595: \newblock In {\em Proceedings of the International Workshop on Verification and

2596:   Computational Logic}. 55--74.

2597: 

2598: \bibitem[\protect\citeauthoryear{Franceschet and Montanari}{Franceschet and

2599:   Montanari}{2002}]{FM02b}

2600: {\sc Franceschet, M.} {\sc and} {\sc Montanari, A.} 2002.

2601: \newblock Time granularities in databases, data mining, and temporal reasoning,

2602:   by {B}ettini, {J}ajodia, and {W}ang (book review).

2603: \newblock {\em The Computer Journal\/}~{\em 45,\/}~6, 683--685.

2604: 

2605: \bibitem[\protect\citeauthoryear{Franceschet and Montanari}{Franceschet and

2606:   Montanari}{2003}]{FM03}

2607: {\sc Franceschet, M.} {\sc and} {\sc Montanari, A.} 2003.

2608: \newblock Branching within time: an expressively complete and elementarily

2609:   decidable temporal logic for time granularity.

2610: \newblock {\em Research on Language and Computation\/}~{\em 1,\/}~3-4,

2611:   229--263.

2612: 

2613: \bibitem[\protect\citeauthoryear{Franceschet, Montanari, and

2614:   de~Rijke}{Franceschet et~al\mbox{.}}{2000}]{FMdeR00}

2615: {\sc Franceschet, M.}, {\sc Montanari, A.}, {\sc and} {\sc de~Rijke, M.} 2000.

2616: \newblock Model checking for combined logics.

2617: \newblock In {\em Proceedings of the International Conference on Temporal

2618:   Logic}. 65--73.

2619: 

2620: \bibitem[\protect\citeauthoryear{Fum, Guida, Montanari, and Tasso}{Fum

2621:   et~al\mbox{.}}{1989}]{FGMT89}

2622: {\sc Fum, D.}, {\sc Guida, G.}, {\sc Montanari, A.}, {\sc and} {\sc Tasso, C.}

2623:   1989.

2624: \newblock Using levels and viewpoints in text representation.

2625: \newblock In {\em Proceedings of the International Conference on Artificial

2626:   Intelligence and Information-Control Systems of Robots}. 37--44.

2627: 

2628: \bibitem[\protect\citeauthoryear{Gabbay, Kurucz, Wolter, and

2629:   Zakharyaschev}{Gabbay et~al\mbox{.}}{2003}]{GKWZ03}

2630: {\sc Gabbay, D.}, {\sc Kurucz, A.}, {\sc Wolter, F.}, {\sc and} {\sc

2631:   Zakharyaschev, M.} 2003.

2632: \newblock {\em Many-dimensional modal logics: theory and applications}. Studies

2633:   in Logic and the Foundations of Mathematics, vol. 148.

2634: \newblock Elsevier.

2635: 

2636: \bibitem[\protect\citeauthoryear{Gabbay and de~Rijke}{Gabbay and

2637:   de~Rijke}{2000}]{GdR00}

2638: {\sc Gabbay, D.~M.} {\sc and} {\sc de~Rijke, M.}, Eds. 2000.

2639: \newblock {\em Frontiers of Combining Systems 2}. Studies in Logic and

2640:   Computation, vol.~7.

2641: \newblock Research Studies Press/Wiley.

2642: 

2643: \bibitem[\protect\citeauthoryear{Hafer and Thomas}{Hafer and

2644:   Thomas}{1987}]{HT87}

2645: {\sc Hafer, T.} {\sc and} {\sc Thomas, W.} 1987.

2646: \newblock Computation tree logic {CTL*} and path quantifiers in the monadic

2647:   theory of the binary tree.

2648: \newblock In {\em Proceedings of the International Colloquium on Automata,

2649:   Languages and Programming}. Lecture Notes in Computer Science, vol. 267.

2650:   Springer, Karlsruhe, Germany, 269--279.

2651: 

2652: \bibitem[\protect\citeauthoryear{Halpern and Shoham}{Halpern and

2653:   Shoham}{1991}]{HS91}

2654: {\sc Halpern, J.~Y.} {\sc and} {\sc Shoham, Y.} 1991.

2655: \newblock A propositional modal logic of time intervals.

2656: \newblock {\em Journal of the {ACM}\/}~{\em 38,\/}~4, 935--962.

2657: 

2658: \bibitem[\protect\citeauthoryear{Immerman and Kozen}{Immerman and

2659:   Kozen}{1989}]{IK89}

2660: {\sc Immerman, N.} {\sc and} {\sc Kozen, D.} 1989.

2661: \newblock Definability with bounded number of bound variables.

2662: \newblock {\em Information and Computation\/}~{\em 83,\/}~2, 121--139.

2663: 

2664: \bibitem[\protect\citeauthoryear{Jajodia, Litwin, and Wiederhold}{Jajodia

2665:   et~al\mbox{.}}{1993}]{JLW93}

2666: {\sc Jajodia, S.}, {\sc Litwin, W.}, {\sc and} {\sc Wiederhold, G.} 1993.

2667: \newblock Integrating temporal data in a heterogeneous environment.

2668: \newblock In {\em Temporal Databases: Theory, Design and Implementation}, {{A.

2669:   Tansel et al.}}, Ed. Database Systems and Applications Series,

2670:   Benjamin/Cummings Pub. Co., Redwood City, CA, 563--579.

2671: 

2672: \bibitem[\protect\citeauthoryear{Jajodia, Subrahmanian, and Wang}{Jajodia

2673:   et~al\mbox{.}}{1995}]{JSW95}

2674: {\sc Jajodia, S.}, {\sc Subrahmanian, V.~S.}, {\sc and} {\sc Wang, X.~S.} 1995.

2675: \newblock Temporal modules: An approach toward federated temporal databases.

2676: \newblock {\em Information Sciences\/}~{\em 82}, 103--128.

2677: 

2678: \bibitem[\protect\citeauthoryear{Jard and Jeron}{Jard and Jeron}{1989}]{JJ89}

2679: {\sc Jard, C.} {\sc and} {\sc Jeron, T.} 1989.

2680: \newblock On-line model checking for finite linear temporal logic

2681:   specifications.

2682: \newblock In {\em Proceedings of the Workshop on Automatic Verification Methods

2683:   for Finite State Systems}. Lecture Notes in Computer Science, vol. 407.

2684:   Springer, 189--196.

2685: 

2686: \bibitem[\protect\citeauthoryear{Kamp and Schiehlen}{Kamp and

2687:   Schiehlen}{2001}]{KS01}

2688: {\sc Kamp, H.} {\sc and} {\sc Schiehlen, M.} 2001.

2689: \newblock Temporal location in natural language.

2690: \newblock In {\em How to say when it happens}, {H.~Kamp} {and} {U.~Reyle}, Eds.

2691:   Max Niemeyer Verlag.

2692: 

2693: \bibitem[\protect\citeauthoryear{Kupferman, Vardi, and Wolper}{Kupferman

2694:   et~al\mbox{.}}{2000}]{KVW00}

2695: {\sc Kupferman, O.}, {\sc Vardi, M.~Y.}, {\sc and} {\sc Wolper, P.} 2000.

2696: \newblock An automata-theoretic approach to branching-time model checking.

2697: \newblock {\em Journal of the ACM\/}~{\em 47,\/}~2, 312--360.

2698: 

2699: \bibitem[\protect\citeauthoryear{Ladkin}{Ladkin}{1987}]{L87}

2700: {\sc Ladkin, P.} 1987.

2701: \newblock The completeness of a natural system for reasoning with time

2702:   intervals.

2703: \newblock In {\em Proceedings of the International Joint Conference on

2704:   Artificial Intelligence}. Morgan Kaufmann, 462--467.

2705: 

2706: \bibitem[\protect\citeauthoryear{Lamport}{Lamport}{1985}]{Lam85}

2707: {\sc Lamport, L.} 1985.

2708: \newblock On interprocess communication.

2709: \newblock Tech. Rep.~8, SRC, Palo Alto, CA.

2710: 

2711: \bibitem[\protect\citeauthoryear{Mannila, Toivonen, and Verkamo}{Mannila

2712:   et~al\mbox{.}}{1995}]{MTV95}

2713: {\sc Mannila, H.}, {\sc Toivonen, H.}, {\sc and} {\sc Verkamo, A.~I.} 1995.

2714: \newblock {Discovering Frequent Episodes in Sequences}.

2715: \newblock In {\em Proceedings of the International Conference on Knowledge

2716:   Discovery and Data Mining}. AAAI Press, Montreal, Canada.

2717: 

2718: \bibitem[\protect\citeauthoryear{Montanari}{Montanari}{1996}]{M96}

2719: {\sc Montanari, A.} 1996.

2720: \newblock {\em Metric and Layered Temporal Logic for Time Granularity}.

2721: \newblock ILLC Dissertation Series 1996-02, ILLC, University of Amsterdam, The

2722:   Netherlands.

2723: 

2724: \bibitem[\protect\citeauthoryear{Montanari, Maim, Ciapessoni, and

2725:   Ratto}{Montanari et~al\mbox{.}}{1992}]{MMCR92}

2726: {\sc Montanari, A.}, {\sc Maim, E.}, {\sc Ciapessoni, E.}, {\sc and} {\sc

2727:   Ratto, E.} 1992.

2728: \newblock Dealing with time granularity in the event calculus.

2729: \newblock In {\em Proceedings of the International Conference on fifth

2730:   Generation Computer Systems}. 702--712.

2731: 

2732: \bibitem[\protect\citeauthoryear{Montanari and Pernici}{Montanari and

2733:   Pernici}{1993}]{MP93}

2734: {\sc Montanari, A.} {\sc and} {\sc Pernici, B.} 1993.

2735: \newblock Temporal reasoning.

2736: \newblock In {\em Temporal Databases}, {{A. Tansel et al.}}, Ed. Database

2737:   Systems and Applications Series. Benjamin/Cummings Pub. Co., Redwood City,

2738:   CA, 534--562.

2739: 

2740: \bibitem[\protect\citeauthoryear{Montanari, Peron, and Policriti}{Montanari

2741:   et~al\mbox{.}}{1999}]{MPP99}

2742: {\sc Montanari, A.}, {\sc Peron, A.}, {\sc and} {\sc Policriti, A.} 1999.

2743: \newblock Decidable theories of $\omega$-layered metric temporal structures.

2744: \newblock {\em Logic Journal of the {IGPL}\/}~{\em 7,\/}~1, 79--102.

2745: 

2746: \bibitem[\protect\citeauthoryear{Montanari, Peron, and Policriti}{Montanari

2747:   et~al\mbox{.}}{2000}]{MPP00}

2748: {\sc Montanari, A.}, {\sc Peron, A.}, {\sc and} {\sc Policriti, A.} 2000.

2749: \newblock The taming (timing) of the states.

2750: \newblock {\em Logic Journal of the {IGPL}\/}~{\em 8,\/}~5, 681--699.

2751: 

2752: \bibitem[\protect\citeauthoryear{Montanari, Peron, and Policriti}{Montanari

2753:   et~al\mbox{.}}{2002}]{MPP02}

2754: {\sc Montanari, A.}, {\sc Peron, A.}, {\sc and} {\sc Policriti, A.} 2002.

2755: \newblock Extending {K}amp's theorem to model time granularity.

2756: \newblock {\em Journal of Logic and Computation\/}~{\em 12}, 641--677.

2757: 

2758: \bibitem[\protect\citeauthoryear{Montanari and Policriti}{Montanari and

2759:   Policriti}{1996}]{MP96}

2760: {\sc Montanari, A.} {\sc and} {\sc Policriti, A.} 1996.

2761: \newblock Decidability results for metric and layered temporal logics.

2762: \newblock {\em Notre Dame Journal of Formal Logic\/}~{\em 37}, 260--282.

2763: 

2764: \bibitem[\protect\citeauthoryear{Montanari, Sciavicco, and

2765:   Vitacolonna}{Montanari et~al\mbox{.}}{2002}]{MSV02}

2766: {\sc Montanari, A.}, {\sc Sciavicco, G.}, {\sc and} {\sc Vitacolonna, N.} 2002.

2767: \newblock Decidability of interval temporal logics over split-frames via

2768:   granularity.

2769: \newblock In {\em Proceedings of the European Conference on Logic in Artificial

2770:   Intelligence}. Lectures Notes on Artificial Intelligence, vol. 2424.

2771:   Springer, Berlin, 259--270.

2772: 

2773: \bibitem[\protect\citeauthoryear{Moszkowski}{Moszkowski}{1983}]{M83}

2774: {\sc Moszkowski, B.} 1983.

2775: \newblock Reasoning about digital circuits.

2776: \newblock Ph.D. thesis, Department of Computer Science, University of Stanford.

2777: 

2778: \bibitem[\protect\citeauthoryear{Mota and Robertson}{Mota and

2779:   Robertson}{1996}]{MR96}

2780: {\sc Mota, E.} {\sc and} {\sc Robertson, D.} 1996.

2781: \newblock Representing interaction of agents at different time granularities.

2782: \newblock In {\em Proceedings of the International Workshop on Temporal

2783:   Representation and Reasoning}. IEEE Computer Society Press, 72--79.

2784: 

2785: \bibitem[\protect\citeauthoryear{Niezette and Stevenne}{Niezette and

2786:   Stevenne}{1993}]{NS93}

2787: {\sc Niezette, M.} {\sc and} {\sc Stevenne, J.} 1993.

2788: \newblock An efficient symbolic representation of periodic time.

2789: \newblock In {\em Proceeding of the International Conference on Information and

2790:   Knowledge Management}. Lecture Notes in Computer Science, vol. 752. Springer,

2791:   161--168.

2792: 

2793: \bibitem[\protect\citeauthoryear{Ning, Jajodia, and Wang}{Ning

2794:   et~al\mbox{.}}{2002}]{NJW02}

2795: {\sc Ning, P.}, {\sc Jajodia, S.}, {\sc and} {\sc Wang, X.~S.} 2002.

2796: \newblock An algebraic representation of calendars.

2797: \newblock {\em Annals of Mathematics and Artificial Intelligence\/}~{\em 36},

2798:   5--38.

2799: 

2800: \bibitem[\protect\citeauthoryear{Poesio and Brachman}{Poesio and

2801:   Brachman}{1991}]{PB91}

2802: {\sc Poesio, M.} {\sc and} {\sc Brachman, R.~J.} 1991.

2803: \newblock Metric constraints for maintaining appointments: Dates and repeated

2804:   activities.

2805: \newblock In {\em Proceedings of the National Conference on Artificial

2806:   Intelligence}. MIT Press, 253--259.

2807: 

2808: \bibitem[\protect\citeauthoryear{Segev and Chandra}{Segev and

2809:   Chandra}{1993}]{SC93}

2810: {\sc Segev, A.} {\sc and} {\sc Chandra, R.} 1993.

2811: \newblock A data model for time-series analysis.

2812: \newblock In Advanced Database Systems. {\em Lecture Notes in Computer

2813:   Science\/}~{\em 759}, 191--212.

2814: 

2815: \bibitem[\protect\citeauthoryear{Shahar}{Shahar}{1996}]{S96}

2816: {\sc Shahar, Y.} 1996.

2817: \newblock Dynamic temporal interpretation contexts for temporal abstraction.

2818: \newblock In {\em Proceedings of the International Workshop on Temporal

2819:   Representation and Reasoning}. IEEE Computer Society Press, 64--71.

2820: 

2821: \bibitem[\protect\citeauthoryear{Thomas}{Thomas}{1990}]{T90}

2822: {\sc Thomas, W.} 1990.

2823: \newblock Automata on infinite objects.

2824: \newblock In {\em Handbook of Theoretical Computer Science, Vol. B}, {J.~van

2825:   Leeuwen}, Ed. Elsevier Science Publishers, 133--191.

2826: 

2827: \bibitem[\protect\citeauthoryear{Vardi and Wolper}{Vardi and

2828:   Wolper}{1986}]{VW86}

2829: {\sc Vardi, M.~Y.} {\sc and} {\sc Wolper, P.} 1986.

2830: \newblock An automata-theoretic approach to automatic program verification.

2831: \newblock In {\em Proceedings of the Symposium on Logic in Computer Science}.

2832:   IEEE Computer Society Press, Washington, D.C., USA, 332--345.

2833: 

2834: \bibitem[\protect\citeauthoryear{Vardi and Wolper}{Vardi and

2835:   Wolper}{1994}]{VW94}

2836: {\sc Vardi, M.~Y.} {\sc and} {\sc Wolper, P.} 1994.

2837: \newblock Reasoning about infinite computations.

2838: \newblock {\em Information and Computation\/}~{\em 115,\/}~1, 1--37.

2839: 

2840: \bibitem[\protect\citeauthoryear{Venema}{Venema}{1991}]{V91}

2841: {\sc Venema, Y.} 1991.

2842: \newblock A modal logic for chopping intervals.

2843: \newblock {\em Journal of Logic and Computation\/}~{\em 1,\/}~4, 453--476.

2844: 

2845: \bibitem[\protect\citeauthoryear{Wijsen}{Wijsen}{1998}]{Wi98}

2846: {\sc Wijsen, J.} 1998.

2847: \newblock Reasoning about qualitative trends in databases.

2848: \newblock {\em Information Systems\/}~{\em 23,\/}~7, 469--493.

2849: 

2850: \bibitem[\protect\citeauthoryear{Wijsen}{Wijsen}{1999}]{W99}

2851: {\sc Wijsen, J.} 1999.

2852: \newblock Temporal {FDs} on complex objects.

2853: \newblock {\em {ACM} Transactions on Database Systems\/}~{\em 24,\/}~1,

2854:   127--176.

2855: 

2856: \bibitem[\protect\citeauthoryear{Wolper}{Wolper}{1983}]{W83}

2857: {\sc Wolper, P.} 1983.

2858: \newblock Temporal logic can be more expressive.

2859: \newblock {\em Information and Control\/}~{\em 56,\/}~1/2, 72--99.

2860: 

2861: \bibitem[\protect\citeauthoryear{Zhou and Hansen}{Zhou and Hansen}{1998}]{CH98}

2862: {\sc Zhou, C.} {\sc and} {\sc Hansen, M.~R.} 1998.

2863: \newblock An adequate first order interval logic.

2864: \newblock In {\em Compositionality: the Significant Difference}, {W.~{de

2865:   Roever}}, {H.~Langmaak}, {and} {A.~Pnueli}, Eds. Lecture Notes in Computer

2866:   Science, vol. 1536. 584--608.

2867: 

2868: \end{thebibliography}

2869: 

2870: 

2871: \end{document}

2872: