Maurice Laveaux: On The Fly Solving for Symbolic Parity Games

Event Details

In model checking we are interested in determining whether a property is satisfied for a given system. In particular, we want to know whether the property holds for the initial state of the system. We often see, especially while developing the model, that properties are already violated in relatively few steps from the initial state. Therefore, we can attempt to verify the property while exploring the state space of the system to find violations early. This approach has already successfully been applied for explicit verification and we lift this to symbolic verification. We use symbolic parity games to encode the model checking question. In this talk I will present the symbolic exploration technique extended with several partial solving methods.