# Linear Temporal Logic with non-Boolean propositions (e.g. Integers)?

LTL works with Boolean propositions. People probably studied extensions to non-Boolean propositions... Do you know a good starting reference?

(I am aware of STL, but it also seems to talk about clocks, is there a variant without clocks?)

Update: the question is not about "true, false, maybe" but rather about LTL where we can refer to integers, for example. Example: one might want to write G(i+1 == X(i)), meaning that value i should increment.

• Re your update, what it sounds like you want is an LTL with quantifiers. The predicates will still be Boolean propositions (i.e. the logic will still be classical), it will just be first-order instead of propositional. For example, as in this paper and its references particularly 40 and 44 and their references. – Derek Elkins left SE Jul 25 '17 at 7:40
• @DerekElkins that is a great reference (i saw it myself before, but your comment prompted to look deeper). Also, I found "freeze LTL", which allows to store and compare counters along the runs. And super paper---"LTL with the Freeze Quantifier and Register Automata"---which has woanderful exhibition of the state-of-the-art.. – Ayrat Aug 28 '17 at 6:11

There has been some relatively recent work on constructive/intuitionistic variants or interpretations of LTL.

Kojima's and Igarashi's Constructive Linear-Time Temporal Logic: Proof Systems and Kripke Semantics is a decent place to start and references a bit of earlier work. In particular, Maier's Intuitionistic LTL and a New Characterization of Safety and Liveness. More recently, there was Jeffrey's LTL types FRP which showed that proofs of (constructive) LTL formulas corresponded to some FRP (Functional Reactive Programming) programs. Logics with tighter connections were formulated in later work, but this prompted some other work. One recent paper working in a linear logic setting shows a Curry-Howard correspondence between a LTL and event-driven programming: Paykin's, Krishnaswami's, and Zdancewic's The Essence of Event-Driven Programming.

At the level of logic, intuitionistic logic corresponds to having a Heyting algebra of truth values as opposed to a Boolean algebra. In a slightly different vein, Robust Linear Temporal Logic by Tabuada and Neider illustrates a many-valued (5-valued particularly) semantics for a LTL. They don't explore a proof theory except demonstrating that their rLTL can be translated to LTL.

While I didn't mention any, there is undoubtedly work in category theory that relates and would provide another perspective and categorical semantics. E.g. and related to the work above Jeltsch's Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming.

• thank you for wonderful overview of connection LTL with functional programs, and on constructive LTL! My question wasn't very clear though and was actually about more rich propositions: e.g., that can refer to integer signals, instead of Boolean ones. – Ayrat Jul 23 '17 at 7:49

You might be interested in three-valued logic. You can find research papers on three-valued semantics for LTL and versions of LTL for three-valued logic.

Here are some references you might find useful.