Metric and Layered Temporal Logic for Time Granularity
Angelo Montanari

Abstract:
This dissertation is about the design of temporal logics that deal with 
changing time granularities. Time granularity can be defined as the resolution
power of the temporal qualification of a statement. Providing a formalism with
the concept of time granularity makes it possible to specify time information
with respect to differently-grained temporal domains. This does not merely mean
that one can use different time units--say, months and days--to represent time
quantities in a unique flat temporal model, but it involves more difficult
semantic issues related to the problem of assigning a proper meaning to the
association of statements with the different temporal domains of a layered
temporal model and of switching from one domain to a coarser/finer one. 

The original motivation of the work was the design of a temporal logic suitable 
for the specification of real-time systems whose components evolve  according 
to different time scales (granular real-time systems). Nevertheless, there are
significant similarities between the problems it addressed and those dealt with
by the current research on logics that deal with changing contexts and
perspectives. The design of these types of logics is emerging as a relevant 
research topic in the broader area of combination of logics, theories, and
structures, at the intersection of logic with artificial intelligence, computer 
science, and computational linguistics. In this dissertation, we devised
suitable combination techniques both to define temporal logics and to prove 
logical properties of these logics, such as completeness and decidability.                                  

We proposed a metric and layered temporal logic for time granularity, and we 
showed how to use it to specify granular real-time systems. We started by 
considering the purely metric fragment in isolation. We defined a general 
two-sorted framework where a number of metric temporal logics, having a 
different expressive power, can be defined as suitable combinations of a 
temporal component and an algebraic one. Then, we exploited the proposed 
framework to study completeness issues for the various systems of metric 
temporal logic. Despite their relevance, these issues have been ignored or 
only partially  addressed in the literature. The next step was the definition 
of a many-layer metric temporal logic, embedding the notion of time 
granularity. We identified  the main functionalities a logic for time 
granularity must support and the constraints it must satisfy. In particular, 
we identified the set of properties constraining the relations between time 
instants belonging to different layers.  Then, we axiomatically defined a 
metric and layered temporal logic, viewed as the combination of a number of 
differently-grained  (single-layer) metric temporal logics, and we studied its 
logical properties. We devoted a special attention to the decidability problem.
We identified relevant classes of metric and layered temporal structures, and 
showed that the corresponding theories are decidable. More precisely, we proved
the decidability of the validity and satisfiability problems for the theory of 
finitely-layered metric temporal structures, and  for two relevant theories of 
omega-layered metric temporal structures. These decidability results provide 
useful insights about the relations between many-layer and flat metric temporal
systems, e.g., they answer the natural question whether, and under which 
conditions, many-layer temporal systems  can be reduced to flat ones. In the 
last part of the dissertation, we concentrated on the problem of executing 
metric and layered temporal logics. However, instead of proposing any 
specific-system oriented solution, we devised a general set-theoretic 
translation method which has a value of its own, and whose range of 
applicability is not restricted to temporal logics.