Three variables suffice for real-time logic

DOI10.1007/978-3-662-46678-0_23zbMATH Open1461.03020arXiv1408.1851OpenAlexW2228368164MaRDI QIDQ2949451FDOQ2949451

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)

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$.

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

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

Mathematics Subject Classification ID

Temporal logic (03B44)

Cited In (2)

• Title not available (Why is that?)
• 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)