© 2002 by Oxford University Press
Original Article |
Extending Kamp's Theorem to Model Time Granularity
1 Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy. E-mail: montana{at}dimi.uniud.it, 2 Dipartimento di Scienze Fisiche, Università di Napoli Federico II, Via Cintia, 80126 Napoli, Italy. E-mail: peron{at}na.infn.it, 3 Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy. E-mail: policrit{at}dimi.uniud.it
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 result is motivated by the search of a modal language capable of expressing properties and operators suitable to model time granularity in
-layered temporal structures.
Keywords: Kamp's theorem; linear temporal logic; functional completeness; time granularity
Received 30 January 2001.