Converting CTL* into a Hesitant Automaton


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

We will convert a given CTL* formula into an alternating hesitant tree automaton (AHT). We assume that the CTL* formula talks about propositions from $I$ and directions $O$. In contrast to the original conversion from Vardi’s paper, we allow CTL* to talk about directions — thus below propose a modified construction.

CTL* with inputs

Syntax of CTL* with inputs

  • state formulas:
    \(\psi = true | false | o | \neg o | \psi_1 \land \psi_2 | \psi_1 \lor \psi_2 | A \pi | E \pi\)
    where $o \in O$.

  • path formulas:
    \(\pi = \psi | i | \neg i | i_1 \land i_2 | i_1 \lor i_2 | \pi_1 \land \pi_2 | \pi_1 \lor \pi_2 | X \pi | \pi_1 U \pi_2 | \pi_1 R \pi_2\)
    where $i \in I$.

Furthermore, we define state-input formulas. State-input formula is a boolean formula over state formulas and inputs.

Semantics of CTL* with inputs

Satisfaction of state formulas is defined wrt. states and is standard, the satisfaction of path formulas is defined wrt. infinite paths and is almost standard with the exception of the new cases involving inputs, so we clarify the case of $i$ — the rest follows: given an infinite path $\pi = s_1 i_1 s_2 i_2 …$, $i \models \pi$ iff $i \in i_1$.

System satisfies a state formula iff all its initial states satisfy it.

Note You cannot write $sys \models i\land o$, since $i \land o$ is a path formula (provided $i \in I$, $o \in O$).

Note The above grammar describes the positive normal form CTL*. The general CTL* (in which negations can appear not only in front of inputs or outputs) can be converted into a positive normal form formula of the same size (since $\neg (\pi_1 U \pi_2) \equiv \neg\pi_1 R \neg\pi_2$).

Conversion

An AHT is a tuple $(\Sigma = 2^O, \Dir = 2^I, Q, q_0, \delta: Q \times \Sigma \to \mathcal{B}^+(Q\times \Dir), \Acc)$ with some restrictions on $\delta$ and $Acc$ (see Vardi’s paper).

The conversion steps are:

step 1. Convert a given CTL* into the positive normal form.

step 2. Divide a CTL* $\Phi$ into maximal subformulas. A state-input formula $\phi$ is a maximal subformula of $\Phi$ if there is no state-input 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 AHT is done bottom-up (inductively):

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

  2. $\Phi = \neg p$ for $p \in O$:
    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.

    • Extend the NBW $(2^{max(\xi)}, Q, q_0, \delta_w: Q \times 2^{max(\xi)} \to 2^Q, \Acc)$ to NBT $(\Sigma=2^{max(\xi) \setminus I}, \Dir=2^I, \delta: Q\times\Sigma \to \mathcal{B}^+(\Dir \times Q), \Acc)$. It is possible that $max(\xi) \cap I$ is nonempty so we remove inputs from the alphabet:

      \[\delta(q,\sigma) = \bigvee_{d_w \in 2^{I \cap max(\xi)}}\bigvee_{d \in 2^{I \setminus max(\xi)}}\bigvee_{q' \in \delta_w(q,d_w\sigma)} (d_w d,q')\]

      where $\sigma \in 2^{max(\xi)\setminus I}$.

    • The previous step gives NBT with alphabet $\Sigma=2^{max(\xi)\setminus I}$, but we need alphabet $2^O$. Thus we adapt $\delta$ to the new alphabet:

      \[\delta(q,\sigma) = \bigvee_{F \in 2^{max(\xi) \setminus I}} \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$. At this point we should already have automata for subformulas from $max(\xi)\setminus I$ computed.

  6. Finally, 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 a hesitant automaton. 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)$:

    and then by replacing all edges with “superedges” that express $\exists dir$, where $dir \in I$, thus we get an AHT:

    Notation:

    • green edges mean nondeterministic choice, green states — visit these states infinitely often (Buechi acceptance), the bold state is initial.
    • e.g., “c&Er” encodes edges with directions $\{cr,c\bar{r}\}$.
    • in NB automata edges leading to $q_\bot$ are not shown, and in UC automata edges leading to $q_\top$ are not shown.

    Now we need to adapt the alphabet $\{e, g\}$ to $\{g\}$. Since $e = EGF c$, we first translate $EFG c$ into NBW:

    and then into NBT (NBT for $e$ is on the left, UCT for $\neg e$ is on the right):

    The final AHT is:

    In the above figure we have special red dots with an outgoing arrow — this means that the edge transition should be conjuncted with the edges from state “~e0”.

    To get the automaton for the desired negation of $E((F(r \land G \neg g) ~R~ \neg e))$, we dualize it:

    Notes:

    • Dualization turned green states/edges into red ones.
    • The sign “&” turned into “||”.
    • “~e” turned into “e” — this is because the dualization of the automaton for “~e” gives the automaton for “e”.

Self-check Let’s check that the automaton from the example accepts “good” trees and rejects “bad” ones. Consider the trees:

          tree A           tree B          tree C
            g                g              !g   
           /                /               /    
          /r               /r!c            /rc   
        !g                g              !g      
        /                /               /       
       /!r              /r!c            /!rc     
     !g               ...             !g         
     / \                              /          
    /!r \c                           /!rc        
  !g    !g                         !g            
 ...      \                        /             
           \c                    ...             
           ...

Tree A has the prefix $(gr\bar{c})(\bar{g}\bar{r}\bar{c})$ and ends with two infinite branches, $(\bar{g}\bar{r}\bar{c})^\omega$ and $(\bar{g}\bar{r}c)^\omega$ — hence it satisfies $A (G(r \rightarrow F g) ~U~ EGF c)$. The accepting run graph (which is actually a tree) is $q_0 - e_0 - e_0 - e_1^\omega$.

Tree B does not have any branch that satisfy $EGF c$, thus it should not be accepted by the automaton. Indeed, any branch of any run will be trapped in $e_0$ or visit infinitely often $q_0$ or $q_1$, which is not accepting.

Tree C satisfies the formula, since already in the root the $EGF c$ is satisfied. (Actually, this should hold for any “good” tree.) (Note that the very first $r$ is not granted.) The automaton accepts the tree, since the run graph $q_0 - e_1^\omega$ is accepting.

Notes We need to be careful about cases of “disappearing edges”. Here is case 1 (NB):

After considering edges from state $e_0$, the resuling automaton on the right has essentially no outgoing edges.

Here is case 2 (UC):

The edges from the state $e_0$ did not affect the result.

This is not a magic, but rather the application of the formula mentioned before (when adapting the alphabet): \(\delta(q,\sigma) = \bigvee_{F \in 2^{max(\xi)\setminus I}} \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)\)