Abstract
A seminal result of Kamp is that over the reals Linear Temporal Logic (LTL) has the same expressive power as firstorder logic with binary order relation < and monadic predicates. A key question is whether there exists an analogue of Kamp's theorem for Metric Temporal Logic (MTL)  a generalization of LTL in which the Until and Since modalities are annotated with intervals that express metric constraints. Hirshfeld and Rabinovich gave a negative answer, showing that firstorder logic with binary order relation < and unary function +1 is strictly more expressive than MTL with integer constants. However, a recent result of Hunter, Ouaknine and Worrell shows that when rational timing constants are added to both languages, MTL has the same expressive power as firstorder logic, giving a positive answer. In this paper we generalize these results by giving a precise characterization of those sets of constants for which MTL and firstorder logic have the same expressive power. We also show that full firstorder expressiveness can be recovered with the addition of counting modalities, strongly supporting the assertion of Hirshfeld and Rabinovich that Q2MLO is one of the most expressive decidable fragments of FO(<,+1).
BibTeX  Entry
@InProceedings{hunter:LIPIcs:2013:4209,
author = {Paul Hunter},
title = {{When is Metric Temporal Logic Expressively Completel}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {380394},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897606},
ISSN = {18688969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4209},
URN = {urn:nbn:de:0030drops42092},
doi = {10.4230/LIPIcs.CSL.2013.380},
annote = {Keywords: Metric Temporal Logic, Expressive power, Firstorder logic}
}
Keywords: 

Metric Temporal Logic, Expressive power, Firstorder logic 
Seminar: 

Computer Science Logic 2013 (CSL 2013) 
Issue Date: 

2013 
Date of publication: 

27.08.2013 