🧠 Introduction

🎯 What are ω-Automata?

ω-Automata are automata that process infinite words (ω-words) instead of finite strings. They're essential for model checking, program verification, and temporal logic. The key challenge: how do you define acceptance when the input never ends?

Key insight: For infinite words, acceptance is defined in terms of which states are visited infinitely often. Different acceptance conditions (Büchi, Rabin, Streett, parity) give different automata classes — but they all recognize the same class of languages (ω-regular languages).

Why ω-Automata Matter

Infinite behavior: Model non-terminating systems. Verification: Model checking. Temporal logic: LTL, CTL. Reactive systems: Operating systems, protocols. Games: Infinite games. Theory: ω-regular languages.

♾️ Infinite words🔄 Büchi⚖️ Parity🔍 Verification

# ω-Automata — the big picture
print("""
=== What are ω-Automata? ===

Classical automata:
  - Process finite words
  - Accept/reject at the end
  - Example: DFA, NFA

ω-Automata:
  - Process INFINITE words
  - Never "end"
  - Acceptance based on infinite behavior
  - Example: Büchi, Rabin, Streett, Parity

=== The Key Question ===

For finite words:
  Accept if the run ends in an accepting state.

For infinite words:
  There's no "end"!
  How do we define acceptance?

Answer:
  Look at which states are visited INFINITELY OFTEN.
  Different conditions = different automata.

=== The Main Types ===

1. BÜCHI AUTOMATA
   Accept if some accepting state is visited infinitely often.
   Condition: ∃ q ∈ F: q appears infinitely often.

2. RABIN AUTOMATA
   Accept if for some pair (E, F):
     All states in E are visited finitely often,
     and some state in F is visited infinitely often.

3. STREETT AUTOMATA
   Dual of Rabin.
   Accept if for all pairs (E, F):
     If some state in E is visited infinitely often,
     then some state in F is visited infinitely often.

4. PARITY AUTOMATA
   States have priorities (natural numbers).
   Accept if the minimum priority visited infinitely often
   is even.

5. MULLER AUTOMATA
   Accept if the set of states visited infinitely often
   is in a specified family F.

=== Why So Many Types? ===

All these types recognize the SAME class:
  ω-regular languages.

But they have different properties:
  - Determinism: some are determinizable, some not.
  - Complementation: some are easier to complement.
  - Expressiveness: all equivalent.
  - Succinctness: some are more concise.

=== Real-World Analogy ===

Think of a program that runs forever:

  while (true) {
    if (condition) {
      do_something();
    }
  }

Questions:
  - Does it ever do_something()?
  - Does it always eventually do_something()?
  - Does it do_something() infinitely often?

ω-Automata can answer these!
""")

# ANALOGY
print("=== Analogy: Traffic Light ===")
print("""
Imagine a traffic light that runs forever:
  Green → Yellow → Red → Green → Yellow → Red → ...

This is an infinite word:
  G Y R G Y R G Y R ...

Questions:
  1. Does the light ever turn green?
     Yes (infinitely often).
  
  2. Does the light always eventually turn red?
     Yes.
  
  3. Is there a state that's never visited?
     No (all states visited).

ω-Automata can express these properties:
  - Büchi: "Green infinitely often"
  - Rabin: "Green finitely often" or "Red infinitely often"
  - Parity: based on priority of states

=== Another Analogy: Operating System ===

An OS runs forever:
  - Processes start and terminate.
  - Resources are allocated and released.
  - Interrupts occur.

Properties:
  - "Every process eventually terminates"
  - "No process starves"
  - "The system never deadlocks"

These are ω-regular properties.
ω-Automata model them.

=== The Verification Pipeline ===

1. MODEL the system as an ω-automaton.
2. SPECIFY the property as an ω-automaton.
3. CHECK if model satisfies property.
4. This is MODEL CHECKING.

Used in:
  - Hardware verification
  - Protocol verification
  - Software verification
""")

# THE BIG PICTURE
print("""
=== The Big Picture ===

ω-Automata:

  ┌─────────────────────────────────────┐
  │ ω-Regular Languages                 │
  │  ┌───────────────────────────────┐  │
  │  │ Büchi                         │  │
  │  │  ┌─────────────────────────┐  │  │
  │  │  │ Rabin                   │  │  │
  │  │  │  ┌───────────────────┐  │  │  │
  │  │  │  │ Streett           │  │  │  │
  │  │  │  │  ┌─────────────┐  │  │  │  │
  │  │  │  │  │ Parity      │  │  │  │  │
  │  │  │  │  └─────────────┘  │  │  │  │
  │  │  │  └───────────────────┘  │  │  │
  │  │  └─────────────────────────┘  │  │
  │  └───────────────────────────────┘  │
  └─────────────────────────────────────┘

All equivalent in expressiveness:
  They recognize the same class (ω-regular).

But different in:
  - Determinizability
  - Complementation
  - Succinctness
  - Algorithms

=== Key Facts ===

1. ALL TYPES ARE EQUIVALENT
   Büchi ≡ Rabin ≡ Streett ≡ Parity ≡ Muller
   All recognize ω-regular languages.

2. NONDETERMINISTIC BÜCHI IS NOT DETERMINIZABLE
   Some Büchi automata can't be determinized.
   (Unlike finite-word NFA.)

3. PARITY IS DETERMINIZABLE
   Every parity automaton has an equivalent
   deterministic parity automaton.
   (With exponential blowup.)

4. APPLICATIONS
   - Model checking
   - Temporal logic
   - Verification
   - Synthesis
""")

# ω-AUTOMATA IN CODE
print("=== ω-Automata in Code ===")

class BuchiAutomaton:
    """A simple nondeterministic Büchi automaton."""
    def __init__(self, states, alphabet, transitions, initial, accept):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions  # (state, symbol) -> set of states
        self.q0 = initial
        self.F = accept  # accepting states
    
    def accepting_run(self, word, max_length=100):
        """Check if there's an accepting run (for finite prefix)."""
        # For demonstration, check finite prefix
        current = {self.q0}
        
        for symbol in word[:max_length]:
            next_states = set()
            for state in current:
                next_states |= self.delta.get((state, symbol), set())
            current = next_states
        
        # Check if any accepting state is reachable
        return bool(current & self.F)


# Example: Büchi automaton for "a infinitely often"
# States: q0 (initial), q1 (accepting)
# Transitions:
#   q0 --a--> q1
#   q0 --b--> q0
#   q1 --a--> q1
#   q1 --b--> q0
buchi = BuchiAutomaton(
    states={'q0', 'q1'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q1'},
        ('q0', 'b'): {'q0'},
        ('q1', 'a'): {'q1'},
        ('q1', 'b'): {'q0'},
    },
    initial='q0',
    accept={'q1'}
)

print("Büchi automaton for 'a infinitely often':")
print("  States: q0 (initial), q1 (accepting)")
print("  Transitions:")
print("    q0 --a--> q1")
print("    q0 --b--> q0")
print("    q1 --a--> q1")
print("    q1 --b--> q0")
print("  Accept: q1 visited infinitely often")

print("\nTesting finite prefixes:")
for w in ['a', 'ab', 'aba', 'abab', 'b', 'bb']:
    result = buchi.accepting_run(w)
    print(f"  '{w}' → {'✓ (accepting state reached)' if result else '✗'}")

print("""
=== Key Observations ===

1. INFINITE WORDS
   The automaton runs forever.
   Acceptance depends on infinite behavior.

2. BÜCHI CONDITION
   Accept if some accepting state
   is visited infinitely often.

3. EXAMPLE
   'a' infinitely often:
     - If 'a' appears infinitely often,
       q1 is visited infinitely often.
     - So the word is accepted.
   
   'b' infinitely often (no 'a'):
     - q1 is never visited.
     - So the word is rejected.

4. NONDETERMINISM
   Büchi automata are typically nondeterministic.
   (Deterministic Büchi is weaker.)

=== The Acceptance Condition ===

For an infinite word w = a₀a₁a₂...:

  Run: q₀ → q₁ → q₂ → ...
  
  Büchi acceptance:
    ∃ q ∈ F: q appears infinitely often in the run.
    
  Equivalently:
    inf(run) ∩ F ≠ ∅
    
  where inf(run) = set of states visited infinitely often.

This is the simplest acceptance condition.
""")

♾️ ω-Words & ω-Languages

🎯 Infinite Words

An ω-word is an infinite sequence of symbols. An ω-language is a set of ω-words. These are the inputs that ω-automata process.

ω-Word Basics

ω-word: Infinite sequence a₀a₁a₂... ω-language: Set of ω-words. Prefix: Finite initial segment. Infinitely often: Visited infinitely many times. Eventually: After some finite point. ω-regular: Recognized by ω-automata.

♾️ Infinite📝 ω-language🔤 Prefix🔄 Infinitely often

# ω-Words and ω-Languages
print("=" * 60)
print("ω-WORDS AND ω-LANGUAGES")
print("=" * 60)

print("""
=== Definition ===

An ω-WORD over alphabet Σ is an infinite sequence:
  w = a₀ a₁ a₂ a₃ ...

where each aᵢ ∈ Σ.

Examples:
  aaaa... = a^ω
  abababab... = (ab)^ω
  aabbcc... (not periodic)
  Any infinite sequence

An ω-LANGUAGE is a set of ω-words:
  L ⊆ Σ^ω

=== Notation ===

Σ^ω: set of all ω-words over Σ
Σ*: set of all finite words over Σ
Σ^+: set of all non-empty finite words

Operations:
  w ∈ Σ^ω: infinite word
  u ∈ Σ*: finite word
  u·w: concatenation of finite u and infinite w

=== Examples ===

1. L = { a^ω } = { aaaa... }
   Single word: all a's.

2. L = { w | w has infinitely many a's }
   All ω-words with infinitely many a's.

3. L = { w | w has finitely many a's }
   All ω-words with finitely many a's.

4. L = { (ab)^ω } = { ababab... }
   Periodic word.

5. L = { w | w has no b's after the first a }
   ω-words where all b's come before all a's.

=== Key Properties ===

1. INFINITELY OFTEN
   A symbol a appears infinitely often in w
   if for all n, there exists m > n with aₘ = a.
   
   Notation: ∃^ω n: aₙ = a

2. EVENTUALLY
   A property holds eventually if it holds
   for all sufficiently large n.
   
   Notation: ∀^ω n: P(aₙ)

3. INFINITELY OFTEN (Set Version)
   A set of states S is visited infinitely often
   if the run visits S infinitely many times.
   
   Notation: inf(run) = set of states visited ∞ often.

=== ω-Regular Languages ===

An ω-language is ω-REGULAR if it can be
recognized by a Büchi automaton
(equivalently, by any ω-automaton).

Examples:
  - { a^ω }
  - { w | w has infinitely many a's }
  - { (ab)^ω }
  - Finite unions/intersections of these

Non-examples:
  - { a^n b^ω | n ≥ 0 } (not ω-regular? Actually is)
  - Some more complex languages

=== The ω-Regular Expressions ===

ω-regular expressions extend regular expressions:

  E ::= ∅ | ε | a | E₁ + E₂ | E₁ · E₂ | E*
       | E^ω | E₁ · E₂^ω

Examples:
  (a + b)* · a^ω: words with infinitely many a's? No.
  Actually: (a+b)* · a^ω = words ending with a^ω
  = words with finitely many b's.

  (a+b)* · (a(a+b)*)^ω = words with infinitely many a's.

=== Connection to Finite Words ===

ω-languages are related to finite languages:

  For L ⊆ Σ*, define:
    L^ω = { w₀w₁w₂... | each wᵢ ∈ L, wᵢ ≠ ε }
    L^∞ = { w | w has infinitely many prefixes in L }
    lim(L) = { w | w has infinitely many prefixes in L }

Key theorem:
  L is ω-regular
  ⟺
  L = ∪ᵢ Lᵢ · Kᵢ^ω for some regular Lᵢ, Kᵢ
""")

