From business rule systems to logic.

In certain industries, such as medical or aerospace, failure can result in
unacceptable losses. To ensure safety, checks are implemented for every step
in the process: standards, certifications, testing, maintenance schedules. . . Forsoftware, this encompasses researching diverse approaches including automatic
testing, safer programming languages, declarative languages to separate
knowledge from execution, or generating provably correct software from a
list of expected behaviours.
This thesis is situated in the domains exploring the two last ideas: Knowledge
Representation and Reasoning (KRR) and Formal Verification (FV). KRR
researches how knowledge can be represented for humans while supporting
(automatic) reasoning with this knowledge. Formal Verification focuses on
modelling the behaviour of systems, verifying correct behaviour in all relevant
scenarios.
One technique, used in KRR for improving reasoning capabilities of algorithms,
is called justifications. Justifications store how consequences were derived in a
graph used for tracing unsupported arguments when invalidating assumptions.
This text explores how justifications improve parity game algorithms, which play
a central role in FV. A parity game is an infinite two-player game on a directed
graph. The core problem of a parity game is deciding the winner of certain
nodes and a corresponding strategy. The solution of a parity game informs
whether an implementation is valid or allows extracting a valid implementation.
First, justifications are adapted to parity games. We introduce an operation
Justify to manipulate justifications for solving parity games. Then, four well-
known recursive algorithms are reconstructed using this operation. These
new variants are also implemented and evaluated experimentally and show
justifications improve the state-of-the-art algorithms. Finally, we show that
justifications for parity games are equivalent to justifications for propositional
nested fixpoint definitions, an older logic with different applications.