Share Your Experience: Take the 2024 Developer Survey

# 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.

96 questions
Filter by
Sorted by
Tagged with
8 views

### Counterexample Construction and Translation in CEGAR

As in this slide, M2 is an abstraction of M1 using the abstraction function f1 which essentially groups based on labels. Then we see that the property is not satisfied by the abstraction so we find ...
• 64
15 views

### When does Simulation Equivalent imply Bisimulation

Here, Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?, it is shown that for two LTSs M1 and M2 ...
• 64
14 views

### LTL Model Checking Worst Case size for NBA

I have a slide that gives the worst case time complexity of LTL model checking which uses a product construction of an LTS along with the NBA for the negation of the LTL formula. My question is, when ...
• 64
15 views

### Irregular Safety Properties

A regular safety property is a safety property whose bad prefixes form a regular language, https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec4.pdf. My questions is, are there ...
• 64
121 views

### Can CTL* express every model's behaviour

CTL* as in https://en.wikipedia.org/wiki/CTL*, is a logic that combines CTL and LTL. I know that CTL* can express everything expressible in these two languages and more. My question is whether we can ...
• 64
21 views

### Linear Time properties classification

I know LT Properties can be classified with classes Invariants, Safety Properties, Liveness Properties as in https://en.wikipedia.org/wiki/Linear_time_property. My question is, does this cover all ...
• 64
1 vote
36 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 ...
• 257
73 views

58 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
133 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?
• 39
1 vote
200 views

• 27
177 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.
• 401
1 vote
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 ...
• 519
153 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,075
1k views

• 135
1 vote
350 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)?
833 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 ...
• 742
996 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 ...
• 41
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 ...
• 9,561
249 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 ...
• 163
1 vote
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 ...
• 13