patternMinor
Linear Temporal Logic with non-Boolean propositions (e.g. Integers)?
Viewed 0 times
temporallinearbooleannonwithlogicintegerspropositions
Problem
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
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.Solution
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.
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.
Context
StackExchange Computer Science Q#78087, answer score: 5
Revisions (0)
No revisions yet.