All Questions
Tagged with linear-temporal-logic temporal-logic
18 questions
1
vote
2
answers
79
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 ...
- 271
2
votes
1
answer
139
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$ ...
- 23
2
votes
2
answers
132
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 ...
- 55
1
vote
1
answer
191
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?
- 13
0
votes
1
answer
459
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^...
- 27
2
votes
1
answer
893
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 ...
- 752
4
votes
1
answer
1k
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
2
votes
2
answers
263
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
0
votes
1
answer
251
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 \...
- 268
0
votes
1
answer
714
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 ...
- 268
1
vote
1
answer
315
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 ...
- 11
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 ...
- 53
15
votes
1
answer
881
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 ...
user33772
0
votes
1
answer
688
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 ...
0
votes
1
answer
549
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 ...
- 143
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:...
- 155
0
votes
1
answer
1k
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 ...
- 303
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) \...
- 541