Skip to main content

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
0 votes
1 answer
92 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
570 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
479 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
286 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
251 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
0 votes
0 answers
250 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 ...
Zeist's user avatar
  • 173
1 vote
0 answers
296 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 ...
LTL's user avatar
  • 11
0 votes
1 answer
238 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.
Perissiane's user avatar
3 votes
3 answers
172 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 ...
Ayrat's user avatar
  • 1,075
2 votes
0 answers
108 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) $...
user avatar
1 vote
1 answer
161 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?
Perissiane's user avatar
0 votes
1 answer
118 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 ...
Svendole's user avatar
7 votes
1 answer
373 views

Non-deterministic Büchi 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 ...
Perissiane's user avatar
2 votes
1 answer
1k 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?
Perissiane's user avatar
2 votes
1 answer
239 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 ...
Ayrat's user avatar
  • 1,075
3 votes
1 answer
886 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 ...
Lee Sleek's user avatar
  • 131
5 votes
2 answers
1k 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 ...
nopekaro's user avatar
1 vote
0 answers
151 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^*...
Zack Newsham's user avatar
1 vote
0 answers
49 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 ...
crazybird's user avatar
14 votes
1 answer
832 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 ...
user avatar
0 votes
1 answer
1k 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 ...
Thang Do's user avatar
  • 219
0 votes
1 answer
670 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 ...
Pieter Verschaffelt's user avatar
2 votes
0 answers
41 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 ...
TomR's user avatar
  • 1,401
-2 votes
1 answer
130 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) → <>[]...
Zac Bagids's user avatar
2 votes
1 answer
465 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 ...
Markus Müller's user avatar
1 vote
2 answers
365 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. ...
Mad A.'s user avatar
  • 143
0 votes
1 answer
536 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 ...
Mad A.'s user avatar
  • 143
0 votes
1 answer
65 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) ...
eyes enberg's user avatar
2 votes
1 answer
1k 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:...
Fabrizio Duroni's user avatar
0 votes
1 answer
939 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 ...
eyes enberg's user avatar
3 votes
1 answer
1k 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) \...
ramgorur's user avatar
  • 541
2 votes
1 answer
620 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, ...
KJ50's user avatar
  • 131
1 vote
1 answer
799 views

Techniques (tools) to convert temporal logic (CTL,CTL* or LTL) to μ-calculus formulae

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
Dimiter's user avatar
  • 129
11 votes
3 answers
3k views

Why use $\mu$-calculus and not LTL,CTL,CTL*?

It is known that the temporal logics LTL,CTL,CTL* can be translated/embedded into the $\mu$-calculus. In other words, the (modal) $\mu$-calculus subsumes these logics, (i.e. it is more expressive.) ...
Dimiter's user avatar
  • 129
5 votes
3 answers
3k views

Howto formally go about proving that two LTL formulas are equivalent?

Do they need to "unwind" exactly to the same set of paths or does it suffice when one set is contained in the other ? Or is it sufficient to argue that M,s satisfies both LTL formulas for any ...
panny's user avatar
  • 153
3 votes
1 answer
56 views

Is there a mistake in the expression for clean behavior in Pnueli's article from 81'?

I am reading an article called The temporal semantics of concurrent programs . On page $9$, there is a small section (numbered as $2$) called "clean behavior". I think that there is a problem with ...
Belgi's user avatar
  • 267
2 votes
1 answer
337 views

Equivalence of logical Formula (Kripke structures)

Can someone explain me how to find if these formulas are equivalent with Kripke structures? AG(Fp or Fq) , A(GFp or GFq) AGF(p and q) , A(GFp and GFq) AFG(p and q) , A(FGp and FGq) Thank you in ...
user8241's user avatar
4 votes
2 answers
101 views

Temporal logic for interface invariants

I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
user1838636's user avatar
3 votes
1 answer
180 views

LTL: Show $\neg(aUb) \Leftrightarrow \neg b U (\neg a \land \neg b) \lor G \neg b$

I got as far as \begin{align} w \vDash \neg (a U b) &\Leftrightarrow \neg (w \vDash a U b) \Leftrightarrow \neg (\exists_{i\geq0} : w^i \vDash b \land \forall_{0\leq k < i} : w^k \vDash a) \\...
hauptbenutzer's user avatar
3 votes
1 answer
899 views

Equivalence of GFp and Gp in LTL

In linear time logic, is $\mathbf{GF}p$ equivalent to $ \mathbf{G}p$ ? $\mathbf{GF}p$ means that it is always the case that p is true eventually. Let $\mathbf{G} p$ be defined as: $\forall j \ge0,\ ...
brabec's user avatar
  • 135
3 votes
0 answers
96 views

Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
reinierpost's user avatar
  • 5,738
3 votes
3 answers
404 views

Why is GFp -> GFq false in LTL, even though GFp and GFq are false?

Consider the Kripke structure: $$ \begin{array}{ccccccc} \to & (p, \neg q) & \to & (\neg p, \neg q) & \to & (\neg p, q) \\ & \circlearrowright & & \circlearrowright ...
dendini's user avatar
  • 31
3 votes
1 answer
504 views

Time to construct a GNBA for LTL formula

I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula: Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
kafka's user avatar
  • 401
33 votes
2 answers
1k views

Equivalence of Büchi automata and linear $\mu$-calculus

It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
Daniil's user avatar
  • 2,197
10 votes
1 answer
893 views

Algorithm to translate a deterministic Büchi automaton to LTL (when possible)

Linear temporal logic and deterministic Büchi automata are incomparable: DBA cannot express $FGa$, and LTL cannot express "at least each odd letter is 'a'". But sometimes it is interesting to know ...
Ayrat's user avatar
  • 1,075

1
2