# ω-REGULAR LANGUAGES
print("""
=== ω-Regular Languages ===

Definition:
  An ω-language is ω-regular if it's recognized
  by a Büchi automaton (or any ω-automaton).

Closure properties:
  ✓ Union
  ✓ Intersection
  ✓ Complement
  ✓ Concatenation with regular languages
  ✓ Kleene star (careful definition)

Characterization:
  L is ω-regular
  ⟺
  L = ∪ᵢ₌₁ⁿ Lᵢ · Kᵢ^ω
  where Lᵢ, Kᵢ are regular languages.

Examples:
  1. { a^ω } = ∅ · ∅^ω ∪ {ε} · {a}^ω
  2. { w | w has ∞ many a's }
     = (a+b)* · (a(a+b)*)^ω
  3. { w | w has finitely many a's }
     = (a+b)* · b^ω
  4. { (ab)^ω } = ∅ · {ab}^ω

=== The ω-Regular Expressions ===

Syntax:
  E ::= ∅ | ε | a | E₁ + E₂ | E₁ · E₂ | E*
       | E^ω

Semantics:
  L(∅) = ∅
  L(ε) = {ε}
  L(a) = {a}
  L(E₁ + E₂) = L(E₁) ∪ L(E₂)
  L(E₁ · E₂) = L(E₁) · L(E₂)
  L(E*) = (L(E))*
  L(E^ω) = { w₀w₁w₂... | each wᵢ ∈ L(E), wᵢ ≠ ε }

Theorem:
  L is ω-regular ⟺ L = L(E) for some ω-regular expression E.

This is the ω-version of Kleene's theorem.

=== Examples ===

1. "Infinitely many a's":
   (a+b)* · (a(a+b)*)^ω

2. "Finitely many a's":
   (a+b)* · b^ω

3. "Eventually always a":
   (a+b)* · a^ω

4. "Infinitely often a and infinitely often b":
   (a+b)* · (a(a+b)* · b(a+b)*)^ω
   (More complex)

5. "Every a is followed by b":
   (b + ab)^ω

=== Why ω-Regular Languages Matter ===

1. VERIFICATION
   System properties are ω-regular.

2. TEMPORAL LOGIC
   LTL formulas define ω-regular languages.

3. MODEL CHECKING
   Check if system ⊆ property.

4. SYNTHESIS
   Construct systems satisfying specifications.

5. GAMES
   Winning conditions are ω-regular.
""")

# ω-REGULAR IN CODE
print("=== ω-Regular Languages in Code ===")

class OmegaLanguage:
    """Simple representation of ω-regular languages."""
    def __init__(self, description):
        self.description = description
    
    def __repr__(self):
        return f"ω-Language: {self.description}"


# Examples
examples = [
    OmegaLanguage("{ a^ω } = { aaaa... }"),
    OmegaLanguage("{ w | w has infinitely many a's }"),
    OmegaLanguage("{ w | w has finitely many a's }"),
    OmegaLanguage("{ (ab)^ω } = { ababab... }"),
    OmegaLanguage("{ w | eventually always a }"),
]

print("Examples of ω-regular languages:")
for ex in examples:
    print(f"  {ex}")

print("""
=== Key Properties ===

1. INFINITELY OFTEN
   A symbol a appears infinitely often in w
   if for all n, there exists m > n with aₘ = a.
   
   ω-regular expression: (a+b)* · (a(a+b)*)^ω

2. EVENTUALLY
   A property holds eventually if it holds
   for all sufficiently large n.
   
   ω-regular expression: (a+b)* · a^ω

3. BOTH INFINITELY OFTEN
   Infinitely many a's AND infinitely many b's.
   
   ω-regular expression:
   (a+b)* · (a(a+b)* · b(a+b)*)^ω
   (Not exactly right, but similar)

4. NEITHER INFINITELY OFTEN
   Finitely many a's AND finitely many b's.
   = Eventually no a's and no b's.
   = Eventually constant.
   
   ω-regular expression:
   (a+b)* · c^ω for some c ∈ {a, b}
   (Actually, eventually constant means
    eventually all same symbol.)

=== Why Infinite Words are Different ===

1. NO END
   Can't just check the last state.

2. INFINITELY OFTEN
   Acceptance depends on infinite behavior.

3. NON-DETERMINIZABILITY
   Nondeterministic Büchi ≠ Deterministic Büchi.

4. COMPLEMENTATION
   Complementing Büchi is hard.
   (Rabin/parity are easier.)

5. DECIDABILITY
   Emptiness is decidable.
   Universality is decidable.
   Equivalence is decidable.
   (For ω-regular languages.)
""")

# SUMMARY
print("""
=== Summary ===

ω-Word:
  - Infinite sequence a₀a₁a₂...
  - No end
  - Acceptance based on infinite behavior

ω-Language:
  - Set of ω-words
  - L ⊆ Σ^ω

ω-Regular Language:
  - Recognized by ω-automata
  - Defined by ω-regular expressions
  - L = ∪ᵢ Lᵢ · Kᵢ^ω

Key operations:
  - Infinitely often (∃^ω)
  - Eventually (∀^ω)
  - Infinitely often (set version: inf(run))

ω-Regular Expressions:
  - Extend regular expressions with ^ω
  - Kleene's theorem for ω-words

Key insight:
  ω-languages model infinite behavior.
  They're essential for verification.
  ω-regular languages are the "regular"
  languages of infinite words.
""")

🔄 Büchi Automata

🎯 The Simplest ω-Automata

Büchi automata are the simplest type of ω-automata. They have a set of accepting states, and accept an infinite word if some accepting state is visited infinitely often.

Büchi Automata Facts

Acceptance: ∃ accepting state visited ∞ often. Nondeterministic: Typically NFA-like. Not determinizable: Nondeterministic Büchi ⊋ Deterministic Büchi. Closure: Union, intersection (not complement). Applications: LTL, model checking. History: Büchi (1960).

🔄 Büchi♾️ Infinitely often❌ Not determinizable📝 LTL

# Büchi Automata
print("=" * 60)
print("BÜCHI AUTOMATA")
print("=" * 60)

print("""
=== Definition ===

A BÜCHI AUTOMATON is a 5-tuple:
  A = (Q, Σ, δ, q₀, F)

where:
  Q: finite set of states
  Σ: finite alphabet
  δ: Q × Σ → P(Q) (nondeterministic)
  q₀: initial state
  F: set of accepting states (F ⊆ Q)

=== Acceptance ===

For an infinite word w = a₀a₁a₂...:

  A run is an infinite sequence of states:
    r = q₀ q₁ q₂ ...
  
  where qᵢ₊₁ ∈ δ(qᵢ, aᵢ).

  The run is ACCEPTING if:
    inf(r) ∩ F ≠ ∅
  
  where inf(r) = set of states appearing
  infinitely often in r.

  A accepts w if there EXISTS an accepting run.

=== The Acceptance Condition ===

  "Some accepting state is visited infinitely often."

Formally:
  ∃ q ∈ F: q appears infinitely often in the run.

Equivalently:
  inf(run) ∩ F ≠ ∅

=== Examples ===

1. "Infinitely many a's":
   Q = {q0, q1}
   Σ = {a, b}
   q0 = q0
   F = {q1}
   
   δ(q0, a) = {q1}
   δ(q0, b) = {q0}
   δ(q1, a) = {q1}
   δ(q1, b) = {q0}
   
   The automaton visits q1 whenever it sees 'a'.
   If 'a' appears infinitely often,
   q1 is visited infinitely often.
   So it accepts words with ∞ many a's.

2. "Finitely many a's":
   Q = {q0, q1}
   Σ = {a, b}
   q0 = q0
   F = {q0}
   
   δ(q0, a) = {q0}
   δ(q0, b) = {q0, q1}
   δ(q1, b) = {q1}
   δ(q1, a) = ∅ (or back to q0)
   
   Intuition: after the last 'a',
   stay in q1 (accepting).
   Since q1 is accepting and visited infinitely often
   (after the last 'a'), the word is accepted.
   
   Wait, this isn't quite right.
   Let me reconsider.
   
   Better: "Finitely many a's":
   Q = {q0, q1}
   F = {q1}
   δ(q0, a) = {q0}
   δ(q0, b) = {q0, q1}
   δ(q1, b) = {q1}
   δ(q1, a) = {q0}
   
   Hmm, still not right.
   
   Actually, the standard construction:
   "Finitely many a's" = (a+b)* · b^ω
   
   This is recognized by:
   Q = {q0, q1}
   F = {q1}
   δ(q0, a) = {q0}
   δ(q0, b) = {q0, q1}
   δ(q1, b) = {q1}
   δ(q1, a) = ∅
   
   If the word has infinitely many a's,
   then q1 can't be visited infinitely often
   (because 'a' sends us to ∅ or q0).
   
   If the word has finitely many a's,
   then after the last 'a',
   all symbols are 'b', and we can stay in q1.
   So q1 is visited infinitely often.
   
   So the automaton accepts exactly
   words with finitely many a's.

=== Nondeterminism ===

Büchi automata are NONDETERMINISTIC:
  δ(q, a) can have multiple states.

Why nondeterminism?
  - It's more powerful.
  - Deterministic Büchi is weaker.
  - Some ω-regular languages can't be
    recognized by deterministic Büchi.

=== Determinizability ===

Nondeterministic Büchi ⊋ Deterministic Büchi.

There are ω-regular languages that
require nondeterminism for Büchi.

Example: "Infinitely many a's AND finitely many b's"
  This is ω-regular but not deterministic Büchi.

However, every Büchi automaton can be
converted to a deterministic Rabin/parity
automaton (with exponential blowup).

=== Closure Properties ===

Büchi automata are CLOSED under:
  ✓ Union
  ✓ Intersection
  ✗ Complement (hard!)
  ✓ Concatenation with regular
  ✓ Kleene star (careful)

Complementing a Büchi automaton:
  - Direct complementation is hard.
  - Convert to Rabin/parity, complement there.
  - Convert back to Büchi.
  - Exponential blowup.

=== Applications ===

1. LTL MODEL CHECKING
   LTL formula → Büchi automaton.
   System → Büchi automaton.
   Check if system ∩ ¬property = ∅.

2. TEMPORAL LOGIC
   LTL, CTL* → Büchi automata.

3. VERIFICATION
   Protocol verification.
   Hardware verification.

4. SYNTHESIS
   Reactive synthesis.

5. GAMES
   Winning conditions.
""")

