Speaker:

Zihui Liang (University of Electronic Science and Technology of China)

Time:

• 16:20-17:20 (Time in Beijing)
• March 3, 2023 (Friday)

Venue:

518, Research Building 4

Abstract:

We introduce Muller games. These are two player games played on finite graphs. They are used to model reactive systems that interact with enviroment. They are also used in model checking applications. To solve a Muller game means to find out the winner of the game that starts at a given vertex of the graph. In 2008 Florian Horn provided a polynomial time solution for Muller games. His proof, however, is unclear and contains many non-trivial gaps. We analyse Horn’s algorithm and provide an indpendent proof that Horn’s algorithm is correct.