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.

Filter by
Sorted by
Tagged with
1 vote
0 answers
29 views

How do I prove relations of two CTL formulas?

If I have two CTL equations, how do I prove they're equivalent or that one implies the other? What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
JobHunter69's user avatar
2 votes
1 answer
69 views

About next operator duality in LTL

I'm learning LTL (linear temporal logic) and we learned that a model $M$ and a starting position $q_0$ satisfies a LTL formula $\psi$ iff for every path $\pi$ starting at $q_0$ it is true that $\pi \...
Golden's user avatar
  • 121
1 vote
0 answers
23 views

Errors in examples of Vardi's paper "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces"

The paper Linear Temporal Logic and Linear Dynamic Logic on Finite Traces has the following examples on page 4: Q1. (Update to Q1: solved. See the comment by DCTLib.) The first example says that the ...
Ayrat's user avatar
  • 1,065
0 votes
1 answer
30 views

A proof of the completeness of PLTL (Propositional Linear Temporal Logic)

In what paper(s), textbook(s), and/or classnote(s) can I find a detailed proof of the completeness of a certain proof system for PLTL (Propositional Linear Temporal Logic)?
Evan Aad's user avatar
  • 237
1 vote
2 answers
64 views

What is the Kripke semantic for a linear temporal logic?

I've read that in general for a modal formula P, a world w and a Kripke frame ⟨W,R⟩ w⊨□P if and only if for every u∈W, if wRu then u⊢P In case of LTL, being a modal logic, I assumed that the worlds ...
jack malkovick's user avatar
2 votes
1 answer
68 views

Safety VS. Liveliness Property

I have to prove whether a certain property is safety or liveliness. The property represents the absence of deadlock so I expected it to be a safety property from what I read online. The issue is that ...
davinci_07's user avatar
0 votes
1 answer
326 views

How can I prove that LTL formula is valid?

I do not know with which technique i can prove if a LTL forumula is valid. Let's say we have for example this one: ¬q U(¬p ∧ ¬q) → ¬Gp. How can prove if this valid or not? (should be true in any state ...
40er's user avatar
  • 3
0 votes
1 answer
23 views

Switching between doing something and not doing it within $k$ steps in LTL

Imagine that we are designing a system in which we have the action to brake or not brake. How can we write an LTL specification that guarantees that we cannot switch between braking and not braking ...
mrjamaisvu's user avatar
4 votes
0 answers
183 views

Understanding a proof from a paper (model checking game)

I'm reading the paper: "Model Checking Games for Branching Time Logics" by Martin Lange and Colin Stirling - https://carrick.fmv.informatik.uni-kassel.de/~mlange/papers/jlc2000.pdf. The ...
Mcgfbtl's user avatar
  • 41
1 vote
1 answer
92 views

Logic foundation for formal verification

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are: Hoare Logic (for proving correctness of imperative programs) Linear ...
a_fan's user avatar
  • 111
0 votes
1 answer
234 views

Getting rid of "FG" in a LTL equation

i am currently struggling with a Linear temporal logic equation: $$\phi=FG( \lnot a\lor X \lnot a )$$ For my understanding, it means that starting at a certain point in the future, proposition a can ...
TheDudeWithTheBeard's user avatar
1 vote
1 answer
266 views

Translating Natural Language to LTL Formulae

I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct. I'm given the sentences, and my assumption is that $l$ ...
UnevenMango's user avatar
1 vote
1 answer
129 views

What does “linear” in Linear Temporal Logic refer to?

Consider the term linear temporal logic (in the meaning of linear-time temporal logic). In linear temporal logic, what does linear refer to: to temporal or to logic? If I interpret http://en....
user avatar
1 vote
1 answer
115 views

Complexity of LTL realizability of safety games with Next operator only