# BÜCHI IN CODE
print("=== Büchi Automata in Code ===")

class BuchiAutomaton:
    """A nondeterministic Büchi automaton."""
    def __init__(self, states, alphabet, transitions, initial, accept):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions  # (state, symbol) -> set of states
        self.q0 = initial
        self.F = accept
    
    def run(self, word, max_steps=1000):
        """Simulate a run (BFS)."""
        from collections import deque
        
        # Start configurations
        queue = deque([(self.q0, 0)])
        visited = set()
        
        # Track states visited infinitely often
        # (For finite simulation, just track reachability)
        
        runs = []
        while queue:
            state, idx = queue.popleft()
            
            if idx >= len(word) or idx >= max_steps:
                # End of finite prefix
                continue
            
            symbol = word[idx]
            for next_state in self.delta.get((state, symbol), set()):
                queue.append((next_state, idx + 1))
        
        return False  # Simplified
    
    def accepts_infinite(self, word, max_length=100):
        """
        Check if there's an accepting run
        (for a finite prefix).
        """
        # BFS to find reachable accepting states
        current = {self.q0}
        
        for i in range(min(len(word), max_length)):
            symbol = word[i]
            next_states = set()
            for state in current:
                next_states |= self.delta.get((state, symbol), set())
            current = next_states
            
            if not current:
                return False
        
        return bool(current & self.F)


# Example: "Infinitely many a's"
buchi_inf_a = BuchiAutomaton(
    states={'q0', 'q1'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q1'},
        ('q0', 'b'): {'q0'},
        ('q1', 'a'): {'q1'},
        ('q1', 'b'): {'q0'},
    },
    initial='q0',
    accept={'q1'}
)

print("Büchi automaton for 'infinitely many a's':")
print("  Q = {q0, q1}")
print("  F = {q1}")
print("  δ(q0, a) = {q1}")
print("  δ(q0, b) = {q0}")
print("  δ(q1, a) = {q1}")
print("  δ(q1, b) = {q0}")

print("\nTesting finite prefixes:")
for w in ['a', 'ab', 'aba', 'abab', 'b', 'bb']:
    result = buchi_inf_a.accepts_infinite(w)
    print(f"  '{w}' → {'✓ (accepting state reachable)' if result else '✗'}")

# Example: "Finitely many a's"
buchi_fin_a = BuchiAutomaton(
    states={'q0', 'q1'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q0'},
        ('q0', 'b'): {'q0', 'q1'},
        ('q1', 'b'): {'q1'},
        # q1 on 'a' -> no transition (dead)
    },
    initial='q0',
    accept={'q1'}
)

print("\nBüchi automaton for 'finitely many a's':")
print("  Q = {q0, q1}")
print("  F = {q1}")
print("  δ(q0, a) = {q0}")
print("  δ(q0, b) = {q0, q1}")
print("  δ(q1, b) = {q1}")
print("  δ(q1, a) = ∅")

print("\nTesting finite prefixes:")
for w in ['a', 'ab', 'aba', 'abab', 'b', 'bb']:
    result = buchi_fin_a.accepts_infinite(w)
    print(f"  '{w}' → {'✓' if result else '✗'}")

print("""
=== Key Observations ===

1. NONDETERMINISM
   Büchi automata can have multiple transitions.
   This is essential for full power.

2. INFINITELY OFTEN
   Acceptance depends on which states
   are visited infinitely often.

3. TWO EXAMPLES
   - "Infinitely many a's": q1 on 'a'
   - "Finitely many a's": q1 on 'b' after last 'a'

4. DETERMINIZABILITY
   Nondeterministic Büchi is more powerful
   than deterministic Büchi.
   
   Some ω-regular languages can't be
   recognized by deterministic Büchi.

5. COMPLEMENTATION
   Complementing Büchi is hard.
   Use Rabin/parity for complementation.
""")

# SUMMARY
print("""
=== Summary ===

Büchi Automaton:
  - 5-tuple: (Q, Σ, δ, q₀, F)
  - Nondeterministic
  - Accept if some state in F is visited ∞ often

Acceptance:
  ∃ accepting run with inf(run) ∩ F ≠ ∅

Examples:
  - "Infinitely many a's"
  - "Finitely many a's"

Properties:
  - Not determinizable (nondet > det)
  - Closed under union, intersection
  - NOT closed under complement (directly)
  - Exponential complementation

Applications:
  - LTL model checking
  - Temporal logic
  - Verification
  - Synthesis

Key insight:
  Büchi is the simplest ω-automaton.
  Simple acceptance condition.
  But powerful enough for many applications.
  Used in model checking and verification.
""")

🏆 Rabin Automata

🎯 Pairs of State Sets

Rabin automata use a set of pairs (E_i, F_i) of state sets. Acceptance requires that for some pair, all states in E_i are visited finitely often and some state in F_i is visited infinitely often.

Rabin Automata Facts

Acceptance: ∃ pair (E,F): E finitely often, F infinitely often. Determinizable: Yes, every Rabin can be determinized. Complement: Easy (swap pairs). Applications: Verification, synthesis. History: Rabin (1969). Power: Equivalent to Büchi.

🏆 Rabin pairs✅ Determinizable🔒 Closed under complement📝 Verification

# Rabin Automata
print("=" * 60)
print("RABIN AUTOMATA")
print("=" * 60)

print("""
=== Definition ===

A RABIN AUTOMATON is a 5-tuple:
  A = (Q, Σ, δ, q₀, Ω)

where:
  Q: finite set of states
  Σ: finite alphabet
  δ: Q × Σ → P(Q) (nondeterministic)
  q₀: initial state
  Ω: acceptance condition
  
  Ω = {(E₁, F₁), ..., (Eₖ, Fₖ)}
  
  where Eᵢ, Fᵢ ⊆ Q.

=== Acceptance ===

For an infinite word w:

  A run is an infinite sequence of states.
  
  The run is ACCEPTING if:
    ∃ i: inf(run) ∩ Eᵢ = ∅ AND inf(run) ∩ Fᵢ ≠ ∅
  
  where inf(run) = set of states visited ∞ often.

In words:
  "There exists a pair (E, F) such that:
   - All states in E are visited finitely often.
   - Some state in F is visited infinitely often."

=== Intuition ===

Think of each pair as a "goal":
  - E: states we want to avoid infinitely often.
  - F: states we want to visit infinitely often.
  
Accept if SOME goal is achieved.

=== Examples ===

1. "Infinitely many a's":
   Q = {q0, q1}
   Ω = {(∅, {q1})}
   
   Accept if q1 is visited ∞ often.
   
   This is equivalent to a Büchi automaton
   with F = {q1}.

2. "Finitely many a's":
   Q = {q0, q1}
   Ω = {({q0}, {q1})}
   
   Accept if q0 is visited finitely often
   AND q1 is visited infinitely often.
   
   Hmm, this doesn't quite work.
   
   Actually: "Finitely many a's" = "Eventually always b"
   
   Q = {q0, q1}
   Ω = {({q0}, {q1})}
   
   Wait, let me think.
   
   We want: finitely many a's.
   Equivalently: eventually no a's.
   Equivalently: eventually always b.
   
   States:
     q0: seen a recently
     q1: no a for a while
   
   Ω = {({q0}, {q1})}
   
   Accept if q0 is visited finitely often
   (no more a's) and q1 is visited infinitely often
   (always b eventually).
   
   This works!

3. "Infinitely many a's and finitely many b's":
   Q = {q0, q1, q2}
   Ω = {({q2}, {q1})}
   
   q1: visited when 'a' is seen.
   q2: visited when 'b' is seen.
   
   Accept if q2 is visited finitely often
   (finitely many b's) and q1 is visited
   infinitely often (infinitely many a's).
   
   This works!

=== Determinizability ===

THEOREM (Rabin, 1969):
  Every Rabin automaton can be converted to
  an equivalent DETERMINISTIC Rabin automaton.
  
  (With exponential blowup.)

This is a key advantage over Büchi:
  - Büchi: not determinizable.
  - Rabin: determinizable.

Why does this matter?
  - Deterministic automata are easier to work with.
  - Complementation is easier.
  - Model checking is easier.

=== Complementation ===

Rabin automata are easy to complement:
  - Swap accepting and non-accepting.
  - Use the dual condition (Streett).
  - Convert back to Rabin.
  
  Or: use the determinization.
  - Determinize.
  - Complement the deterministic automaton.
  - Convert back to Rabin.

=== Closure Properties ===

Rabin automata are CLOSED under:
  ✓ Union
  ✓ Intersection
  ✓ Complement
  ✓ Concatenation
  ✓ Kleene star

All standard operations!

This makes Rabin automata very convenient.

=== Applications ===

1. MODEL CHECKING
   System → Rabin automaton.
   Property → Rabin automaton.
   Check if system ⊆ property.

2. SYNTHESIS
   Reactive synthesis.
   Construct system from specification.

3. VERIFICATION
   Hardware verification.
   Protocol verification.

4. GAMES
   Winning conditions.
   Parity games are a special case.

5. DECISION PROCEDURES
   S1S (monadic second-order logic).
   Decidable via Rabin automata.
""")

# RABIN IN CODE
print("=== Rabin Automata in Code ===")

class RabinAutomaton:
    """A nondeterministic Rabin automaton."""
    def __init__(self, states, alphabet, transitions, initial, pairs):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions
        self.q0 = initial
        self.pairs = pairs  # list of (E, F) pairs
    
    def accepting(self, inf_states):
        """
        Check if the set of infinitely often visited states
        satisfies the Rabin condition.
        """
        for (E, F) in self.pairs:
            if not (inf_states & E) and (inf_states & F):
                return True
        return False


# Example: "Finitely many a's"
rabin_fin_a = RabinAutomaton(
    states={'q0', 'q1'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q0'},
        ('q0', 'b'): {'q0', 'q1'},
        ('q1', 'b'): {'q1'},
    },
    initial='q0',
    pairs=[({'q0'}, {'q1'})]
)

print("Rabin automaton for 'finitely many a's':")
print("  Q = {q0, q1}")
print("  Ω = {({q0}, {q1})}")
print("  δ(q0, a) = {q0}")
print("  δ(q0, b) = {q0, q1}")
print("  δ(q1, b) = {q1}")

print("\nAcceptance condition:")
print("  Accept if q0 is visited finitely often")
print("  AND q1 is visited infinitely often.")

