Embedding time granularity in a logical specification language for synchronous real-time systems (Q685609)

The paper presents a logical language for specifying a wide-ranging class of real-time systems: the systems whose components have dynamic behaviour regulated by very different time constants (granular systems). It confines itself to the treatment of the class of synchronous granular systems, whose components are temporally qualified with respect to the same clock. The proposed specification language is a metric and layered temporal logic (MLTL) extending metric temporal logics with contextual and projection operators to deal with time granularity. MLTL allows the specifier (i) to associate a time granularity with a formula (contextual operator), (ii) to move a formula in the past/future without changing granularity (displacement operator), and (iii) to shift a formula to coarser/finer time granularities (projection operator). The combined use of the three operators makes it possible to build granular system specifications by referring to the `natural' scale in the specification of any component and by properly constraining interactions between components. MLTL is provided with a model-theoretic semantics and a sound axiomatization.