Muller Automaton - Formal Definition

Formal Definition

Formally, a deterministic Muller-automaton is a tuple A = (Q,Σ,δ,q0,F) that consists of the following information:

  • Q is a finite set. The elements of Q are called the states of Q.
  • Σ 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.
  • F is a set of sets of states. Formally, FP(Q) where P(Q) is powerset of Q. F defines the acceptance condition. A accepts exactly those runs in which the set of infinitely often occurring states is an element of F

In a non-deterministic Muller automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states and initial state is q0 is replaced by a set of initial states Q0. Generally, Muller automaton refers to non-deterministic Muller automaton.

For more comprehensive formalism look at ω-automaton.

Read more about this topic:  Muller Automaton

Famous quotes containing the words formal and/or definition:

    This is no argument against teaching manners to the young. On the contrary, it is a fine old tradition that ought to be resurrected from its current mothballs and put to work...In fact, children are much more comfortable when they know the guide rules for handling the social amenities. It’s no more fun for a child to be introduced to a strange adult and have no idea what to say or do than it is for a grownup to go to a formal dinner and have no idea what fork to use.
    Leontine Young (20th century)

    Although there is no universal agreement as to a definition of life, its biological manifestations are generally considered to be organization, metabolism, growth, irritability, adaptation, and reproduction.
    The Columbia Encyclopedia, Fifth Edition, the first sentence of the article on “life” (based on wording in the First Edition, 1935)