5
votes
Accepted
Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators
In order to prove the equivalence of two formulas $\phi,\psi$, it is enough to show that for every computation $\pi$, it holds that $\pi\models \phi$ iff $\pi\models \psi$. This is semantic ...
- 17k
5
votes
Linear Temporal Logic (LTL) Syntax Infinitely Often
Consider just $Fx$. It means that at some point in time, say $t_k$, from the perspective of current moment $t_0$, $x$ will be true. After this moment, $x$ may never again be true. Specificaly, at the ...
- 1,191
4
votes
Accepted
How do you correctly write this sentence as a CTL formula?
You can learn a lot about CTL at Wikipedia page.
The sentence you need to write, expressed more closely in the vocabulary of CTL operators, would be
Along all paths starting from current state, it ...
- 1,191
4
votes
Accepted
What's the definition of ACTL?
ACTL is the universal fragment of CTL.
Thus, existential path quantification is not allowed.
So a path formula is of the form $AF\psi$, $AG\psi$, or $AX\psi$ (or a conjunction or disjunction of path ...
- 17k
4
votes
Accepted
What are the differences between propositional logic and temporal logic?
An interpretation in propositional logic consists of assigning a truth value to every variable. In contrast an interpretation of, say, LTL consists of assigning a truth value to every variable at each ...
- 275k
4
votes
Accepted
CTL* query evaluation order
Your interpretation of the $G$ modality is incorrect; it does not inherently talk about all paths. In particular, the example you give specifies that there is a path such that from some point on, all ...
- 2,178
4
votes
Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators
\begin{alignat*}{2}
\Box \varphi \to \Diamond q
&\equiv \neg \Box \varphi \lor \Diamond \psi &&\text{($\to$ elim)}\\
&\equiv \Diamond \neg \varphi \lor \Diamond \psi &&\text{(...
- 41
3
votes
Accepted
Temporal logic - mixing AF and AG in CTL formula
Does it mean that: 1. or 2. or 3.?
Your second interpretation is correct: $\varphi_1 \rightarrow AG(\varphi_2)$ is a CTL state formula, and to check whether it is satisfied by a state $s$, the path ...
2
votes
Accepted
distinguishing between CTL* formulas $A[FG p]$ and $AFAG p$ using transition system
(This is the "standard" example which proves that CTL is not a superset of LTL, in terms of expressiveness)
Consider this system:
state $q0$, transitions to $q0$ and $q1$
state $q1$, transition to $...
- 14.4k
2
votes
How to graph search a LTL-generated Buchi automaton to generate valid execution paths
I would interpret your problem as follows:
Given a non-deterministic Büchi automaton representing some language $L$, you want to enumerate all shortest good prefixes of $L$ such that in every ...
- 2,732
2
votes
Accepted
Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$
If you're just asking for any model satisfying the formula, you simply try to make one of these the case
The left hand side false
The right hand side true
Let's just pick number 2. You have to make ...
- 15.5k
2
votes
Accepted
LTL globally implies
You seem to be pretty confused, so let's sort some things out.
First, it's "implies", not "replies". That is, the formula $\phi\implies \psi$ means that if $\phi$ holds, then $\psi$ holds.
To be more ...
- 17k
2
votes
Accepted
Difference between CTL and CTL*
First, let's see a formula that's in CTL$^*$ but not in CTL:
$EGFp$. That is, there exists a path with infinitely many $p$'s.
One intuition (and this is by no means a formal argument) is that the &...
- 17k
2
votes
Accepted
Given LTL formulas $m$ and $p$, is there a tool that can check whether $m \models p$ does hold?
Yes, you can use an LTL-to-Büchi-automaton translator for this.
Let's assume that you want to check if $\psi \rightarrow \psi'$ is a valid LTL formula, i.e., every word satisfying the LTL property $\...
- 2,732
1
vote
Logics for multi-agent and distributed systems and algorithms
TLA+ is commonly used for verification of distributed algorithms. I've seen it actively used by researchers and industry engineers/architects.
1
vote
What is the Kripke semantic for a linear temporal logic?
tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind.
Details:
Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
- 663
1
vote
Accepted
Which temporal logic is the one described in Manna & Pnueli's "The Temporal Logic of Reactive and Concurrent Systems: Specification"?
LTL.
PS The very book you mention has a historical note section discussing various other temporal logics near page 271.
Edit (leaving the above intact for the comments to make sense): None of the ...
- 663
1
vote
Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$
General notes on LTL
Intuitively, LTL formulas are statements about infinite sequences (or "infinite words"). First, you have to understand what these sequences consist of.
In the usual definition ...
1
vote
Accepted
Prove that $\text{EF p}$ can't be written in LTL
There is a delicate point here, about the semantics of LTL vs CTL.
Given a formula $\psi$ in LTL, we say that it holds in a structure $K$ if every path in $K$ satisfies $\psi$.
In CTL, however, the ...
- 17k
1
vote
LTL Logic Finally, Globally and Until to irreflexive Version
Sorry, I misread your question at first as wanting to express the irreflexive variant using the reflexive variant (which could be done with the next operator). You don't actually need the next for the ...
1
vote
Semantics of E and A operators in CTL*
I believe it means that $\sigma,\sigma$ should share the same prefix up to position $i$.
Then the quantification ranges over all possible extensions of this prefix from state $\sigma(i) = \sigma(i)'$.
- 134
1
vote
Reasoning about resources: "resource logics"?
Just learned about Bunched Logic which seems to fit the bill too.
- 2,163
1
vote
Reasoning about resources: "resource logics"?
Do you mean a resource-aware logic?
If so, yes, there's linear logic [Girard, 1987] (as was already noted in the comments). It has had a big influence on the study of concurrency and implicit ...
- 171
1
vote
Linear Temporal Logic, Idempotent law
Also by definition of $G$, some formula holds in every state.
Well, $\sf true$ holds in every state. I'm unsure about why you mention $G$ here.
So if globally $\phi$ holds until we see $\psi$ does ...
- 14.4k
1
vote
Can the foundation of computer science be implemented to include new rules of inference so that computer can do causal reasoning?
This is a hot topic at the moment. Read this recent paper by Judea Pearl for example. In general, ML and AI are not very good at causal inference at the moment, because it requires a symbolic ...
- 111
1
vote
Given two formulae E[G F p] (which is CTL*) and EG EF p ( which is a CTL) with a Model prove that they are not equivalent
Consider a system with 3 states, $s_1,s_2,s_3$ and the following transitions:
$s_1\to s_1$, $s_1\to s_2$, $s_2\to s_3$ and $s_3\to s_3$.
The state $s_2$ is labelled $p$.
Clearly $E[GF p]$ doesn't ...
- 17k
1
vote
Accepted
Counterexample for LTL - CTL equivalence
Consider the following model: you have 3 states, $s_0,s_1,s_2$ with the transitions: $s_0\to s_0$, $s_0\to s_1$, $s_1\to s_2$ and $s_2\to s_2$ and the labels are $L(s_0)=\{p,q\}$, $L(s_1)=\emptyset$ ...
- 17k
Only top scored, non community-wiki answers of a minimum length are eligible