Summary

Abstract

The main contributions of the book can be summarized as follows:

• We explored the automaton-based approach to time granularity in full detail. In particular, we introduced suitable notions of single-string automata (possibly extended with counters), which allow one to compactly represent and efficiently manipulate single (ultimately periodic) time granularities. We provided effective procedures to solve the crucial problems of granule conversion, equivalence, and optimization of automaton-based representations of time granularities.

• We dealt with the problem of managing (possibly infinite) sets of time granularities. We characterized the subclass of Büchi automata that recognize exactly the rational ω-languages consisting of ultimately periodic words only (these languages represent possibly infinite sets of ultimately periodic time granularities) and we provided efficient solutions to several basic problems (the emptiness problem, the acceptance problem, the equivalence problem, the inclusion problem, and the state optimization problem), as well as to the granularity comparison problem.

• We addressed the model checking problem for monadic second-order logics interpreted over deterministic vertex-colored trees. We generalized Elgot and Rabin’s contraction method to deal with such a problem and we introduced a large class of trees, called reducible trees, which naturally extends that of regular trees and for which the model checking problem turns out to be decidable.

• We identified several natural operations on trees (e.g., tree morphisms, tree transductions, unfoldings with backward edges and loops) and we proved closure properties of the class of reducible trees with respect to such operations. Then, we exploited these closure properties to prove that the class of reducible trees includes all deterministic trees in the Caucal hierarchy as well as several trees outside it. Moreover, we gave various application examples of the contraction method. In particular, we exploited it to show the equivalence between one-way and two-way alternating Muller tree automata and to prove the decidability of the model checking problem for morphic trees.

• We introduce the class of totally-unbounded layered temporal structures, whose theories subsume the theories of previously known layered temporal structures (i.e., n-layered structures, downward-unbounded and upward-unbounded layered structures). We proved the decidability of the monadic second-order theories of these structures and the decidability of the model checking problem for the chain fragment of monadic second-order logic interpreted over the totally-unbounded layered temporal structures extended with either the equi-level or the equi-column predicate. These results subsume and extend previous results in the literature.