9

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


8

You are not missing anything. These expressions are indeed not equivalent. Assume $f$ in your case is an atomic proposition. Then the computation: $f,\neg f,(f,\neg f)^\omega$ satisfies $□◊f$, but not $\Diamond \square f$. Intuitively, $\Diamond \square f$ means "After a finite prefix, there is always $f$", while $\square \Diamond f$ means: "There are ...


6

The models of an LTL formula $\varphi$, with atomic propositions $P$, are infinite words $w = \sigma_0\sigma_1\ldots$, where each $\sigma_i$ is a subset of $P$. To recognize such words, the edges of an automaton recognizing the language of $\varphi$ generally have to be labeled by symbols in $2^P$ (i.e. subsets of $P$). Often multiple transitions are ...


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

There has been some relatively recent work on constructive/intuitionistic variants or interpretations of LTL. Kojima's and Igarashi's Constructive Linear-Time Temporal Logic: Proof Systems and Kripke Semantics is a decent place to start and references a bit of earlier work. In particular, Maier's Intuitionistic LTL and a New Characterization of Safety and ...


5

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


5

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 equivalence. Let's look at (1). You got to the formula $true{\bf U} (\psi\vee \neg \phi)$. Now, this holds in a computation $\pi$ iff there exists $i\ge 0$ such that $\...


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


5

You are certainly right that the level of rigor found in old papers making such claims can be a bit low at times when viewed from today's perspective. The claim is correct anyway, even if it does not follow from Sistla/Clarke's proof. The reason is that LTL satisfiability checking is also PSPACE-complete. You can see satisfiability checking as a special ...


4

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.


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


4

\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{(neg near var)}\\ &\equiv \Diamond (\neg \varphi \lor \psi) &&\text{(grouping $\Diamond$)}\\ &\equiv \neg (\neg \varphi \lor \psi) U (\neg \varphi ...


4

This is only a partial answer (as I believe that the state of the art is insufficient to answer your questions completely - I am happy to be proven wrong here), but I hope that it helps you anyway. First of all, note that when taking the conjunction of two automata with $n$ and $m$ states, the result having $nm - o(n) - o(m)$ states cannot be avoided. This ...


4

You can define syntactic fragments of LTL that ensure that all properties expressible in these fragments are representable as DBAs. An example is given in the paper "A LTL Fragment for GR(1)-Synthesis". Also, the common fragment of ACTL and LTL only contains properties that are representable as DBAs. But note that such a fragment will never be complete in ...


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

Think about what the formula means. The first part says that it's always true that $P$ implies $Q$; the second part says that, if $P$ is true somewhere, then $Q$ must be true somewhere, too. Well, if $P$ implies $Q$ then, if $P$ is true somewhere, then $Q$ had better be true in that place, too!


4

Since Büchi automata are strictly more expressive than LTL, such a translation is not possible in the general case. For instance, the language $L = \{w_0 w_1 w_2 \ldots \in (2^{\{a\}})^\omega \mid \exists^\infty i \in \mathbb{N}. w_{2i} = \{a\} \}$ is representable by a Büchi automaton with 3 states, but is not expressible in LTL as it is a counting ...


3

Let us try to prove that $F(\neg a \vee b) \rightarrow a\,\mathcal{U}\,(b \vee \neg a)$ is a tautology. For this, we have to show that every word that is a model of $F(\neg a \vee b)$ is also a model of $a\,\mathcal{U}\,(b \vee \neg a)$ Let $i \in \mathbb{N}$ be the least index of the word for which we have $w^i \models (\neg a \vee b)$, where $w^i$ denotes ...


3

It's implication as indicated in en.wikipedia.org/wiki/List_of_mathematical_symbols


3

Consider a nondeterministic Büchi automaton $\mathcal{A} = \langle \Sigma, Q, q_0, \delta, \alpha\rangle$. The acceptance condition of $\mathcal{A}$ is a subset of states $\alpha\subseteq Q$, and an infinite run $r = q_0, q_1, q_2, \ldots$ over an infinite word $\sigma_1\sigma_2\cdots $ is accepting iff $r$ visits a state in $\alpha$ infinitely many times. ...


3

LTL is less expressive than $\omega$-regular expressions. For example, the expression $$((a+b)b)^\omega$$ i.e. "there is $b$ in all the even places" cannot be expressed in LTL. In addition, observe that checking whether an $\omega$ regular expression is expressible in LTL is harder than checking universality, which is PSPACE hard. However, there are ways ...


3

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.


3

It is correct that writing the Buchi automaton to memory takes exponential space.....which is why you don't do that. The construction for the Buchi automaton is however very regular and can be done in a forward manner. This allows you to construct it on-the-fly while you search for an accepting lasso in the product between the Buchi automaton and $T$. In ...


3

There are languages that are representable by an LTL formula but by no deterministic Büchi automaton (DBA). Thus a translation from LTL to DBA cannot exist. An example is the formula $\mathbf{F}\mathbf{G} a$, which states that from some moment on $a$ has to hold forever. A nondeterministic Büchi automaton can guess when this moment occurs. No deterministic ...


3

The important thing that is missing from your question is how you model your program, and specifically, what are the atomic propositions you allow. If your atomic propositions are "y=0",...,"y=8", and your transition system is modeled accordingly, then the formula $FX y=8$ means the eventually, the next position would have "y=8". Note that this is ...


3

Unfortunately, the approach of constructing automata for each formula and testing their equivalence is pretty much the best you can do. The problem of checking whether an LTL formula is valid, that is, whether it is satisfied in every computation, is PSPACE complete (this is an easy exercise, given that LTL satisfiability is PSPACE complete). Thus, checking ...


2

You could build a Büchi automaton, but that might be harder than just understanding the formulas. Let's consider the first formula: $$(\diamond\square p \wedge \diamond \square q)\to\diamond\square(p\wedge q)$$ In the left hand side of the "$\to$", consider the expression $\diamond\square p$, which reads "eventually always $p$". Thus, the entire left hand ...


2

The property "always eventually main terminates" should be expressible and verifiable in a bounded model checker. For such properties, the model checker would either verify the property or find a "acceptance cycle" that shows that there exists a loop in an execution trace that does not satisfy the property (by considering execution traces of bounded lengths)....


2

Initial states are somewhat of an anomaly. A similar problem is encountered in the $X$ operator when you try to define LTL over finite words. That is, it somehow would have made more sense to define PLTL over computations that are "infinite on both sides". So, being an anomaly, it is probably easiest to treat it as such, and just explicitly deal with the ...


2

There is no precise answer to this. The smallest GBA for a given language is never larger than the smallest BA for a given language, simply by the fact that BAs are a special case of GBAs. It is easy to construct a language for which smaller GBA exist. Example would be (in LTL) $\mathsf{GF}(a \wedge b) \wedge \mathsf{GF}(a \wedge \neg b) \wedge \mathsf{GF}(\...


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