print("""
=== Key Observations ===

1. PAIRS OF SETS
   Each pair (E, F) specifies:
     - E: states to avoid infinitely often.
     - F: states to visit infinitely often.

2. ACCEPTANCE
   Accept if SOME pair is satisfied.

3. COMPLEMENT
   Swap the condition:
     Accept if ALL pairs are NOT satisfied.
   This gives a Streett condition.
   Then convert back to Rabin.

4. DETERMINIZABILITY
   Every Rabin automaton is determinizable.
   (Rabin's theorem, 1969.)
   With exponential blowup.

5. APPLICATIONS
   Rabin automata are used in:
   - Model checking
   - Synthesis
   - Verification
   - Logic (S1S)

=== Comparison with Büchi ===

Büchi:
  - Simpler acceptance (just F).
  - Not determinizable.
  - Complement is hard.

Rabin:
  - More complex acceptance (pairs).
  - Determinizable.
  - Complement is easy.

Both recognize the same class:
  ω-regular languages.

=== Why Rabin is Important ===

1. DETERMINIZABILITY
   Enables deterministic model checking.

2. COMPLEMENTATION
   Easy to complement.
   Used in verification.

3. LOGIC
   S1S decidability uses Rabin automata.

4. SYNTHESIS
   Reactive synthesis uses Rabin/parity.

5. GAMES
   Parity games are Rabin games.
""")

# SUMMARY
print("""
=== Summary ===

Rabin Automaton:
  - 5-tuple: (Q, Σ, δ, q₀, Ω)
  - Ω = {(E₁, F₁), ..., (Eₖ, Fₖ)}
  - Accept if ∃ i: Eᵢ finitely often, Fᵢ infinitely often

Acceptance:
  ∃ pair (E, F): inf(run) ∩ E = ∅ and inf(run) ∩ F ≠ ∅

Properties:
  - Determinizable (Rabin's theorem)
  - Closed under complement
  - Closed under union, intersection
  - Equivalent to Büchi

Applications:
  - Model checking
  - Synthesis
  - Verification
  - S1S decidability
  - Games

Key insight:
  Rabin automata are more complex than Büchi
  but have better properties (determinizability,
  complementation).
  They're used in verification and synthesis.
""")

📊 Streett Automata

🎯 The Dual of Rabin

Streett automata are the dual of Rabin automata. They use pairs (E_i, F_i) but with the opposite acceptance condition: for all pairs, if some state in E_i is visited infinitely often, then some state in F_i must also be visited infinitely often.

Streett Automata Facts

Acceptance: ∀ pairs: E ∞ often ⟹ F ∞ often. Dual: Of Rabin. Complement: Rabin. Applications: Fairness conditions. History: Streett (1982). Power: Equivalent to Rabin.

📊 Streett pairs⚖️ Dual of Rabin🤝 Fairness📝 Verification

# Streett Automata
print("=" * 60)
print("STREETT AUTOMATA")
print("=" * 60)

print("""
=== Definition ===

A STREETT AUTOMATON is a 5-tuple:
  A = (Q, Σ, δ, q₀, Ω)

where:
  Q: finite set of states
  Σ: finite alphabet
  δ: Q × Σ → P(Q)
  q₀: initial state
  Ω: Streett condition
  
  Ω = {(E₁, F₁), ..., (Eₖ, Fₖ)}
  
  where Eᵢ, Fᵢ ⊆ Q.

=== Acceptance ===

For an infinite word w:

  A run is ACCEPTING if:
    ∀ i: (inf(run) ∩ Eᵢ ≠ ∅) ⟹ (inf(run) ∩ Fᵢ ≠ ∅)

In words:
  "For all pairs (E, F):
   If some state in E is visited infinitely often,
   then some state in F is visited infinitely often."

=== Intuition ===

Think of each pair as a "fairness condition":
  - E: states that trigger a requirement.
  - F: states that satisfy the requirement.
  
Accept if ALL requirements are satisfied.

=== Examples ===

1. "If a occurs infinitely often, 
    then b occurs infinitely often":
   
   Ω = {({q_a}, {q_b})}
   
   where q_a is visited when 'a' is seen,
   and q_b is visited when 'b' is seen.
   
   Accept if: a ∞ often ⟹ b ∞ often.

2. "If request occurs, response eventually occurs":
   
   Ω = {({q_req}, {q_res})}
   
   Accept if: request ∞ often ⟹ response ∞ often.
   
   This is a FAIRNESS condition!

3. "No starvation":
   
   For each process i:
     Ωᵢ = ({q_wait_i}, {q_critical_i})
   
   Accept if: waiting ∞ often ⟹ critical ∞ often.
   
   This ensures no process starves.

=== The Dual Relationship ===

Rabin:
  ∃ i: (Eᵢ finitely often) AND (Fᵢ infinitely often)
  = ∃ i: (inf ∩ Eᵢ = ∅) AND (inf ∩ Fᵢ ≠ ∅)

Streett:
  ∀ i: (Eᵢ infinitely often) ⟹ (Fᵢ infinitely often)
  = ∀ i: (inf ∩ Eᵢ ≠ ∅) ⟹ (inf ∩ Fᵢ ≠ ∅)
  = ∀ i: (inf ∩ Eᵢ = ∅) OR (inf ∩ Fᵢ ≠ ∅)

Duality:
  Streett is the negation of Rabin with swapped pairs.

  ¬Rabin(Ω) = Streett(dual(Ω))

This duality is useful:
  - Complement Rabin → Streett
  - Complement Streett → Rabin

=== Applications ===

1. FAIRNESS
   Streett conditions naturally express fairness:
     "If a process is enabled infinitely often,
      it eventually runs."
   
   This is a Streett condition.

2. VERIFICATION
   Fairness assumptions in model checking.

3. SYNTHESIS
   Reactive synthesis with fairness.

4. GAMES
   Streett games (dual of Rabin games).

5. LOGIC
   Some logics use Streett conditions.

=== Determinizability ===

Streett automata are also determinizable:
  - Convert to Rabin (dual).
  - Determinize the Rabin.
  - Convert back to Streett.

Or directly determinize.

=== Closure Properties ===

Streett automata are CLOSED under:
  ✓ Union
  ✓ Intersection
  ✓ Complement
  ✓ Concatenation
  ✓ Kleene star

Same as Rabin (they're dual).

=== Comparison Table ===

Aspect          Rabin          Streett
──────────────────────────────────────────
Condition       ∃ pairs        ∀ pairs
Type            Existential    Universal
Complement      Streett        Rabin
Fairness        Less natural   More natural
Applications    Verification   Fairness
""")

# STREETT IN CODE
print("=== Streett Automata in Code ===")

class StreettAutomaton:
    """A nondeterministic Streett automaton."""
    def __init__(self, states, alphabet, transitions, initial, pairs):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions
        self.q0 = initial
        self.pairs = pairs  # list of (E, F) pairs
    
    def accepting(self, inf_states):
        """
        Check if the set of infinitely often visited states
        satisfies the Streett condition.
        """
        for (E, F) in self.pairs:
            if (inf_states & E) and not (inf_states & F):
                return False
        return True


# Example: "If a ∞ often, then b ∞ often"
streett_fairness = StreettAutomaton(
    states={'q_a', 'q_b', 'q_other'},
    alphabet={'a', 'b', 'c'},
    transitions={
        ('q_a', 'a'): {'q_a'},
        ('q_a', 'b'): {'q_b'},
        ('q_a', 'c'): {'q_other'},
        ('q_b', 'b'): {'q_b'},
        ('q_b', 'a'): {'q_a'},
        ('q_b', 'c'): {'q_other'},
        ('q_other', 'a'): {'q_a'},
        ('q_other', 'b'): {'q_b'},
        ('q_other', 'c'): {'q_other'},
    },
    initial='q_other',
    pairs=[({'q_a'}, {'q_b'})]
)

print("Streett automaton for fairness:")
print("  'If a occurs infinitely often,")
print("   then b occurs infinitely often.'")
print("  Ω = {({q_a}, {q_b})}")

print("\nAcceptance condition:")
print("  Accept if q_a ∞ often ⟹ q_b ∞ often.")

print("""
=== Key Observations ===

1. FAIRNESS CONDITIONS
   Streett conditions naturally express fairness:
     "If enabled ∞ often, then executed ∞ often."

2. DUALITY
   Rabin and Streett are duals.
   Complement of one is the other.

3. APPLICATIONS
   - Fairness in verification
   - No starvation
   - Reactive synthesis

4. DETERMINIZABILITY
   Streett automata are determinizable
   (via Rabin duality).

5. LOGIC
   Some logics use Streett conditions.

=== Why Streett Matters ===

1. FAIRNESS
   Streett is the natural language for fairness.

2. VERIFICATION
   Fairness assumptions are common in verification.

3. SYNTHESIS
   Fairness is important in synthesis.

4. DUALITY
   Understanding Rabin/Streett duality
   is important for theory.

5. GAMES
   Streett games are important in game theory.
""")

# SUMMARY
print("""
=== Summary ===

Streett Automaton:
  - 5-tuple: (Q, Σ, δ, q₀, Ω)
  - Ω = {(E₁, F₁), ..., (Eₖ, Fₖ)}
  - Accept if ∀ i: Eᵢ ∞ often ⟹ Fᵢ ∞ often

Acceptance:
  ∀ pairs (E, F): inf(run) ∩ E ≠ ∅ ⟹ inf(run) ∩ F ≠ ∅

Properties:
  - Dual of Rabin
  - Determinizable
  - Closed under complement
  - Equivalent to Büchi/Rabin

Applications:
  - Fairness conditions
  - Verification
  - Synthesis
  - Games

Key insight:
  Streett is the dual of Rabin.
  It's natural for fairness conditions.
  Understanding duality is important.
  Rabin and Streett are complementary views.
""")

⚖️ Parity Automata

🎯 Priorities and Parity

Parity automata assign a priority (natural number) to each state. Acceptance depends on the minimum priority visited infinitely often: the word is accepted if that minimum is even.

Parity Automata Facts

Acceptance: Min priority ∞ often is even. Determinizable: Yes, with exponential blowup. Complement: Easy (add 1 to priorities). Games: Parity games. Applications: Model checking, synthesis. History: Emerson-Jutla (1991).

⚖️ Priorities📊 Min even✅ Determinizable🎮 Games

# Parity Automata
print("=" * 60)
print("PARITY AUTOMATA")
print("=" * 60)

