Solving Games Without Determinization

The synthesis of reactive systems requires the solution of two-player games on graphs with -regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic B

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Thomas A. Henzinger, Nir Piterman
• Keywords: Automated Reasoning, CSL 2006, Equivalent Deterministic Automaton, Nondeterministic B¨uchi, Nondeterministic Parity Automaton