Skip to main content
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$ ...
Pål GD's user avatar
  • 16.1k
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 ...
Sandro Lovnički's user avatar
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 ...
Klaus Draeger's user avatar
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 ...
hengxin's user avatar
  • 9,551
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$".
Hendrik Jan's user avatar
  • 30.7k
3 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 &...
Shaull's user avatar
  • 17.2k
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.'s user avatar
  • 159k
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: ...
ivcha's user avatar
  • 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 ...
HackerBoss's user avatar
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 ...
Ariel's user avatar
  • 13.4k
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 ...
Shaull's user avatar
  • 17.2k
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 ...
Pål GD's user avatar
  • 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 ...
Shaull's user avatar
  • 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)'$.
SimonJ's user avatar
  • 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 ...
alias's user avatar
  • 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 ...
chi's user avatar
  • 14.6k

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