print("""
=== Definition ===

A PARITY AUTOMATON is a 5-tuple:
  A = (Q, Σ, δ, q₀, p)

where:
  Q: finite set of states
  Σ: finite alphabet
  δ: Q × Σ → P(Q)
  q₀: initial state
  p: Q → ℕ (priority function)

=== Acceptance ===

For an infinite word w:

  A run is an infinite sequence of states.
  
  Let inf(run) = set of states visited infinitely often.
  
  The run is ACCEPTING if:
    min{ p(q) | q ∈ inf(run) } is EVEN.

In words:
  "The minimum priority visited infinitely often
   is even."

=== Intuition ===

Priorities are like levels in a game:
  - Even priorities: good for the player.
  - Odd priorities: bad for the player.
  
Accept if the "best" priority that appears
infinitely often is even.

=== Examples ===

1. "Infinitely many a's":
   Q = {q0, q1}
   p(q0) = 1 (odd)
   p(q1) = 2 (even)
   
   Run: q0 when 'b', q1 when 'a'.
   
   If a ∞ often: q1 ∞ often, min priority = 2 (even). Accept.
   If a finitely often: q1 finitely often, min = 1 (odd). Reject.
   
   This is equivalent to a Büchi automaton.

2. "Finitely many a's":
   Q = {q0, q1}
   p(q0) = 2 (even)
   p(q1) = 1 (odd)
   
   If a finitely often: q0 ∞ often, min = 2 (even). Accept.
   If a ∞ often: q1 ∞ often, min = 1 (odd). Reject.
   
   This works!

3. "If a ∞ often, then b ∞ often":
   Q = {q_a, q_b, q_other}
   p(q_a) = 1 (odd)
   p(q_b) = 2 (even)
   p(q_other) = 0 (even)
   
   If both a and b ∞ often: min = 0 (even). Accept.
   If a ∞ often but b finitely often:
     q_a ∞ often, q_b finitely often.
     min priority = 1 (odd). Reject.
   If a finitely often: min = 0 (even). Accept.
   
   This captures fairness!

=== Properties ===

1. DETERMINIZABILITY
   Every parity automaton can be converted to
   an equivalent DETERMINISTIC parity automaton.
   
   (With exponential blowup.)
   
   This is a key property.

2. COMPLEMENTATION
   Easy: add 1 to all priorities.
   
   min even → min odd (after adding 1).
   So complement = increment priorities.

3. EQUIVALENCE
   Parity ≡ Rabin ≡ Streett ≡ Büchi.
   All recognize ω-regular languages.

4. SUCCINCTNESS
   Parity is often more succinct than Rabin.

=== Parity Games ===

Parity games are a special case:
  - Two players: Even and Odd.
  - States owned by Even or Odd.
  - Even wins if min priority ∞ often is even.
  - Odd wins otherwise.

Solving parity games:
  - Determine the winner.
  - Construct winning strategies.

Complexity:
  - In NP ∩ co-NP.
  - In UP ∩ co-UP.
  - In QP (quasi-polynomial, Calude et al. 2017).
  - In P? (Open problem!)

Parity games are important in:
  - Model checking
  - Synthesis
  - Verification
  - Logic

=== Applications ===

1. MODEL CHECKING
   μ-calculus model checking.
   Reduce to parity games.

2. SYNTHESIS
   Reactive synthesis.
   Reduce to parity games.

3. VERIFICATION
   System verification.
   Reduce to parity games.

4. LOGIC
   Modal μ-calculus.
   Decidable via parity games.

5. GAMES
   Parity games themselves.
""")

# PARITY IN CODE
print("=== Parity Automata in Code ===")

class ParityAutomaton:
    """A nondeterministic parity automaton."""
    def __init__(self, states, alphabet, transitions, initial, priorities):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions
        self.q0 = initial
        self.p = priorities  # dict: state -> priority
    
    def accepting(self, inf_states):
        """
        Check if the set of infinitely often visited states
        satisfies the parity condition.
        """
        if not inf_states:
            return False
        min_priority = min(self.p[q] for q in inf_states)
        return min_priority % 2 == 0


# Example: "Infinitely many a's"
parity_inf_a = ParityAutomaton(
    states={'q0', 'q1'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q1'},
        ('q0', 'b'): {'q0'},
        ('q1', 'a'): {'q1'},
        ('q1', 'b'): {'q0'},
    },
    initial='q0',
    priorities={'q0': 1, 'q1': 2}
)

print("Parity automaton for 'infinitely many a's':")
print("  Q = {q0, q1}")
print("  p(q0) = 1 (odd)")
print("  p(q1) = 2 (even)")

print("\nAcceptance condition:")
print("  Accept if min priority ∞ often is even.")
print("  q1 ∞ often → min = 2 (even) → accept.")
print("  q1 finitely often → min = 1 (odd) → reject.")

print("\nTest sets of infinitely often states:")
test_sets = [
    {'q0'},
    {'q1'},
    {'q0', 'q1'},
]

for s in test_sets:
    result = parity_inf_a.accepting(s)
    print(f"  inf = {s} → {'✓' if result else '✗'}")

print("""
=== Key Observations ===

1. PRIORITIES
   Each state has a priority (natural number).

2. MINIMUM PRIORITY
   The minimum priority visited infinitely often
   determines acceptance.

3. EVEN = ACCEPT
   If the minimum is even, accept.
   If odd, reject.

4. COMPLEMENT
   Add 1 to all priorities.
   Even becomes odd, odd becomes even.
   So complement is easy.

5. DETERMINIZABILITY
   Every parity automaton is determinizable.
   (Emerson-Jutla, 1991.)
   With exponential blowup.

=== Why Parity is Important ===

1. ELEGANT
   Simple acceptance condition.

2. DETERMINIZABLE
   Enables deterministic algorithms.

3. COMPLEMENTABLE
   Easy to complement.

4. GAMES
   Parity games are fundamental.

5. MODEL CHECKING
   μ-calculus uses parity games.

6. SYNTHESIS
   Reactive synthesis uses parity games.

7. COMPLEXITY
   Parity games: in QP, open if in P.

=== Parity vs Other Automata ===

Büchi:
  - Simple: just F.
  - Not determinizable.
  - Complement: hard.

Rabin:
  - Pairs (E, F).
  - Determinizable.
  - Complement: Streett.

Streett:
  - Dual of Rabin.
  - Determinizable.
  - Complement: Rabin.

Parity:
  - Priorities.
  - Determinizable.
  - Complement: increment priorities.
  - Most elegant.

Muller:
  - Family of sets.
  - Most general.
  - Determinizable.

All equivalent in power.
Parity is often the most convenient.
""")

# SUMMARY
print("""
=== Summary ===

Parity Automaton:
  - 5-tuple: (Q, Σ, δ, q₀, p)
  - p: Q → ℕ (priority function)
  - Accept if min priority ∞ often is even

Acceptance:
  min{ p(q) | q ∈ inf(run) } is even

Properties:
  - Determinizable (Emerson-Jutla)
  - Easy complementation (add 1 to priorities)
  - Equivalent to Büchi/Rabin/Streett/Muller
  - Often more succinct

Applications:
  - Model checking (μ-calculus)
  - Synthesis
  - Verification
  - Parity games

Key insight:
  Parity automata are the most elegant
  ω-automata.
  Simple acceptance condition.
  Determinizable.
  Easy complementation.
  Used in model checking and synthesis.
""")

🔀 Muller Automata

🎯 Families of State Sets

Muller automata are the most general type of ω-automata. They specify a family F of sets of states, and accept if the set of states visited infinitely often is in F.

Muller Automata Facts

Acceptance: inf(run) ∈ F. General: Most general acceptance. Subsumes: Büchi, Rabin, Streett, Parity. Determinizable: Yes. Applications: Theory. History: Muller (1963).

🔀 Family F📊 inf(run) ∈ F🏆 Most general📝 Theory

# Muller Automata
print("=" * 60)
print("MULLER AUTOMATA")
print("=" * 60)

print("""
=== Definition ===

A MULLER AUTOMATON is a 5-tuple:
  A = (Q, Σ, δ, q₀, F)

where:
  Q: finite set of states
  Σ: finite alphabet
  δ: Q × Σ → P(Q)
  q₀: initial state
  F: family of subsets of Q (F ⊆ P(Q))

=== Acceptance ===

For an infinite word w:

  A run is an infinite sequence of states.
  
  Let inf(run) = set of states visited infinitely often.
  
  The run is ACCEPTING if:
    inf(run) ∈ F

In words:
  "The set of states visited infinitely often
   is in the family F."

=== Intuition ===

F is a family of "acceptable" sets of states.
Accept if the set of states you see infinitely often
is one of the acceptable sets.

This is the most general form of acceptance.

=== Examples ===

1. Büchi as Muller:
   F = { S ⊆ Q | S ∩ F_Büchi ≠ ∅ }
   
   Accept if the infinitely often set
   contains a Büchi accepting state.

2. Rabin as Muller:
   F = { S ⊆ Q | ∃ i: S ∩ Eᵢ = ∅ and S ∩ Fᵢ ≠ ∅ }
   
   Accept if some Rabin pair is satisfied.

3. Parity as Muller:
   F = { S ⊆ Q | min{ p(q) | q ∈ S } is even }
   
   Accept if the minimum priority is even.

4. Streett as Muller:
   F = { S ⊆ Q | ∀ i: S ∩ Eᵢ ≠ ∅ ⟹ S ∩ Fᵢ ≠ ∅ }
   
   Accept if all Streett pairs are satisfied.

All these are special cases of Muller!

=== Properties ===

1. GENERALITY
   Muller is the most general acceptance condition.
   Every other condition is a special case.

2. DETERMINIZABILITY
   Every Muller automaton can be converted to
   an equivalent deterministic Muller automaton.
   
   (Muller's theorem, 1963.)

3. COMPLEMENTATION
   Easy: F^c = P(Q) \ F.
   
   Complement is just the complement family.

4. SUCCINCTNESS
   Muller can be very succinct.
   But also very complex.

5. EQUIVALENCE
   Muller ≡ Büchi ≡ Rabin ≡ Streett ≡ Parity.
   All recognize ω-regular languages.

=== Why Muller is Less Used ===

Despite being the most general:
  - Complex acceptance condition.
  - Family F can be large (2^|Q|).
  - Less intuitive than other conditions.
  - Parity is usually more convenient.

But Muller is important for:
  - Theory
  - Understanding the landscape
  - Proving equivalences

=== Applications ===

1. THEORY
   Muller automata are used to prove
   equivalences between acceptance conditions.

2. LOGIC
   Some logics use Muller conditions.

3. GAMES
   Muller games are more general than parity games.

4. VERIFICATION
   Rarely used directly.
   Usually converted to parity.

5. SYNTHESIS
   Rarely used directly.
   Usually converted to parity.
""")

# MULLER IN CODE
print("=== Muller Automata in Code ===")

class MullerAutomaton:
    """A nondeterministic Muller automaton."""
    def __init__(self, states, alphabet, transitions, initial, family):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions
        self.q0 = initial
        self.F = family  # set of frozensets of states
    
    def accepting(self, inf_states):
        """
        Check if the set of infinitely often visited states
        is in the family F.
        """
        return frozenset(inf_states) in self.F


# Example: "Infinitely many a's" as Muller
# States: q0, q1
# Family: all sets containing q1
muller_inf_a = MullerAutomaton(
    states={'q0', 'q1'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q1'},
        ('q0', 'b'): {'q0'},
        ('q1', 'a'): {'q1'},
        ('q1', 'b'): {'q0'},
    },
    initial='q0',
    family={
        frozenset({'q1'}),
        frozenset({'q0', 'q1'}),
    }
)

