# Tag Info

8

As for a $\mu$-calculus formula not expressible in CTL*, see this post. As for texts on the subject, you are likely to get further ahead by reading papers, as these topics are not covered in many books. Still, the Handbook of Modal Logic may be a good start. As for papers, try: Expressive power of Temporal Logics This PhD thesis Emerson's Model checking ...

5

For what it concerns LTL, your understanding is almost correct except that there may be more than one initial states in a transition system. An LTL formula $\varphi$ holds in state $s$ of a transition system $TS$ if all paths starting in $s$ satisfy $\varphi$. The transition system $TS$ satisfies an LTL formula $\varphi$ if if all initial paths of $... 5 Technically, LTL and CTL are incomparable in their differentiating power over Kripke structures. So intuitively, it shouldn't be easier to design one or the other. However, most people tend to find it easier to think in linear time. Making sure a certain property holds for all paths is easier than studying a branching-time property. In particular, this is ... 4 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 always has to hold that there exists at least one path where$p$eventually is true. I think you can take it from there, but comment if you have troubles. hint: ... 4 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$says that agent (or coalition)$A$can enforce$\phi$to come about. In your case,$\langle\langle P_1 \rangle\rangle \text{Win}_1$. In modal µ-calculus, it ... 4 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$". 4 You have some misconception regarding transition systems: The alphabet of the system is$2^P$for some set$P$, and paths induce words over$2^P$. In the first system, there is a single path:$(S_0,S_1)^\omega$, and it induces a single word:$(\{a\},\{a,b\})^\omega$. Now, this word satisfies$aUb$, since$a$holds until the secod letter, in which$b$holds.... 4 The$\mu$-calculus is strictly more expressive than LTL, CTL and CTL*. This is a consequence of a few different results. The first step is to show that the$\mu$-calculus is as expressive as temporal logics. The main idea for encoding these logics comes from recognizing temporal properties as fixed points. At a very informal level, least fixed points allow ... 4 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 states on that path satisfy$p$. As you suspect, for CTL* it is in general not possible to use a simple bottom-up evaluation, as you would for CTL, the reason ... 4 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 usability of LTL and CTL, and tries to convince readers that LTL is easier to understand (especially for engineers in practice). In my experience, it indeed ... 3 The set of states satisfying$\exists a U b$is the smallest set$S$such that$S$contains all states satisfying$b$, and$S$contains all states satisfying$a$which have a successor in$S$Note that we specify the "smallest" such set because otherwise you could pick the set of all states, or include arbitrary cycles of$a$-states, etc. Do you see how ... 3 Your answer$Sat(A(a \cup b)) = \{ s_1, s_2, s_3, s_4 \}$is correct. And your conclusion that the model does not satisfy the property is also correct because the initial state$s_0 \notin Sat(A(a \cup b))$. In my opinion, there is a typo in Line 7: $$Q := Q \cup \left( \{ s \mid \forall s' \in Q. (s,s') \in R \} \cap Sat(\phi) \right).$$ According to the ... 3 CTL formulas are always evaluated from the starting state of the Kripke structure. Indeed, CTL stands for computation Tree logic, and the tree in question is the unwinding of the Kripke structure, starting from the initial state. If you want to specify that$EF q$should hold from every (reachable) state, that can be specified as$AGEFq$, which is still a ... 3 First, to answer the question in your question title: the difference between equivalence and implication in CTL formulae is the same as the difference between equivalence and implication in propositional logic, that is,$A \leftrightarrow B$is the same$(A \to B) \land (B \to A)$. But your real question is whether$\mathrm{AG}\,(A \land B)$is equivalent ... 3 You may find an answer or at least relevant references in the article A linear translation from LTL to the fi rst-order modal $\mu$-calculus. 2 It is well known that$\mu$-calculi can express properties that "count modulo a constant", e.g., "all even steps visit a$A$-state" which is captured by something like$\mu X.A \land\Box\Box X$. Such properties cannot be stated with the standard TL modalities Until and Next since these modalities are 1st-order definable. See D. C. Kozen's 1983 article. 2 I'm pretty sure that you need your system to be designed in Promela, rather than Java. You then input the system in Promela, and the specification in LTL (or CTL) to SPIN, which outputs a C code for a model checker for the specific instance. 2 A somewhat late response: The formula$AX(p U q)$is equivalent to the CTL formula$AXA(pUq)$: Consider a state that satisfies the former, then in all the paths from it, after one transition it holds that$pUq$. Thus, in all the paths after one transition, we reach a state from which all the paths satisfy$p U q$, so the state satisfies the latter. The ... 2 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: a => F(b && F(c && F d)) and in CTL, which in the given example is equivalent to TCTL, due to lack of timing constraints (you may assume they are of form [0, inf) and consider a TCTL ... 2 You seem to be stuck, so here is the answer: You want$a$to hold for at least as long as$b$does. The alphabet consists of$2^{\{a,b\}}=\{\emptyset, \{a\},\{b\},\{a,b\}\}$. Rephrasing the condition, it means that$\{b\}$cannot appear before either$\{a\}$or$\emptyset$have appeared. Indeed, this is the only violation of the condition. So once$\{a\}$... 2 A small addendum to @Shaull's anwswer, which is completely correct: for the output (1),$aaaaaaaaa\ldots$, you suggested (if it were possible in your transition system), your assumption that the formula does not hold is correct. The formula$A [a U b]$does not hold on such a path; Wikipedia gives the following definition:$\bigg( (\mathcal{M}, s) \models A[...

2

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 precise, the formula $\phi\implies \psi$ is true in one of two cases: either $\phi$ is false, in which case we say that the implication is vacuously true, or ...

2

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 straight-line program in a very simple language with an unlimited number of registers $r_1,r_2,r_3,\dots$ and with only two legal operations: $r_i := \text{inverse}(... 1$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 ask your question about CTL*: Is the formula$AGFstart$equivalent to$AGEFstart$? The answer to this question is no. The first formula says that in every ... 1 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 formula$AF~EG~\neg p$says on all paths starting at$s_0$, we eventually get to a state such that there is a path where$\neg p$holds forever. And indeed that ... 1 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 problem will be$c^kn$. This will require time$$\sum_{i=0}^{k-1}O(\log(c^in)/\log(\log(c^in)))=\sum_{i=0}^{k-1}O\left(\frac{i\log c+\log n}{\log(i\log c+\log n)}\... 1 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 with the empty set yields:$G(\emptyset)=[[\psi]]$,$G^2(\emptyset)=[[\psi]]\cup ([[\varphi]]\cap pre_\exists([[\psi]]))=[[\psi]]\cup\left\{s\in S | s\in[[\...

1

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 it make every state after it true? A state can not be true or false, like 42 can not be true or false. This is meaningless. is it correct to say that also $... 1 For the answer$\forall \lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$: I think you have got the right idea. However, this formula is not in CTL since$\lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$is not a path formula. By$\forall \lnot \exists \left( \left( \lnot a \right) \bigcup b \right)$, I think you want to say$\...

1

The semantics of the "Until" operator allows for the eventuality to be satisfied immediately. That is, $pUq$ holds both in the computation $ppppq$, but also in $q$. Thus, in your formula, the eventuality is satisfied immediately in states $s_1,s_3$, and satisfied within 1 step in $s_2$. But all of them satisfy it.

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