Skip to main content

All Questions

Filter by
Sorted by
Tagged with
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 ...
user avatar
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
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 ...
yraj429's user avatar
  • 41
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
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
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 ...
pblass's user avatar
  • 55
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 ...
Don Fanucci's user avatar
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$ ...
Meowth8743's user avatar
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 ...
user_1_1_1's user avatar
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 ...
jack malkovick's user avatar
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?
root's user avatar
  • 13
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 ...
LTL's user avatar
  • 11
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 ...
Amir-Mousavi's user avatar
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^...
comrade's user avatar
  • 27
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 \...
Amir-Mousavi's user avatar
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 ...
Pieter Verschaffelt's user avatar
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 ...
Mad A.'s user avatar
  • 143
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 ...
eyes enberg's user avatar