Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automata that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states. ω-automata are useful for specifying behavior of systems that are not expected to terminate, such as hardware, operating systems and control systems. For such systems, one may want to specify a property such as "for every request, an acknowledge eventually follows", or its negation "there is a request that is not followed by an acknowledge". The former is a property of infinite words: one cannot say of a finite sequence that it satisfies this property. Classes of ω-automata include the Büchi automata, Rabin automata, Streett automata, parity automata and Muller automata, each deterministic or non-deterministic. These classes of ω-automata differ only in terms of acceptance condition. They all recognize precisely the regular ω-languages except for the deterministic Büchi automata, which is strictly weaker than all the others. Although all these types of automata recognize the same set of ω-languages, they nonetheless differ in succinctness of representation for a given ω-language. Formally, a deterministic ω-automaton is a tuple A = (Q,Σ,δ,Q0,Acc) that consists of the following components: Q is a finite set. The elements of Q are called the states of A. Σ is a finite set called the alphabet of A. δ: Q × Σ → Q is a function, called the transition function of A. Q0 is an element of Q, called the initial state. Acc is the acceptance condition, formally a subset of Qω. An input for A is an infinite string over the alphabet Σ, i.e. it is an infinite sequence α = (a1,a2,a3,...). The run of A on such an input is an infinite sequence ρ = (r0,r1,r2,...) of states, defined as follows: r0 = q0. r1 = δ(r0,a1). r2 = δ(r1,a2). rn = δ(rn-1,an). The main purpose of an ω-automaton is to define a subset of the set of all inputs: The set of accepted inputs.
Michael Christoph Gastpar, Sung Hoon Lim, Adriano Pastore, Chen Feng
Anton Schleiss, Javier García Hernández, Bettina Schaefli, Fränz Zeimetz, Guillaume Mathieu Artigue
Maryam Kamgarpour, John Lygeros, Tony Alan Wood