# Questions tagged [linear-temporal-logic]

LTL (linear temporal logic or linear-time temporal logic) is a temporal logic that can encode assertions about the future of traces.

91 questions
Filter by
Sorted by
Tagged with
23 views

### Validity of ♢(p ∨ q) → ¬□(¬p ∨ ¬q) in linear temporal logic

Let p, q denote propositional variables and ϕ, ψ denote LTL formulas. Is the following LTL formulas is valid? ♢(p ∨ q) → ¬□(¬p ∨ ¬q) and how to proof using A not satisfying word is σ1,unsat := {p}∅∅......
779 views

### The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
1 vote
20 views

1 vote
173 views

1 vote
120 views

### is (infinitely often p) ∨ (infinitely often ¬p) valid?

i'm trying to prove every trace over PROP = {p} is a model of the formula. I am very stuck in figuring out a model pi that satisfies this formula, can anyone point me in the right direction?
54 views

### A way to express LTL (varient) to enforce a stream of data to satisfy some linear time logic

Linear Time Logic (LTL) is used for system verification. In my case, I am investing some time, to see the feasibility of using LTL this time to enforce a constraint on a stream of data. Enough of ...
1 vote
56 views

### Automaton-based model checking on finite traces

I want to check whether a formula in finite LTL is valid on a finite, linear trace. For infite traces I would create a Kripke structure of the trace and a Büchi automaton for the negated formula, ...
114 views

### Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$

I am new to LTL and I am trying to understand how it works. My question is: is there such $\sigma$ that: $\sigma \models [\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)]$ I know ...
138 views

### What is the LTL expression for "there is a value of y whose next value is 8"?

Basically i have a program which increases a variable by 1 in each iteration and resets it to 0 as soon as y becomes 8 (i.e. mod 8). It is a quite simple example but it still bugs me out because i ...
60 views

### Validity of self refering state with linear temporal logic 'X' connective

Lets say we have model like the one above or a similar one where a node refers back to itself. Now let's say if I want to know the validity of the formula: $M, s_2 \models Xr$ Will this be valid ...
1 vote
145 views

### Prove that $\text{EF p}$ can't be written in LTL

Why can't we somehow represent it's negation in LTL and go from there? I think maybe because it has (effectively) two existential quantifiers, so negating it does not work. But how do I prove it?
342 views

1 vote
67 views

### Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?

Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$? Attempt: In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as ...
134 views

### Is model checking PSpace-hard *in formula size*?

Sistla/Clarke proved [SC82] that the LTL model-checking problem is PSpace-complete. Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally? ...
1 vote
323 views

### Validity of □(P→ Q) → (◊P → ◊Q) in linear temporal logic

How can I prove that $\Box(P\rightarrow Q)\rightarrow (\Diamond P\rightarrow\Diamond Q)$ is valid in linear temporal logic (LTL)?
1 vote
446 views

### LTL to Büchi automaton, deterministic?

I know it is possible to convert LTL formulas to Büchi automatons. But is it possible to convert a LTL formula to a deterministic Büchi automaton? Are there formulas that can't be converted to a ...
260 views

### Why is LTL Model Checking in PSPACE

Given a LTL formula $\phi$ and a transition system $T$ we have to do following steps: Build a (non deterministic) Büchi automaton for $T$ Build a (non deterministic) Büchi automaton for $\phi$ ...
165 views

### 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 ...
1 vote
622 views

### distinguishing between CTL* formulas $A[FG p]$ and $AFAG p$ using transition system

It is to show, using a transition system, that the two formulas $A[FG p]$ and $AFAG p$ are not equivalent. For me, it seems strange that they are not equivalent. As the first one says that any ...
861 views

### Linear Temporal Logic (LTL) Syntax Infinitely Often

I'm a little confused about some LTL syntax. When the Global and Future operator (GFx) or []<>x is used, what does it mean. In the lecture slides it is given as infinitely often. But I don't ...
117 views

### How to express the existence of winning strategy of the starter of a game in temporal logic?

Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds. A game can be unfolded to a ...
228 views

### How to graph search a LTL-generated Buchi automaton to generate valid execution paths

I have a set of tasks, and a LTL specification that describes which orders of the tasks are legal. I want to find a way to enumerate all permutations of the tasks that meet the specification. For ...
1 vote
For a lecture I am attending, we have to prove that $$\forall \big(a \textsf{U} (b \land \forall \square a)\big) \equiv \big(a \textsf{U} (b \land \square a)\big).$$ That is, we need to prove that ...