# Tag Info

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$ ...
• 16.1k
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
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

### 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,551

### 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$".
• 30.7k
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 &...
• 17.2k
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 ...
• 159k

### 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

### 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 ...
• 350
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.4k
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 ...
• 17.2k
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 ...
• 16.1k
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 ...
• 17.2k
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.6k

Only top scored, non community-wiki answers of a minimum length are eligible