Converting CTL* into a Hesitant Word Automaton

$\newcommand\Dir{\textit{Dir}} \newcommand\Acc{\textit{Acc}} \newcommand{\trans}[3]{#1 \stackrel{\textit{#2}}{\rightarrow} #3}$

(Failed Attempt)

step 1. Normalize general CTL* to the form
$\phi = true | false | p | \neg p | p_1 \land p_2 | p_1 \lor p_2 | A \psi | E \psi \\ \psi = \phi | \psi_1 \land \psi_2 | \psi_1 \lor \psi_2 | X \psi | \psi_1 U \psi_2 | \psi_1 R \psi_2$

where $p_i \in I \cup O$.
The first line ($\phi$) describes state formulas, the second — path formulas. Note that the path formulas cannot be negated — negations can appear only on propositions $I \cup O$.

Can an arbitrary CTL* formula be expressed in the normalized form?
Yes, and this can be done without the exponential blowup. (Since the $R$ operator is dual to the $U$ operator.)

Below we assume that CTL*s are in the normalized form.

step 2. Divide a CTL* $\Phi$ into maximal subformulas. A state formula $\phi$ is a maximal subformula of $\Phi$ if there is no state subformula of $\Phi$ that includes it (subformulas are strict here). Examples: $AGFp \land EGFr \land AFs$ has three maximal subformulas, $AGFp$, $EGFr$, and $AFs$; $A(Xp~U~EFp)$ has two maximal subformulas, $EFp$ and $p$.

step 3. Translation of a CTL* $\Phi$ into an AHW is done bottom-up (inductively):

1. $\Phi = p$ for $p \in O \cup I$:
   if $p \in \sigma$, then $\delta(q,\sigma) = q_\top$, otherwise $\delta(q, \sigma) = q_\bot$.

2. $\Phi = \neg p$ for $p \in O \cup I$:
   if $p \not\in \sigma$, then $\delta(q,\sigma) = q_\top$, otherwise $\delta(q,\sigma) = q_\bot$.

3. If $\Phi = \phi_1 \land \phi_2$, then $\delta(q, \sigma) = \delta_1(q,\sigma) \land \delta_2(q,\sigma)$ for any $q$ and $\sigma$, where $\delta_1$ and $\delta_2$ are transition functions of automata for $\phi_1$ and $\phi_2$.

4. If $\phi_1 \lor \phi_2$, then similarly to the previous.

5. If $\Phi = E \xi$, then:
   • Convert $\xi$ into NBW.

   • The previous step gives NBW with alphabet $\Sigma=2^{max(\xi)}$ and may include state formulas, but we need alphabet $2^{O \cup I}$. Thus first convert all $\max{xi}$ into AHWs, and then adapt $\delta$ to the new alphabet:

     $$\delta(q,\sigma) = \bigvee_{F \in 2^{max(\xi)}} \delta(q,F) \land \bigwedge_{\phi_i \in F} \delta_i(q_0, \sigma) \land \bigwedge_{\phi_i \not\in F} \tilde\delta_i(\tilde q_0, \sigma)$$

     where $\sigma \in 2^{O \cup I}$.

6. If $\Phi = A \xi$, then apply the previous step to $E \neg \xi$ and then dualize the result. Note that $E \neg \xi$ should first be normalized.

Example Consider CTL* $\Phi = A(G(r \rightarrow F g)~U~EGF c)$, where signals $r$ and $c$ are controlled by the environment ($I=\{r,c\}$, $O=\{g\}$).

• step 1: $\Phi$ is already normalized.

• step 2: The maximal subformulas are $EGF c$, $r$,and $g$.

• step 3: build an AHW. First, build the NBT for $\neg\Phi$ with $AP=\{EGF c, r, g\}$, i.e., for
  $\neg(A (G(r \rightarrow F g) ~U~ e)) \equiv \\ E(\neg (G(r \rightarrow F g) ~U~ e)) \equiv \\ E((\neg G(r \rightarrow F g) ~R~ \neg e)) \equiv \\ E((F(r \land G \neg g) ~R~ \neg e))$
  where $e = EGFc$. We do this by creating NBW for $F((r \land G\neg g) ~R~ \neg e)$:

  

  Notation:

  • green edges mean nondeterministic choice, green states — visit these states infinitely often (Buechi acceptance), the bold state is initial.
  • in NB automata edges leading to $q_\bot$ are not shown, and in UC automata edges leading to $q_\top$ are not shown.

  The alphabet of the NBW contains $EFG c$, so we first convert it into an AHW:

  

  Now we merge the previous automaton with these ones and thus adapt the alphabet to $\{g, r, c\}$:

  

  (Note that in the connection points (red points) two edges are connected with “&”.)

  Finally, we dualize the above automaton and get the result:

  

  Notes:

  • Dualization turned green states/edges into red ones.
  • Operator “&” turned into “||”.

NO!NO!NO!NO!NO!NO!NO!NO!NO!NO!NO!NO!NO!

This does not work, because the resulting transitions should be equivalent to the original, but they differ. Consider:

versus

They differ! (e.g., $(\bar{c}r,\bar{e_0})$ satisfies the first but not the second.