print("Muller automaton for 'infinitely many a's':")
print("  Q = {q0, q1}")
print("  F = {{q1}, {q0, q1}}")
print("  Accept if inf(run) ∈ F, i.e., q1 ∈ inf(run).")

print("\nTest sets of infinitely often states:")
test_sets = [
    {'q0'},
    {'q1'},
    {'q0', 'q1'},
]

for s in test_sets:
    result = muller_inf_a.accepting(s)
    print(f"  inf = {s} → {'✓' if result else '✗'}")

# Example: Parity as Muller
# Priorities: q0=1 (odd), q1=2 (even), q2=0 (even)
muller_parity = MullerAutomaton(
    states={'q0', 'q1', 'q2'},
    alphabet={'a', 'b', 'c'},
    transitions={
        ('q0', 'a'): {'q1'},
        ('q0', 'b'): {'q0'},
        ('q0', 'c'): {'q2'},
        ('q1', 'a'): {'q1'},
        ('q1', 'b'): {'q0'},
        ('q1', 'c'): {'q2'},
        ('q2', 'a'): {'q1'},
        ('q2', 'b'): {'q0'},
        ('q2', 'c'): {'q2'},
    },
    initial='q0',
    family={
        # All sets where min priority is even
        frozenset({'q2'}),
        frozenset({'q1'}),
        frozenset({'q0', 'q2'}),
        frozenset({'q1', 'q2'}),
        frozenset({'q0', 'q1', 'q2'}),
    }
)

print("\nMuller automaton (parity as Muller):")
print("  Priorities: q0=1 (odd), q1=2 (even), q2=0 (even)")
print("  Accept if min priority is even.")

print("\nTest sets:")
for s in [{'q0'}, {'q1'}, {'q2'}, {'q0', 'q1'}, {'q0', 'q2'}, {'q1', 'q2'}, {'q0', 'q1', 'q2'}]:
    result = muller_parity.accepting(s)
    print(f"  inf = {s} → {'✓' if result else '✗'}")

print("""
=== Key Observations ===

1. MOST GENERAL
   Muller is the most general acceptance condition.
   All others are special cases.

2. FAMILY F
   F is a set of subsets of Q.
   Accept if inf(run) ∈ F.

3. COMPLEMENT
   F^c = P(Q) \ F.
   Complement is just the complement family.

4. DETERMINIZABILITY
   Every Muller automaton is determinizable.
   (Muller's theorem, 1963.)

5. SUBSUMES OTHERS
   - Büchi: F = { S | S ∩ F_B ≠ ∅ }
   - Rabin: F = { S | ∃ i: S ∩ Eᵢ = ∅, S ∩ Fᵢ ≠ ∅ }
   - Streett: F = { S | ∀ i: S ∩ Eᵢ ≠ ∅ ⟹ S ∩ Fᵢ ≠ ∅ }
   - Parity: F = { S | min priority is even }

6. LESS USED
   Muller is less used in practice
   because it's more complex.
   Parity is usually preferred.

=== Why Muller Matters ===

1. THEORETICAL COMPLETENESS
   Muller completes the landscape.

2. PROOFS
   Used to prove equivalences.

3. GENERALITY
   Shows all conditions are special cases.

4. UNDERSTANDING
   Helps understand the structure of ω-automata.

5. GAMES
   Muller games are a generalization of parity games.
""")

# SUMMARY
print("""
=== Summary ===

Muller Automaton:
  - 5-tuple: (Q, Σ, δ, q₀, F)
  - F ⊆ P(Q) (family of state sets)
  - Accept if inf(run) ∈ F

Acceptance:
  The set of states visited infinitely often
  is in the family F.

Properties:
  - Most general acceptance condition
  - Subsumes Büchi, Rabin, Streett, Parity
  - Determinizable (Muller's theorem)
  - Easy complementation (complement F)
  - Equivalent to all other ω-automata

Applications:
  - Theory
  - Proving equivalences
  - Understanding ω-automata
  - Muller games

Key insight:
  Muller is the most general ω-automaton.
  All other acceptance conditions are special cases.
  It's theoretically important but
  less used in practice (parity is preferred).
""")

🔍 Determinization

🎯 Making ω-Automata Deterministic

Determinization is the process of converting a nondeterministic ω-automaton into an equivalent deterministic one. This is crucial for complementation, model checking, and synthesis.

Determinization Facts

Büchi: Not determinizable! Rabin: Determinizable (Rabin, 1969). Parity: Determinizable (Emerson-Jutla, 1991). Muller: Determinizable (Muller, 1963). Cost: Exponential blowup. Technique: Safra's construction.

🔍 Determinization❌ Büchi fails✅ Rabin/Parity work📊 Exponential

# Determinization of ω-Automata
print("=" * 60)
print("DETERMINIZATION OF ω-AUTOMATA")
print("=" * 60)

print("""
=== The Problem ===

Nondeterministic Büchi:
  - Cannot be determinized!
  - There are ω-regular languages
    that require nondeterminism for Büchi.
  - Example: "Infinitely many a's AND finitely many b's"

Rabin/Parity/Muller:
  - CAN be determinized.
  - Every Rabin automaton has an equivalent
    deterministic Rabin automaton.
  - Every parity automaton has an equivalent
    deterministic parity automaton.

=== Why Determinize? ===

1. COMPLEMENTATION
   Deterministic automata are easy to complement.
   Swap accept and reject states.

2. MODEL CHECKING
   Need deterministic automata for
   efficient model checking.

3. SYNTHESIS
   Need deterministic automata for
   reactive synthesis.

4. DECISION PROCEDURES
   Many decision procedures require
   deterministic automata.

5. LOGIC
   S1S decidability requires determinization.

=== Determinization Algorithms ===

1. SAFRA'S CONSTRUCTION (1988)
   - Converts NFA to DFA (for finite words).
   - Converts NBA to DRA (for infinite words).
   - Complexity: 2^{O(n log n)}
   - Optimal for Rabin.

2. PITEMAN'S CONSTRUCTION (2006)
   - Simpler than Safra's.
   - Determinizes Büchi to parity.
   - Complexity: 2^{O(n log n)}

3. EMPTY-LEAF CONSTRUCTION
   - Alternative to Safra's.
   - Used in practice.

4. SCHEWE'S CONSTRUCTION (2007)
   - Determinizes Büchi to Rabin.
   - Complexity: 2^{O(n log n)}

=== Safra's Construction ===

Input: NFA (or NBA) with n states.
Output: DFA (or DRA) with 2^{O(n log n)} states.

Idea:
  - States of DFA are "Safra trees."
  - A Safra tree is a tree of subsets of NFA states.
  - The tree structure encodes the nondeterminism.
  - Accepting condition tracks infinite visits.

Complexity:
  Number of Safra trees: 2^{O(n log n)}
  This is optimal for Rabin.

=== Piterman's Construction ===

Input: NBA with n states.
Output: Deterministic parity automaton with 2^{O(n log n)} states.

Idea:
  - Similar to Safra's.
  - Uses a different data structure.
  - Simpler to implement.

Advantages:
  - Simpler than Safra's.
  - Still optimal.
  - Widely used.

=== Determinization of Parity ===

Emerson-Jutla (1991):
  Every parity automaton can be determinized.
  Complexity: 2^{O(n log n)}.

But there's a simpler approach:
  1. Convert parity to Rabin.
  2. Determinize Rabin (Safra).
  3. Convert back to parity.

=== Determinization of Muller ===

Muller (1963):
  Every Muller automaton can be determinized.
  Complexity: exponential.

McNaughton (1966):
  Every Muller automaton can be converted to
  a deterministic Muller automaton.
  
This is the original determinization result.

=== The Complexity of Determinization ===

Lower bound:
  Determinization requires 2^{Ω(n log n)} states.
  (Michel, 1988)
  
This is tight:
  Safra's construction achieves 2^{O(n log n)}.

So determinization is inherently exponential.
But optimal algorithms exist.

=== Applications ===

1. MODEL CHECKING
   Determinize property automaton.
   Check if system ⊆ property.

2. SYNTHESIS
   Determinize specification.
   Construct system.

3. LOGIC
   S1S decidability.
   μ-calculus model checking.

4. VERIFICATION
   Protocol verification.
   Hardware verification.

5. GAMES
   Determinize winning condition.
   Solve game.
""")

# DETERMINIZATION IN CODE
print("=== Determinization in Code (Conceptual) ===")

class NFA:
    """Simple NFA for demonstration."""
    def __init__(self, states, alphabet, transitions, initial, accept):
        self.Q = states
        self.Sigma = alphabet
        self.delta = transitions  # (state, symbol) -> set of states
        self.q0 = initial
        self.F = accept
    
    def to_dfa(self):
        """
        Subset construction (for finite words).
        For ω-words, Safra's construction is needed.
        """
        from itertools import chain
        
        # Start state: epsilon closure of {q0}
        start = frozenset({self.q0})
        dfa_states = {start}
        dfa_delta = {}
        dfa_F = set()
        
        queue = [start]
        visited = {start}
        
        while queue:
            current = queue.pop(0)
            
            # Check if accepting
            if current & self.F:
                dfa_F.add(current)
            
            # For each symbol
            for symbol in self.Sigma:
                next_set = set()
                for state in current:
                    next_set |= self.delta.get((state, symbol), set())
                
                next_frozen = frozenset(next_set)
                dfa_delta[(current, symbol)] = next_frozen
                
                if next_frozen not in visited:
                    visited.add(next_frozen)
                    queue.append(next_frozen)
        
        return {
            'states': dfa_states,
            'delta': dfa_delta,
            'initial': start,
            'accept': dfa_F,
        }


# Example NFA
nfa = NFA(
    states={'q0', 'q1', 'q2'},
    alphabet={'a', 'b'},
    transitions={
        ('q0', 'a'): {'q0', 'q1'},
        ('q0', 'b'): {'q0'},
        ('q1', 'b'): {'q2'},
        ('q2', 'a'): {'q2'},
        ('q2', 'b'): {'q2'},
    },
    initial='q0',
    accept={'q2'}
)

print("NFA for 'strings containing ab':")
print("  Q = {q0, q1, q2}")
print("  F = {q2}")

dfa = nfa.to_dfa()
print(f"\nDeterminized DFA:")
print(f"  States: {len(dfa['states'])}")
print(f"  Accept: {len(dfa['accept'])}")

for s in sorted(dfa['states'], key=str):
    marker = " *" if s in dfa['accept'] else ""
    print(f"    {set(s)}{marker}")

