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

learn more… | top users | synonyms (1)

1
vote
0answers
18 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 ...
4
votes
0answers
32 views

The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with below assertions about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
0
votes
1answer
25 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
0answers
18 views

NuSMV : simple game modeling

I'm new to NuSMV and try to model this simple turn-based game. There are 10 bricks in a pile, each player can take 1-3 brick per turn, whoever take the last brick wins the game. Assume player A go ...
0
votes
0answers
17 views

How BDI agent can select next step (action)?

I am reading now about BDI (Belief-Desire-Intention) agents. I guess that this type of agents is the most popular model of cognitive agents and agents of multi-agent systems. Of course I am reading ...
0
votes
1answer
40 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 ...
1
vote
0answers
10 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
38 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) → <>[...
0
votes
0answers
61 views

How to express r-bounded waiting for $r=0,1,2$ in LTL and Promela?

How to express $r$-bounded waiting for $r=0,1,2$ in LTL? I'm having trouble expressing the above in LTL and translating it to Promela. I've already expressed starvation-free and mutual exclusion. ...
2
votes
1answer
147 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
71 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
106 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
0answers
24 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
174 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
94 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
402 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
155 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, ...
0
votes
1answer
143 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 ...
8
votes
3answers
1k 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.) ...
3
votes
3answers
860 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 ...
3
votes
1answer
44 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 ...
2
votes
1answer
151 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 ...
4
votes
2answers
67 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 ...
3
votes
1answer
88 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) \\...
3
votes
1answer
198 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,\ ...
3
votes
0answers
80 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, ...
3
votes
3answers
181 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 ...
3
votes
1answer
134 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}$ ...
24
votes
2answers
639 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 ...
8
votes
1answer
369 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 ...