Expressive completeness for metric temporal logic

DOI10.1109/LICS.2013.41MaRDI QIDQ5271072zbMATH OpenOpenAlexWikidataFDO

Authors Paul Hunter, Joël Ouaknine, James Worrell

Publication date 3 July 2017

Published in 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1208.4993

zbMATH Keywords

expressive completenessfirst-order logiclinear temporal logicmetric temporal logic

Mathematics Subject Classification ID

Temporal logic (03B44)

Abstract: Metric Temporal Logic (MTL) is a generalisation of Linear Temporal Logic in which the Until and Since modalities are annotated with intervals that express metric constraints. A seminal result of Hirshfeld and Rabinovich shows that over the reals, first-order logic with binary order relation < and unary function +1 is strictly more expressive than MTL with integer constants. Indeed they prove that no temporal logic whose modalities are definable by formulas of bounded quantifier depth can be expressively complete for FO(<,+1). In this paper we show the surprising result that if we allow unary functions +q, (q rational), in first-order logic and correspondingly allow rational constants in MTL, then the two logics have the same expressive power. This gives the first generalisation of Kamp's theorem on the expressive completeness of LTL for FO(<) to the quantitative setting. The proof of this result involves a generalisation of Gabbay's notion of separation.

Recommendations

• When is metric temporal logic expressively complete?
• scientific article; zbMATH DE number 7056237
• On the expressiveness of metric temporal logic over bounded timed words
• Expressiveness of Metric modalities for continuous time
• On the expressiveness of TPTL and MTL

Cited in

(24)

• Theorem proving for metric temporal logic over the naturals
• Bounded variability of metric temporal logic
• A multiple-valued logic approach to the design and verification of hardware circuits
• Expressive completeness for LTL with modulo counting and group quantifiers
• When is metric temporal logic expressively complete?
• On Process-Algebraic Extensions of Metric Temporal Logic
• On the expressiveness of metric temporal logic over bounded timed words
• scientific article; zbMATH DE number 1222565 (Why is no real title available?)
• The unary fragments of metric interval temporal logic: bounded versus lower bound constraints
• Separation in nonlinear time models
• Logics meet 1-clock alternating timed automata
• Revisiting separation: algorithms and complexity
• The Expressive Power of Temporal and First-Order Metric Logics
• Heterogeneous and asynchronous networks of timed systems
• \(\mathrm{FO}=\mathrm{FO}^3\) for linear orders with monotone binary relations
• Completeness results for two-sorted metric temporal logics
• Making Metric Temporal Logic Rational
• scientific article; zbMATH DE number 5587267 (Why is no real title available?)
• On the decidability and complexity of Metric Temporal Logic over finite words
• scientific article; zbMATH DE number 7056237 (Why is no real title available?)
• Linear Time Monitoring for One Variable TPTL
• When do you start counting? Revisiting counting and Pnueli modalities in timed logics
• Metric quantifiers and counting in timed logics and automata
• Expressive equivalence between decidable freeze and metric timed temporal logics.

This page was built for publication: Expressive completeness for metric temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5271072)