AGV 5.3 -- Complement Büchi Automaton with Odd Ranking

Notes > UdS AGV

Created At : 2024-11-22 16:36

Count:1.4k Views :

Comment:

Introduction
Level Ranking
1. $\ell’$ covers $\ell$ ?
Complement Automaton Construction

Previous chapter: Ranking of DAG

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Introduction

In section 4.2, we have shown the complementation construction for deterministic Büchi Automata.

Now, by using DAG we can construct complement automaton of any Büchi Automata, with the help of the definition of odd ranking and the new function Level Ranking.

Level Ranking

$\textbf{Definition 5.3. }\text{(Level Ranking). Consider a Büchi Automaton }\mathcal{A}=(\Sigma,Q,I,T,\small\text{BÜCHI}\normalsize(F)).\newline\text{A level ranking }\ell\text{ is a pair }(S,g)\text{ such that:}$
$\begin{array}{l}
\hspace{1cm} \cdot \ S\subseteq Q,\newline
\hspace{1cm} \cdot \ g:S\rightarrow\lbrace 0,\dots,2|Q|\rbrace\text{ with }g(q)\text{ necessarily even if }q\in F.\end{array}\newline \ \newline\text{We also denote: }$
$\begin{array}{lll}
\hspace{1cm} \cdot \ \textsf{Lvlrks}&=&\text{the (finite) set of level ranks, and }\newline
\hspace{1cm} \cdot \ \textsf{Initrks}&=&\text{the set of level ranks s.t. }S=I\end{array}\newline \ \newline
\hspace{1cm}\text{We say that a level ranking }\ell’\text{, given by }(S’,g’)\text{ cover }\ell\text{, given by }(S,g)\text{ for }\sigma\in\Sigma,\newline\text{if }S’=\lbrace q’\mid(q,\sigma,q’)\in T\rbrace\text{ and for all }q\in S,q’\in S’\text{ with }(q,\sigma,q’)\in T\text{, it holds that } g’(q’)\leq g(q).$

Here, the level ranking refers to a pair that contains set of states that share the same ranking.

$\ell’$ covers $\ell$ ?

The last part of the definition states that one level ranking is covering the other if the following satisfied:

Let $\ell’=(S’,g’)$ and $\ell=(S,g)$ for $\sigma\in\Sigma$
$q$ are the states that in the set $S$, so as $q’$ are in $S’$
All states $q’$ are some successors of some states $q, \ (S’=\lbrace q’\mid(q,\sigma,q’)\in T\rbrace)$
for all $q\in S,q’\in S’, (q,\sigma,q’)\in T$, the rank of $q’$ is lower than $q, \ (g’(q’)\leq g(q))$

That means the whole level’s successors will never have higher rank than itself.

Complement Automaton Construction

By lemma 5.1, we know that a word $\alpha$ that is rejected by $\mathcal{A}$ has an odd ranking on the run DAG of $\mathcal{A}$ on $\alpha$.
Now our complement will do the opposite: it only accepts the word that has odd ranking.

To achieve this, we construct the odd ranking, level by level, by assigning ranks to vertices.
The definition of level ranks and covering for a letter ensure that the requirements of a ranking are satisfied.

Through the acceptance condition, we ensure that the ranking is odd, i.e., there is no infinite path that consists only of even-ranked vertices.

$\textbf{Construction 5.1. }\text{Given a Büchi Automaton }\mathcal{A}=(\Sigma,Q,I,T,\small\text{BÜCHI} \normalsize(F))\text{ that recognizes}\newline\text{the language }L\text{, we construct a Büchi Automaton}$ $$\newline \mathcal{A’}=(\Sigma,\textsf{Lvlrks}\times\textsf{OnEvenPath},I’,T’,\small\text{BÜCHI}\normalsize(F))$$ $\text{that recognizes the language }\Sigma^\omega\setminus L\text{ as follows.}$
$\begin{array}{lrl}
\hspace{0.5cm} \cdot &\textsf{OnEvenPath} = & 2^Q, \text{tracking states in the current level,} \newline
\hspace{0.5cm} \cdot &I’= & \lbrace (\ell,R) \mid \ell \in \textsf{InitRks, } \ell \text{ is given by } (S,g) \text{, and } R = \lbrace q \mid g(q) \text{ is even} \rbrace \rbrace \newline
\hspace{0.5cm} \cdot &T’= & \textsf{NewEvenPaths} \cup \textsf{ContinueEvenPaths}, \text{ where} \newline
\hspace{0.5cm} && \hspace{0.9cm}\textsf{NewEvenPaths}=\lbrace ((\ell,\varnothing),\sigma,(\ell’,R’)) \mid \ell’ \text{ covers } \ell \text{ for } \sigma, \newline
\hspace{0.5cm} && \hspace{4.8cm} \ell’ \text{ is given by } (S’,g’), \newline
\hspace{0.5cm} && \hspace{4.8cm} \text{and } R’ = \lbrace q’ \mid g’(q’) \text{ is even} \rbrace \rbrace \newline
\hspace{0.5cm} && \textsf{ContinueEvenPaths} = \lbrace ((\ell,R),\sigma,(\ell’,R’)) \mid R \neq \varnothing, \ell’ \text{ covers } \ell \text{ for } \sigma,\newline
\hspace{0.5cm} && \hspace{4.8cm} \ell’ \text{ is given by } (S’,g’)\text{, and}\newline
\hspace{0.5cm} && \hspace{4.8cm} R’ = \lbrace q’ \mid (q,\sigma,q’) \in T, q \in R, \text{ and } g’(q’) \text{ is even} \rbrace \rbrace \newline
\hspace{0.5cm} \cdot &F’ = & \textsf{Lvlrks} \times \lbrace \varnothing \rbrace.
\end{array}$

