Ericpony's Blog: February 2013

Tuesday, February 19, 2013

$\omega$ -automata are finite state automata interpreted on infinite words. Non-deterministic

$\omega$ -automata are quintuples

$(Q,\Sigma,I,T,\mathcal F)$ , where

$Q$ is a finite set of states,

$I$ is a non-empty set of initial states,

$T:Q\times\Sigma\times Q\to Q$ is a transition relation, and

$\mathcal F$ is an acceptance condition.
The Rabin condition is in form of

$\mathcal F=\{(A_i,R_i):i\in J\}$ , and run is accepting iff there exists

$j\in J$ such that it visits

$A_j$ i.o. but visits

$R_i$ only finitely many times.
The Streett condition is

$\mathcal F=\{(A_i,R_i):i\in J\}$ such that a run is accepting iff there exists

$j\in J$ such that it visits

$A_j$ i.o. or visits

$R_i$ only finitely many times.
The parity automata are

$\omega$ -automata with a priority function

$p:Q\to [c]$ for some

$c\in\mathbb N.$ A run

$\pi$ is accepting iff

$\lim\sup p(\pi(n))$ is even. Parity automata can be simulated by

$\omega$ -automata with the Rabin acceptance conditions: just define

$J:=\mathbb N$ ,

$A_n:={s\in S: p(s)\le 2n\}$ , and

$R_n:={s\in S: p(s)\le 2n-1\}$ .

Parity Automata.