3
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Derek Elkins left SE
    Commented Jul 25, 2017 at 7:40
  • $\begingroup$ @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.. $\endgroup$
    – Ayrat
    Commented Aug 28, 2017 at 6:11

3 Answers 3

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Ayrat
    Commented Jul 23, 2017 at 7:49
1
$\begingroup$

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.

Improve this answer
$\endgroup$
0
$\begingroup$

Here are some references you might find useful.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.