Explanation

$Q’ = \textsf{Lvlrks}\times\textsf{OnEvenPath}:$ all states contain their level ranking and set of all states that is tracked currently (states would be dropped if it leads to odd-ranked vertex).

$I’:$ The initial state contains the initial level ranking ($\textsf{Lvlrks}$), and the set of all even ranking states ($R$).

$T’:$ We have transitions $\textsf{NewEvenPaths}$ and $\textsf{ContinueEvenPaths}$. Both share some properties in common.

all the states are covered by their successors,
their successors only keep track on even ranking states,
$\textsf{ContinueEvenPaths}$ requires that the current states must keep track on even ranking states already

$F’:$ Accepting states are those has no infinite path that consists only of even-ranked vertices.(odd ranking).

Proof

Now we can try to verify the Lemma with our construction:

$\textbf{Lemma 5.2. }\textit{The automaton of Construction 5.1 has an accepting run on input }\alpha\newline\textit{if and only if the run DAG of }\mathcal{A}\textit{ on }\alpha\textit{ has an odd ranking.}$

The run of the automaton on the input word builds a potential ranking, level by level. Note that the level-by-level guessing of the ranking is the only source of non-determinism. But if the guess is indeed an odd ranking, then the automaton has a unique run.

In the construction, we used level rankings to ensure the definition of ranking is satisified, so instead of verify whether it is odd ranking, we only need to verify that in the guessed ranking, there is no infinite path of even-ranked vertices.

At any given point, the second component ($\textsf{OnEvenPath}/R$) in the state of the constructed automaton tracks a “batch” of paths that traverse solely through even-ranked vertices. Paths that hit an odd-ranked vertex are dropped from the batch. The acceptance condition enforces that every batch that is followed must be eventually be emptied.

Odd ranking = no infinite path of even-ranked vertices = eventually every batch are emptied

So we can rephrase the lemma as “The run is accepting if and only if eventually every batch are emptied“.

If the run is accepting, then eventually every batch are emptied

This condition is clearly necessary for the guessed ranking to be odd: if there is eventually a batch that is never emptied, this corresponds to an infinite path of even-ranked vertices in the run DAG, violating requirement 3 (The rank cannot increase upon traversing an edge).

Why? Because as long as we have one empty batch, the ranking of that batch will definitely be hihger than the those which are not empty (consider the definition of rank function and pruning), and any states will never have high rank than their successors.

If eventually every batch are emptied, then the run is accepting

Assume we have non accepting run that have emptied batch, which means there is an infinite path of even-ranked vertices in the run DAG.

Now suppose this run has the batch-tracking set $\textsf{OnEvenPath}$ is emptied infinitely often. That means in the infinite path of even-ranked vertices there is an level $n$ so that $\textsf{OnEvenPath}$ is emptied at step $n$.

Because this is an infinite path of even-ranked vertices, once $\textsf{OnEvenPath}$ is emptied at step $n$, the next transition will be $\textsf{NewEvenPath}$. Which means there is a successor in level $n+1$ that has an even rank.

Since the path is infinite, subsequent transitions will be $\textsf{ContinueEvenPaths}$, and the even-rank vertices will be remained in the set of $\textsf{OnEvenPath}$. Which contradicts that the run have emptied batch. Therefore this non accepting run that have emptied batch do not exist.

Next chapter: Linear-Time Temporal Logic (LTL)