This paper focuses on decidability problems for metric and layered temporal logics. The considered logics - suitable to model time granularity in various contexts - allow one to build granular temporal models by referring to the natural scale in any component of the model and properly constraining the interactions between differently grained components. We prove the decidability of both the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily fine temporal layers. The proof for the first theory is obtained by a reduction to the decidability problem of an extension of the standard monadic second-order theory of one successor MSO[<], while the proof for the second one is done through a reduction to the monadic second-order decidable theory of k successors MSO[<k, succ0,...,succk-1].

Theories of Omega-Layered Metric Temporal Structures: Expressiveness and Decidability

MONTANARI, Angelo;
1999-01-01

Abstract

This paper focuses on decidability problems for metric and layered temporal logics. The considered logics - suitable to model time granularity in various contexts - allow one to build granular temporal models by referring to the natural scale in any component of the model and properly constraining the interactions between differently grained components. We prove the decidability of both the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily fine temporal layers. The proof for the first theory is obtained by a reduction to the decidability problem of an extension of the standard monadic second-order theory of one successor MSO[<], while the proof for the second one is done through a reduction to the monadic second-order decidable theory of k successors MSO[
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/667801
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact