Lecture 3 [slides]

summary

• review of alternating Büchi automata
  • basic automata constructions
  • translation from alternating Büchi automata to Büchi automata
• Expressive power: LTL vs. nondeterministic Büchi automata
• Branching-time logics: CTL and CTL*

references

• “Alternating finite automata on ω-words”, Miyano & Hayashi, 1984
• “Alternating automata and program verification”, Vardi, 1995
• “An Until Hierarchy and Other Applications of an Ehrenfeucht–Fraı̈ssé Game for Temporal Logic”, Etessami & Wilke, 2000
• “Principles of Model Checking”, Baier & Katoen, §4.3, 5