Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

1
vote
1answer
42 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 ...
4
votes
1answer
40 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? ...
2
votes
1answer
72 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)...
0
votes
1answer
35 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 ...
3
votes
2answers
54 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$ ...
2
votes
1answer
41 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\ ...
1
vote
3answers
101 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)?
0
votes
1answer
46 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 ...
2
votes
1answer
112 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 ...
2
votes
2answers
80 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 ...
0
votes
0answers
36 views

Writing LTL formula for sequencing with coordination

Suppose there are 2 workers w1 and w2 who can cool a hot iron. So if iron is hot (denoted by atomic proposition ...
2
votes
2answers
86 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
1answer
300 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 ...
0
votes
1answer
62 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 \...
0
votes
1answer
114 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 ...
2
votes
0answers
136 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 ...
2
votes
1answer
46 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 ...
0
votes
1answer
65 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 ...
0
votes
0answers
155 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 ...
1
vote
1answer
132 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 ...
2
votes
1answer
48 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 ...
3
votes
1answer
90 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)...
1
vote
1answer
95 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?
1
vote
0answers
154 views

Show the formula is a law of LTL

Show that the following formula is a law of LTL, i. e. the formula is satisfied on all paths in all models G(p → X q) ∧ G(q → F p) ∧ p → G F p I dont know how ...
1
vote
0answers
58 views

Unable to have an equivalent of A(FG p) and AG(EF p)

It states in my lecture notes that there is no CTL formula that is equivalent to A(FG p) in LTL and likewise, there is no LTL formula that is equivalent to CTL formula AG(EF p). I am just starting to ...
0
votes
1answer
85 views

LTL to GBA versus LTL to BA

Let's assume that I have an LTL formula and I want to convert it to a Buchi automaton. For which fragment of LTL, GBA is more succinct and for which fragment BA has the same size as GBA.
3
votes
3answers
101 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 ...
2
votes
0answers
97 views

Satisfying of $\square (\neg A \cup B)$

Let's consider the following formula: $\square (\neg A \cup B)$. Does the following computation satisfy it? The numbers in brackets are number of state. (0) $\neg A, \neg B$ (1) $\neg A, B$ (2) $...
1
vote
1answer
81 views

What kind of LTL formula can be represented by DBAs

I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?
0
votes
1answer
88 views

Buchi Automaton G(Xa->b)

I have a question regarding buchi automatons. The automata for the LTL formula, G(Xa->b) is as the attached picture. Why dosen't a have to be true in order to make the automaton correct? My ...
6
votes
0answers
94 views

Non-deterministic Buchi vs Rabin: Automaton size for LTL->automaton

Is there any general result to show that which automaton is more succinct? I have a set of LTL properties and I would like to know (show) which automaton is more efficient in term of state number and ...
2
votes
1answer
327 views

$\omega$-regular expression to LTL

Is there any systematic (algorithmic) method to convert an $\omega$-regular expression like $ (a^∗)(b)(b^∗)(a^∗)(c^\omega) $ to an LTL property?
2
votes
1answer
143 views

Are there any LTL to _non_ deterministic Rabin automaton translators?

I know of two translators LTL -> deterministic Rabin automaton: Rabinizer3 ltl2dstar They produce deterministic automata, which can be much larger than their possible non-deterministic variants. Is ...
3
votes
1answer
278 views

What does “AF AX p” mean in CTL?

Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased): In LTL, X F p and F X p are ...
5
votes
2answers
468 views

Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators

Need to prove equivalence for (or disprove equivalence for): $ \hspace{1cm}\square ϕ → \lozenge ψ ≡ ϕ\textsf{ U }(ψ ∨ ¬ϕ) \\ $ My current attempt using the LTL equivalnce rules to determine ...
1
vote
0answers
96 views

generic technique to build LTL/CTL formula that satisfy specific inputs to a model

I have an automaton, for example the below automaton and would like to generate a single formula (LTL or CTL, or some other representation) that satisfy exactly the traces provided. e.g., $t_1 = i^*...
1
vote
0answers
44 views

Size of parity automata and Buchi automata from linear time mu-calculus?

Given a linear time mu-calculus formula, there are many works on transforming the formula to Buchi or Parity automaton. Using the best algorithm, what is the size of the resulting Buchi automaton and ...
12
votes
1answer
429 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 ...
0
votes
1answer
368 views

How to prove LTL-formulas true for all paths?

I'm quoting a question from my homework which I don't understand its wording. Also, I'm not looking for an answer for my problem, I just want to be pointed at some articles/tutorials/reading/tips to ...
0
votes
1answer
282 views

Counterexample for LTL - CTL equivalence [closed]

I have to find an example of a model where the LTL-formula $F G p \wedge F q$ is valid and the CTL-formula $EF AG p \wedge AF q$ is not valid. I found this example, but I'm not completely sure whether ...
2
votes
0answers
27 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
-2
votes
1answer
83 views

Help understaning LTL formulae [closed]

I am studying Software Engineering and I have different LTL formulas for which I have to determine if they are valid, unsatisfiable or neither. Here are the formulas : (<>[]p ∧ <>[]q) → <>[]...
2
votes
1answer
340 views

LTL properties in bounded model checking via assertions

Is there a way to check LTL properties in a bounded model checker? As an example, consider a liveness property ($G F p$ - always eventually $p$)? Suppose we have the following trivial program ...
1
vote
1answer
146 views

Find equivalent LTL formula, without Y (Yesterday) operator. How can I handle first state?

The task is to find an equivalent LTL formula for $G(a \Rightarrow Yb)$, which doesn't contain the Y operator. My idea is to search for invalid path patterns with 2 $a$'s in a row, e.g. bbbbaab. ...
0
votes
1answer
265 views

Given a set of LTL formulas, on which states does the Kripke structure hold? [closed]

I'm currently learning about LTL and CTL formulas and to get a better understanding I try to manually interpret the formulas over a given Kripke structure. Since I'm not 100% sure if my results are ...
0
votes
1answer
54 views

A linear temporal property that represents this (basic) execution?

A question gives me a set of atomic propositions AP = {a, b, c}and asks me to give a linear temporal property that represents all executions over AP such that: (1) ...
2
votes
1answer
672 views

CTL vs LTL - when a formula satisfy a model

I'm trying to understand the difference between LTL and CTL. In particular, i'm trying to understand when a model (a transition system eg. Kripke structure) satisfy a formula. This is my point of view:...
0
votes
1answer
417 views

Given this transition system, for which states are these (very basic) LTL formulas fulfilled?

I missed a lot of lectures for this module due to surgery so I'm trying to teach it to myself now. This is the question I've been working on: First of all, would I be correct in saying that the LTL ...
2
votes
1answer
874 views

Proving Linear Time Temporal Logic formula □ ◊ f ⇔ ◊ □ f

I am new to this topic, Linear Time Temporal Logic and I am trying to prove this equivalence -- $\Box\Diamond f \Leftrightarrow \Diamond\Box f$ This is my take -- Basic definitions: $(\sigma, j) \...
2
votes
1answer
372 views

Transition systems that satisfy LTL but not CTL, and vice versa

I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...