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:

    Two clergymen disputing whether ordination would be valid without the imposition of both hands, the more formal one said, “Do you think the Holy Dove could fly down with only one wing?”
    Horace Walpole (1717–1797)

    According to our social pyramid, all men who feel displaced racially, culturally, and/or because of economic hardships will turn on those whom they feel they can order and humiliate, usually women, children, and animals—just as they have been ordered and humiliated by those privileged few who are in power. However, this definition does not explain why there are privileged men who behave this way toward women.
    Ana Castillo (b. 1953)