Three variables suffice for real-time logic

DOI10.1007/978-3-662-46678-0_23MaRDI QIDQ2949451zbMATH OpenOpenAlexFDO

Authors Timos Antonopoulos, Paul Hunter, Shahab Raza, James Worrell

Publication date 1 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Temporal logic (03B44)

Abstract: A natural framework for real-time specification is monadic first-order logic over the structure $(mathbbR,<,+1)$---the ordered real line with unary $+1$ function. Our main result is that $(mathbbR,<,+1)$ has the 3-variable property: every monadic first-order formula with at most 3 free variables is equivalent over this structure to one that uses 3 variables in total. As a corollary we obtain also the 3-variable property for the structure $(mathbbR,<,f)$ for any fixed linear function $f:mathbbRightarrowmathbbR$. On the other hand, we exhibit a countable dense linear order $(E,<)$ and a bijection $f:EightarrowE$ such that $(E,<,f)$ does not have the $k$-variable property for any $k$.

Recommendations

• scientific article; zbMATH DE number 1693545
• An Expressive Temporal Logic for Real Time
• Finite variability interpretation of monadic logic of order
• The decision problem for linear temporal logic
• Decidability and Expressive Power of Real Time Logics

Cited in

(2)

• scientific article; zbMATH DE number 7561609 (Why is no real title available?)
• Finite variability interpretation of monadic logic of order

This page was built for publication: Three variables suffice for real-time logic

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