< Back to previous page


Reconstructing and Improving Parity Game Solvers with Justifications

Book - Dissertation

In certain industries, such as medical or aerospace, failure can result inunacceptable losses. To ensure safety, checks are implemented for every stepin the process: standards, certifications, testing, maintenance schedules. . . For
software, this encompasses researching diverse approaches including automatictesting, safer programming languages, declarative languages to separateknowledge from execution, or generating provably correct software from alist of expected behaviours.This thesis is situated in the domains exploring the two last ideas: KnowledgeRepresentation and Reasoning (KRR) and Formal Verification (FV). KRRresearches how knowledge can be represented for humans while supporting(automatic) reasoning with this knowledge. Formal Verification focuses onmodelling the behaviour of systems, verifying correct behaviour in all relevantscenarios.One technique, used in KRR for improving reasoning capabilities of algorithms,is called justifications. Justifications store how consequences were derived in agraph used for tracing unsupported arguments when invalidating assumptions.This text explores how justifications improve parity game algorithms, which playa central role in FV. A parity game is an infinite two-player game on a directedgraph. The core problem of a parity game is deciding the winner of certainnodes and a corresponding strategy. The solution of a parity game informswhether an implementation is valid or allows extracting a valid implementation.First, justifications are adapted to parity games. We introduce an operationJustify to manipulate justifications for solving parity games. Then, four well-known recursive algorithms are reconstructed using this operation. Thesenew variants are also implemented and evaluated experimentally and showjustifications improve the state-of-the-art algorithms. Finally, we show thatjustifications for parity games are equivalent to justifications for propositionalnested fixpoint definitions, an older logic with different applications.
Publication year:2021