4
votes
Accepted
How to express the existence of winning strategy of the starter of a game in temporal logic?
I don't think it's possible in CTL nor LTL to model two competing players.
You would probably need ATL (Alternating-time Temporal Logic). In ATL, the formula $\langle\langle A \rangle\rangle \phi$ ...
- 15k
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,171
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
What does "AF AX p" mean in CTL?
Your understanding of $AF AX p$ is correct (in my opinion). But whether it seems particularly strange or hard to understand is rather subjective. The argument you quote compares the expressiveness or ...
- 9,471
4
votes
Why is $AF \phi \lor \varphi$ not equivalent to $AF \phi \lor AF \varphi$?
You also need to argue the other way around. "Each path has either $\psi$ or $\varphi$" is not the same as "either each path has $\psi$ or each path has $\varphi$".
- 29.6k
2
votes
Accepted
Intuition behind straight-line programs
A straight-line program is one with no branches, no loops, no conditional statements, no comparisons -- just a sequence of basic operations.
A straight-line program for a finite group $G$ is a ...
D.W.♦
- 154k
2
votes
How to verify a property about a certain order of events in TCTL / UPPAAL?
Under the assumption that your property can be interpreted in an intuitive way, as it is written, it seems that you can formulate it both in LTL, as:
...
- 540
2
votes
Reduce the running by using doubly logarithmic tree
I will assume you are using parallel processing to achieve the advertised runtimes. Say algorithm B scales the size of P by a factor $c<1$. If we apply algorithm B $k$ times, the size of our ...
- 340
2
votes
Accepted
Least fix point of CTL formula
They actually start by proving that $[[E(\varphi U\psi)]]=\bigcup\limits_{k\ge 1}G^k(\emptyset)$.
You can see (or prove by induction for the general case) that repeated applications of $G$ starting ...
- 13.3k
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
CTL trouble translating text into formula
$\newcommand{AF}{\text{AF}\;}\newcommand{AG}{\text{AG}\;}$Try to decode this:
For each path:
In the future: p and
In the future q and
Always in the future not p
You correctly concluded that the ...
- 15k
1
vote
Accepted
$Sat(EG^2\alpha)$ as a fixpoint of an operator
Let us prove that $EG^2\alpha$ is the greatest fixpoint of $\tau(Z):=\alpha\wedge EXEXZ$.
Suppose $s_0\in Sat(\tau(EG^2\alpha))$, then $s_0\in Sat(\alpha)$ and for some path starting at $s_0$, we have ...
- 149
1
vote
Accepted
CTL formula for "for every computation it is always possible to return to the initial state"
$AGF start$ is not a well-formed CTL formula, since in CTL you cannot write GF. Every temporal quantifier must be preceded by a path quantifier.
However, $AGF start$ is a formula in CTL*, so we can ...
- 17k
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
Accepted
Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model
You're correct. Another way to see would be to consider the de-morgan equivalent: $\neg (AF~EG~\neg p)$. To show this invalid, we can show its negation $AF~EG~\neg p$ is valid, which is easier: The ...
- 211
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
Only top scored, non community-wiki answers of a minimum length are eligible