print("""
=== Key Observations ===

1. SUBSET CONSTRUCTION
   For finite words, subset construction works.
   States of DFA = subsets of NFA states.

2. FOR INFINITE WORDS
   Subset construction doesn't work directly.
   Need Safra's or Piterman's construction.
   Because acceptance depends on infinite behavior.

3. COMPLEXITY
   Finite words: 2^n states.
   Infinite words: 2^{n log n} states.
   (Safra's construction.)

4. BÜCHI CAN'T BE DETERMINIZED
   Nondeterministic Büchi is strictly more powerful
   than deterministic Büchi.
   But can be converted to deterministic Rabin/parity.

5. APPLICATIONS
   Determinization is crucial for:
   - Complementation
   - Model checking
   - Synthesis
   - Logic

=== The Determinization Pipeline ===

For model checking:

  1. Property (LTL) → NBA
  2. NBA → Deterministic Rabin/Parity
  3. System → Deterministic automaton
  4. Check if System ∩ ¬Property = ∅

For synthesis:

  1. Specification → NBA
  2. NBA → Deterministic Parity
  3. Solve parity game
  4. Extract strategy
  5. Construct system

Determinization is the key step.
""")

# SUMMARY
print("""
=== Summary ===

Determinization:
  - Convert nondeterministic ω-automaton
    to deterministic equivalent.

Key facts:
  - Büchi: NOT determinizable.
  - Rabin: Determinizable (Rabin, 1969).
  - Parity: Determinizable (Emerson-Jutla, 1991).
  - Muller: Determinizable (Muller, 1963).

Algorithms:
  - Safra's construction: 2^{O(n log n)}
  - Piterman's construction: simpler
  - Schewe's construction: Büchi to Rabin

Complexity:
  - Lower bound: 2^{Ω(n log n)}
  - Upper bound: 2^{O(n log n)}
  - Optimal!

Applications:
  - Complementation
  - Model checking
  - Synthesis
  - Logic (S1S)
  - Verification

Key insight:
  Determinization is exponential but optimal.
  It's essential for many applications.
  Büchi can't be determinized,
  but Rabin/parity can.
  Safra's construction is the key algorithm.
""")

📝 ω-Regular Expressions

🎯 Regular Expressions for Infinite Words

ω-Regular expressions extend classical regular expressions to describe ω-languages. They provide a convenient algebraic notation for ω-regular languages.

ω-Regular Expressions Facts

Syntax: Extend regex with ^ω. Semantics: L(E^ω) = infinite repetitions. Equivalence: Same as ω-automata. Kleene: ω-Kleene theorem. Applications: Specification, verification. History: Büchi (1962).

📝 ω-regex♾️ E^ω🔄 Kleene theorem📊 Specification

# ω-Regular Expressions
print("=" * 60)
print("ω-REGULAR EXPRESSIONS")
print("=" * 60)

print("""
=== Definition ===

ω-REGULAR EXPRESSIONS extend regular expressions:

  E ::= ∅ | ε | a | E₁ + E₂ | E₁ · E₂ | E*
       | E^ω

where:
  a ∈ Σ: single symbol
  ∅: empty language
  ε: empty word
  E₁ + E₂: union
  E₁ · E₂: concatenation
  E*: Kleene star
  E^ω: infinite repetition

=== Semantics ===

L(∅) = ∅
L(ε) = {ε}
L(a) = {a}
L(E₁ + E₂) = L(E₁) ∪ L(E₂)
L(E₁ · E₂) = L(E₁) · L(E₂)
L(E*) = (L(E))*
L(E^ω) = { w₀w₁w₂... | each wᵢ ∈ L(E), wᵢ ≠ ε }

Note: E^ω means "infinitely many repetitions of E."

=== Examples ===

1. "Infinitely many a's":
   (a+b)* · (a(a+b)*)^ω
   
   Or: (a+b)* · (a(a+b)*)^ω
   
   Explanation: 
     - (a+b)*: any finite prefix.
     - (a(a+b)*)^ω: infinitely many a's.
   
   Simpler: (a+b)* · (a(a+b)*)^ω

2. "Finitely many a's":
   (a+b)* · b^ω
   
   Explanation:
     - (a+b)*: finite prefix.
     - b^ω: infinitely many b's.
   
   This means: eventually always b.
   Equivalently: finitely many a's.

3. "Eventually always a":
   (a+b)* · a^ω
   
   Explanation:
     - (a+b)*: finite prefix.
     - a^ω: always a forever.

4. "Infinitely often a and b":
   (a+b)* · ((a+b)* · a · (a+b)* · b)^ω
   
   This is more complex.
   It says: infinitely many blocks
   containing both a and b.

5. "Every a is followed by b":
   (b + ab)^ω
   
   Explanation:
     - b: a b with no a.
     - ab: an a followed by b.
     - ^ω: repeat forever.
   
   This ensures every a has a following b.

=== Kleene's Theorem for ω-Words ===

THEOREM (Büchi, 1962):
  L is ω-regular
  ⟺
  L = L(E) for some ω-regular expression E.

This is the ω-version of Kleene's theorem.

Proof idea:
  (→) Convert ω-automaton to ω-regex.
  (←) Convert ω-regex to ω-automaton.

Both directions are constructive.

=== The ω-Regular Expression Algebra ===

Identities:
  E + ∅ = E
  E · ε = E
  ∅ · E = ∅
  (E*)* = E*
  (E₁ + E₂)* = (E₁* · E₂*)*
  E^ω · E^ω = E^ω (if E ≠ ∅)
  (E*)^ω = E^ω (if E ≠ ∅)

These help simplify expressions.

=== Applications ===

1. SPECIFICATION
   Specify properties of systems:
     "Infinitely often a"
     "Eventually always b"
     "Every request is followed by a response"

2. VERIFICATION
   Check if system satisfies specification.
   System ⊆ Specification.

3. SYNTHESIS
   Construct system from specification.

4. LOGIC
   ω-regular expressions are equivalent to:
   - Büchi automata
   - LTL (partially)
   - S1S (monadic second-order logic)

5. PATTERN MATCHING
   Infinite pattern matching.
   Stream processing.
""")

# ω-REGEX IN CODE
print("=== ω-Regular Expressions in Code ===")

class OmegaRegex:
    """Simple representation of ω-regular expressions."""
    def __init__(self, description):
        self.description = description
    
    def __repr__(self):
        return self.description


# Examples
examples = [
    OmegaRegex("(a+b)* · (a(a+b)*)^ω"),
    OmegaRegex("(a+b)* · b^ω"),
    OmegaRegex("(a+b)* · a^ω"),
    OmegaRegex("(b + ab)^ω"),
    OmegaRegex("(a+b)* · ((a+b)* · a · (a+b)* · b)^ω"),
]

print("Examples of ω-regular expressions:")
for i, ex in enumerate(examples, 1):
    print(f"  {i}. {ex}")

print("""
=== Key Properties ===

1. INFINITELY OFTEN
   E^ω means "infinitely many repetitions of E."
   This is the key new operator.

2. EVENTUALLY
   (a+b)* · a^ω means "eventually always a."
   This is the eventually operator.

3. FAIRNESS
   (b + ab)^ω means "every a is followed by b."
   This is a fairness condition.

4. EQUIVALENCE
   ω-regular expressions ≡ ω-automata.
   Both recognize ω-regular languages.

5. ALGEBRA
   ω-regular expressions have algebraic laws.
   These help simplify and manipulate.

=== The Power of ω-Regular Expressions ===

1. CONCISE
   ω-regular expressions are often more concise
   than automata.

2. INTUITIVE
   They resemble regular expressions,
   which are familiar.

3. ALGEBRAIC
   They support algebraic reasoning.

4. SPECIFICATION
   They're natural for specifying properties.

5. EQUIVALENT
   They're equivalent to ω-automata,
   so we can convert between them.

=== ω-Regular Expressions vs LTL ===

LTL (Linear Temporal Logic):
  G a: always a
  F a: eventually a
  G F a: infinitely often a
  F G a: eventually always a

ω-regular expressions:
  a^ω: always a (from some point)
  (a+b)* · a^ω: eventually always a
  (a+b)* · (a(a+b)*)^ω: infinitely often a

LTL is a subset of ω-regular.
Not all ω-regular languages are LTL-definable.
LTL is more intuitive for specifications.
ω-regular is more expressive.
""")

# SUMMARY
print("""
=== Summary ===

ω-Regular Expression:
  - Extends regular expressions with ^ω
  - E ::= ∅ | ε | a | E₁+E₂ | E₁·E₂ | E* | E^ω
  - L(E^ω) = infinite repetitions of L(E)

Examples:
  - (a+b)* · b^ω: finitely many a's
  - (a+b)* · a^ω: eventually always a
  - (b + ab)^ω: every a followed by b

Kleene's theorem:
  L is ω-regular ⟺ L = L(E) for some ω-regex E

Algebra:
  - Identities for simplification
  - E^ω · E^ω = E^ω
  - (E*)^ω = E^ω

Applications:
  - Specification
  - Verification
  - Synthesis
  - Logic

Key insight:
  ω-regular expressions are the "regular expressions"
  of infinite words.
  They're equivalent to ω-automata.
  They're concise and algebraic.
  They're used for specification and verification.
""")

💼 Applications

🎯 ω-Automata in the Real World

ω-Automata are the foundation of model checking, program verification, and reactive synthesis. They're used to verify hardware, protocols, and software systems.

Application Areas

Model checking: Verify systems. Temporal logic: LTL, CTL*. Synthesis: Construct systems. Hardware: Circuit verification. Protocols: Protocol verification. Software: Program verification.

🔍 Model checking📝 LTL🏗️ Synthesis💻 Verification

# Applications of ω-Automata
print("=" * 60)
print("APPLICATIONS OF ω-AUTOMATA")
print("=" * 60)

# 1. MODEL CHECKING
print("""
=== 1. Model Checking ===

Model checking:
  Given a system M and a property φ,
  does M satisfy φ?

  M ⊨ φ?

Approach:
  1. Model M as an ω-automaton.
  2. Model φ as an ω-automaton.
  3. Check if L(M) ⊆ L(φ).
  4. Equivalently: L(M) ∩ L(¬φ) = ∅.

Steps:
  1. System → Kripke structure → ω-automaton.
  2. Property (LTL) → ω-automaton.
  3. Complement property.
  4. Intersect.
  5. Check emptiness.

Applications:
  - Hardware verification
  - Protocol verification
  - Software verification
  - Embedded systems

Tools:
  - SPIN (LTL)
  - NuSMV (CTL, LTL)
  - PRISM (probabilistic)
  - UPPAAL (timed)

=== 2. Temporal Logic ===

Linear Temporal Logic (LTL):
  G a: always a
  F a: eventually a
  X a: next a
  a U b: a until b
  G F a: infinitely often a
  F G a: eventually always a

LTL → Büchi automaton:
  - Each LTL formula → NBA
  - Size: exponential in formula length
  - Used in model checking

Computation Tree Logic (CTL*):
  - More expressive than LTL
  - Includes path quantifiers
  - CTL* → ω-automaton

μ-calculus:
  - Fixed-point logic
  - Model checking → parity games
  - Very expressive

=== 3. Synthesis ===

Reactive synthesis:
  Given a specification φ,
  construct a system M such that M ⊨ φ.

Approach:
  1. Specification φ → ω-automaton.
  2. Determinize (parity).
  3. Solve parity game.
  4. Extract winning strategy.
  5. Construct system.

Applications:
  - Controller synthesis
  - Protocol synthesis
  - Robot planning

Tools:
  - Acacia
  - Lily
  - RATSY
  - BoSy
""")