It is known that the computational complexity of deciding whether an LTL specification is realizable in a safety game is 2EXP-complete (that is, you receive an LTL formula, where some variables belong ...
Noel Arteche's user avatar
0 votes
0 answers
37 views

Can an LTL formula uniquely be represented by an expression tree?

Just like we can represent a mathematical expression uniquely with a binary expression tree, I was wondering if we could do the same for LTL formulae? Such that no two different looking LTL formula ...
user3598542's user avatar
2 votes
1 answer
123 views

Given LTL formulas $m$ and $p$, is there a tool that can check whether $m \models p$ does hold?

To the best of my understanding, $m \models p$ asks whether the LTL formula $p$ satisfies the LTL formula $m$. In other words, $m \to p$ is a tautology. Here are some examples of where $m \models p$ ...
Meowth8743's user avatar
2 votes
0 answers
54 views

Does Rice's theorem apply to sequential logic circuits?

I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
Grisu47's user avatar
  • 121
5 votes
1 answer
166 views

Test two LTL expression trees for equivalence

Is there an algorithm on how to check if two LTL expressions (represented as binary trees) are semantically equivalent? Since there are many smaller equivalences such as $a\Rightarrow b \equiv \neg a \...
user126114's user avatar
2 votes
1 answer
57 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 ...
Abderrahim ben's user avatar
1 vote
3 answers
130 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?
Jim's user avatar
  • 39
1 vote
1 answer
195 views

LTL Model of (infinitely often p) ∧ ( infinitely often q) ∧ (¬ Eventually (p ∧ q))?

Can anyone give a model of the following LTL formula? $$ \Box\Diamond p \land \Box\Diamond q \land \lnot \Diamond (p \land q). $$ That is, we want each of $p$ and $q$ to hold infinitely often, but $p \...
Jim's user avatar
  • 39
1 vote
1 answer
69 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, ...
twinrix's user avatar
  • 13
2 votes
2 answers
125 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 ...
pblass's user avatar
  • 55
3 votes
1 answer
147 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 ...
null1's user avatar
  • 157
0 votes
1 answer
61 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 ...
KetDog's user avatar
  • 157
1 vote
1 answer
171 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?
root's user avatar
  • 13
0 votes
1 answer
401 views

LTL Logic Finally, Globally and Until to irreflexive Version

my professor said that we can transform the reflexive Finally, Globally and Until into irreflexive Finally, Globally, Until. Can someone explain me this? For irreflexive Finally we have $w \models F^...
comrade's user avatar
  • 27
2 votes
1 answer
167 views

Büchi automaton to Linear Temporal Logic

Given a Büchi automaton what is the procedure to build an equivalent LTL formula? And what is its size? I'm looking for references but I haven't found them so far.
kafka's user avatar
  • 401
1 vote
1 answer
70 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 ...
kauray's user avatar
  • 519
4 votes
1 answer
152 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? ...
Ayrat's user avatar
  • 1,065
2 votes
2 answers
1k views

Negation of the semantics of the Until operator in LTL

I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to: $\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
Jack's user avatar
  • 23
1 vote
1 answer
468 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 ...
ScientiaEtVeritas's user avatar
2 votes
2 answers
313 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$ ...
Cilenco's user avatar
  • 405
2 votes
1 answer
202 views

How to prove a LTL formula correct in a specific model?

I have been learning Verification by model checking recently and I get the following question: $Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
Bowen Peng's user avatar
1 vote
3 answers
347 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)?
zhou ziyao's user avatar
2 votes
1 answer
811 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 ...
Don Fanucci's user avatar
4 votes
1 answer
977 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 ...
yraj429's user avatar
  • 41
2 votes
2 answers
122 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 ...
hengxin's user avatar
  • 9,551
2 votes
2 answers
247 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 ...
user_1_1_1's user avatar
1 vote
1 answer
2k views

Proving the equivalence of an LTL and a CTL formula

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 ...
Luca's user avatar
  • 13
0 votes
1 answer
234 views

Linear Temporal Logic, Idempotent law

in many lecture notes, I have seen the LTL idempotent law for until and its equivalence is described as $\phi U(\phi U \psi) \equiv \phi U\psi$ and also $(\phi U \...
Amir-Mousavi's user avatar
0 votes
1 answer
676 views

LTL globally implies

I have got confused in undressing the informal definition of LTL below: $$G(\phi \Longrightarrow\psi)\Longrightarrow(G\phi \Longrightarrow G\psi)$$ in many literatures I have seen implies is said as ...
Amir-Mousavi's user avatar
2 votes
0 answers
342 views

Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
tender hopper's user avatar
2 votes
1 answer
209 views

Acceptance conditions when translating LTL to Büchi automaton?

As an exercise in better understanding, I have been implementing the LTL to Generalized Büchi Automaton translation algorithm of Gerth, et al. (which is also discussed in Clarke, et al., Model ...
Robert P. Goldman's user avatar
0 votes
1 answer
91 views

LTL to automaton translation that can only read disjunctions of labels per transition

Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the ...
Perissiane's user avatar
0 votes
0 answers
562 views

How to draw a Non Deterministic Buchi Automaton (NBA) from the given property?

I'm new to LTL and Buchi automaton, and I have a hard time in constructing NBA from the given formula or the property. Could somebody please help me? The following property is given, P= "Whenever ...
Rao208's user avatar
  • 1
1 vote
1 answer
465 views

LTL Until Tautology

Today I had to prove some tautologies as an exercise, one of them was: (Ga)->(Fb) equivalent aU(b v ¬a) It is clear that I have to prove the implication in both ways. After putting into negation ...
Stefan's user avatar
  • 45
2 votes
1 answer
271 views

LTL Formula Until with same atoms (aUa)

I am trying to solve some past papers in preparations for my next exam and I've stumbled across the following exercise: While I managed to solve most parts of the exercise, I am still unsure about ...
Stefan's user avatar
  • 45
4 votes
1 answer
245 views

Minimal Deterministic Buchi Automata Product

Problem: Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas. Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1)...
Abhishek Kulkarni's user avatar
1 vote
1 answer
111 views

What is this operator in "The Temporal Logic of Programs" Pnueli 1977?

In The Temporal Logic of Programs there is an operator first appearing on page 3 (48) under "Partial Correctness" that looks like an elongated super set symbol. What is it?
Brent's user avatar
  • 2,553