Using SMT for solving fragments of parameterised boolean equation systems

Abstract

Fixpoint logics such as parameterised Boolean equation systems (PBESs) provide a unifying framework in which a number of practical decision problems can be encoded. Efficient evaluation methods (solving methods in the terminology of PBESs) are needed to solve the encoded decision problems. We present a sound pseudo-decision procedure that uses SMT solvers for solving conjunctive and disjunctive PBESs. These are important fragments, allowing to encode typical verification problems and planning problems. Our experiments, conducted with a prototype implementation, show that the new solving procedure is complementary to existing techniques for solving PBESs.