Edward Liem: Extraction of Invariants in Parameterised Boolean Equation Systems

Event Details

Parameterised Boolean Equation Systems (PBESs) are used to express and solve various model checking and equivalence checking problems. However, it may not always be efficient, or even possible, to find a solution to PBESs since they may encode undecidable problems. One particular technique towards finding a solution to a PBES is the concept of exploiting global PBES invariants. Although invariants have been studied extensively, there is a lack of research towards invariant discovery and exploitation in PBESs. Our paper presents PBES invariant extraction techniques inspired from various concepts found in program verification literature well as provide new conditions for invariance properties. We also present a novel graph structure, namely relevancy graphs, which characterize relevant predicate variable instances of instantiated PBES equations. Using relevancy graphs, we illustrate how invariants interact with PBESs as well as provide an alternative criteria to proving the PBES global invariant condition in simple functions.