# 4. HARDWARE VERIFICATION
print("""
=== 4. Hardware Verification ===

Hardware circuits are reactive systems:
  - Run forever
  - Respond to inputs
  - Have infinite behavior

Properties:
  - Safety: "Something bad never happens."
  - Liveness: "Something good eventually happens."
  - Fairness: "Every request is eventually granted."

ω-Automata model:
  - Circuit → ω-automaton.
  - Property → ω-automaton.
  - Check inclusion.

Examples:
  - Cache coherence protocols
  - Bus protocols
  - Memory controllers
  - Processors

Tools:
  - Cadence
  - Synopsys
  - Mentor Graphics

=== 5. Protocol Verification ===

Network protocols are reactive systems:
  - Run forever
  - Send/receive messages
  - Handle failures

Properties:
  - "Every message is eventually delivered."
  - "No message is duplicated."
  - "The protocol never deadlocks."
  - "The protocol is fair."

ω-Automata model:
  - Protocol → ω-automaton.
  - Property → ω-automaton.
  - Check inclusion.

Examples:
  - TCP
  - HTTP
  - Bluetooth
  - Security protocols

Tools:
  - SPIN
  - UPPAAL
  - ProVerif

=== 6. Software Verification ===

Software is a reactive system:
  - Runs forever (server, OS).
  - Responds to inputs.
  - Has infinite behavior.

Properties:
  - "The program never crashes."
  - "Every request is eventually handled."
  - "No memory leaks."

ω-Automata model:
  - Program → ω-automaton (abstract).
  - Property → ω-automaton.
  - Check inclusion.

Challenges:
  - Infinite state space.
  - Undecidability.
  - Abstraction needed.

Tools:
  - SLAM (Microsoft)
  - BLAST
  - CPAchecker
""")

# 7. SUMMARY TABLE
print("""
=== Application Summary ===

Domain              Use Case                ω-Automata Role
────────────────────────────────────────────────────────────
Model Checking      Verify systems          Check inclusion
Temporal Logic      Specify properties      LTL → Büchi
Synthesis           Construct systems       Parity games
Hardware            Circuit verification    ω-regular properties
Protocols           Protocol verification   ω-regular properties
Software            Program verification    ω-regular properties
Games               Game solving            Parity games
Logic               S1S decidability        Determinization

Key observations:
  - Model checking is the primary application.
  - LTL → Büchi is the key translation.
  - Parity games are central.
  - Determinization is essential.
  - ω-Automata are everywhere in verification.

=== 8. Case Study: LTL Model Checking ===

Given:
  - System M (Kripke structure)
  - LTL property φ

Question:
  Does M satisfy φ?

Algorithm:
  1. Convert φ to NBA A_φ.
  2. Convert ¬φ to NBA A_¬φ.
  3. Build product M × A_¬φ.
  4. Check if product has an accepting run.
  5. If yes: M does NOT satisfy φ.
     If no: M satisfies φ.

Complexity:
  - PSPACE-complete (in |φ|).
  - Polynomial in |M|.
  - Exponential in |φ|.

Optimizations:
  - On-the-fly construction.
  - Symbolic representation (BDDs).
  - Partial order reduction.
  - Bounded model checking.

Tools:
  - SPIN
  - NuSMV
  - LTSmin
  - Spot
""")

# 9. TAKEAWAYS
print("""
=== Practical Takeaways ===

1. MODEL CHECKING
   ω-Automata are the foundation.
   System ⊆ Property.

2. TEMPORAL LOGIC
   LTL → Büchi.
   CTL* → ω-Automata.
   μ-calculus → Parity games.

3. SYNTHESIS
   Specification → Parity game.
   Solve → Construct system.

4. VERIFICATION
   Hardware, protocols, software.
   ω-regular properties.

5. GAMES
   Parity games are central.
   Solving games = model checking.

6. DETERMINIZATION
   Essential for complementation.
   Exponential but optimal.

7. TOOLS
   SPIN, NuSMV, PRISM, UPPAAL.
   Used in industry.

Key insight:
  ω-Automata are not just theory.
  They're the foundation of
  formal verification and synthesis.
  They're used to verify real systems.
  They're essential for reliable computing.
""")

🚀 Advanced Topics

🎯 Beyond Basic ω-Automata

ω-Automata connect to many advanced topics: probabilistic automata, timed automata, weighted automata, and quantum automata.

Advanced Directions

Probabilistic: Markov decision processes. Timed: Real-time systems. Weighted: Quantitative properties. Quantum: Quantum automata. Games: Stochastic games. Learning: Automata learning.

🎲 Probabilistic⏱️ Timed📊 Weighted⚛️ Quantum

# Advanced Topics
print("=" * 60)
print("ADVANCED TOPICS")
print("=" * 60)

# 1. PROBABILISTIC AUTOMATA
print("""
=== 1. Probabilistic ω-Automata ===

Probabilistic automata:
  - Transitions have probabilities.
  - Acceptance with probability.

Markov Decision Processes (MDPs):
  - Probabilistic transitions.
  - Nondeterministic choices.
  - Used in planning, RL.

Probabilistic ω-Automata:
  - Infinite words.
  - Probabilistic acceptance.
  - Used in verification.

Applications:
  - Randomized protocols.
  - Fault-tolerant systems.
  - AI planning.
  - Reinforcement learning.

Tools:
  - PRISM
  - Storm
  - Modest

=== 2. Timed Automata ===

Timed automata:
  - Clocks (real-valued).
  - Time constraints.
  - Infinite state space.

Timed ω-Automata:
  - Infinite words with time.
  - Real-time properties.
  - Used in real-time systems.

Applications:
  - Real-time protocols.
  - Embedded systems.
  - Cyber-physical systems.

Tools:
  - UPPAAL
  - Kronos
  - HyTech

=== 3. Weighted Automata ===

Weighted automata:
  - Transitions have weights.
  - Compute weighted languages.
  - Used in NLP, ML.

Weighted ω-Automata:
  - Infinite words.
  - Weighted acceptance.
  - Quantitative properties.

Applications:
  - Speech recognition.
  - Machine translation.
  - NLP.
  - Machine learning.

Tools:
  - OpenFST
  - PyTorch (for weighted automata)

=== 4. Quantum Automata ===

Quantum automata:
  - Quantum states.
  - Unitary transitions.
  - Measurement at end.

Quantum ω-Automata:
  - Infinite words.
  - Quantum acceptance.
  - Research area.

Applications:
  - Quantum computing.
  - Quantum verification.
  - Quantum NLP.

Research:
  - Still experimental.
  - Theoretical interest.
  - Potential applications.
""")

# 5. STOCHASTIC GAMES
print("""
=== 5. Stochastic Games ===

Stochastic games:
  - Two players.
  - Probabilistic transitions.
  - ω-regular winning conditions.

Applications:
  - Verification of probabilistic systems.
  - Synthesis with uncertainty.
  - Security.
  - Economics.

Solving stochastic games:
  - Reduce to MDPs.
  - Use value iteration.
  - Use strategy improvement.

Tools:
  - PRISM-games
  - GIST
  - MultiGain

=== 6. AUTOMATA LEARNING ===

Automata learning:
  - Learn automata from data.
  - Angluin's L* algorithm.
  - Active learning.

Learning ω-Automata:
  - Learn from infinite words.
  - Harder than finite words.
  - Active research.

Applications:
  - Program synthesis.
  - Verification.
  - Model inference.
  - Testing.

Tools:
  - LearnLib
  - TTT
  - AALpy

=== 7. OPEN PROBLEMS ===

1. PARITY GAMES IN P?
   Are parity games solvable in polynomial time?
   Currently: in QP (quasi-polynomial).
   Open: in P?

2. DETERMINIZATION LOWER BOUNDS
   Is 2^{n log n} optimal?
   Yes (Michel, 1988).
   But are there better algorithms for special cases?

3. PROBABILISTIC VERIFICATION
   Scalability.
   State space explosion.
   Symbolic methods.

4. TIMED AUTOMATA
   Scalability.
   Real-time verification.
   Decidability boundaries.

5. QUANTUM AUTOMATA
   Power and limitations.
   Practical applications.
   Still early.

6. LEARNING ω-AUTOMATA
   Efficient algorithms.
   Scalability.
   Applications.
""")

# 8. RECOMMENDATIONS
print("""
=== Recommendations ===

For students:
  1. Master basic ω-Automata first.
  2. Understand Büchi and parity.
  3. Learn determinization (Safra).
  4. Study model checking.
  5. Explore applications.

For researchers:
  1. Parity games in P?
  2. Probabilistic verification.
  3. Timed automata.
  4. Learning ω-Automata.
  5. Quantum automata.

For practitioners:
  1. Use model checking tools.
  2. Understand LTL → Büchi.
  3. Apply to verification.
  4. Use synthesis tools.
  5. Know the limitations.

=== Final Thoughts ===

ω-Automata are:

✓ FOUNDATIONAL
  For verification and synthesis.

✓ ELEGANT
  Simple definitions, deep theory.

✓ PRACTICAL
  Used in industry.

✓ CONNECTED
  To logic, games, verification.

✓ EVOLVING
  Probabilistic, timed, quantum.

✓ CHALLENGING
  Open problems remain.

Key takeaway:
  ω-Automata are the foundation of
  formal verification and synthesis.
  They model infinite behavior.
  They're used to verify real systems.
  They connect logic, games, and computation.
  
  Understanding ω-Automata is essential
  for anyone working in verification,
  synthesis, or formal methods.

"The infinite is not just a mathematical
 curiosity; it's the key to verifying
 real systems."
  — Formal Methods Researcher

Go verify something!
""")

# QUICK REFERENCE
print("""
=== Quick Reference ===

ω-Automaton:
  - Processes infinite words.
  - Acceptance based on infinite behavior.

Types:
  Büchi: some accepting state ∞ often.
  Rabin: ∃ pair (E,F): E finitely, F infinitely.
  Streett: ∀ pairs (E,F): E ∞ ⟹ F ∞.
  Parity: min priority ∞ often is even.
  Muller: inf(run) ∈ F.

Properties:
  - All recognize ω-regular languages.
  - All equivalent in power.
  - Parity is determinizable.
  - Büchi is NOT determinizable.

Determinization:
  - Safra's construction: 2^{O(n log n)}
  - Optimal (Michel's lower bound).
  - Essential for complementation.

Applications:
  - Model checking
  - Temporal logic (LTL)
  - Synthesis
  - Verification
  - Games

Key insight:
  ω-Automata model infinite behavior.
  They're the foundation of verification.
  Parity is the most elegant.
  Determinization is essential.
  Used in industry.
""")