Extending Kamp's Theorem to Model Time Granularity

摘要

In this paper, a generalization of Kamp's theorem relative to the functional completeness of the until operator is proved. Such a generalization consists in showing the functional completeness of more expressive temporal operators with respect to the extension of the first-order theory of linear orders MFO[＜] with an extra binary relational symbol. The results is motivated by the search of a modal language capable of expressing properties and operators suitable to model time granularity in ω-layered temporal structures.