Reduced Dependency Spaces for Existential Parameterised Boolean Equation Systems

TL;DR

This paper introduces a method to reduce infinite dependency spaces of a subclass of parameterised Boolean equation systems to finite graphs using equivalence relations, enabling decidable membership checking.

Contribution

It proposes a technique to construct finite dependency spaces for a subclass of PBESs by identifying equivalence relations, with a sound procedure and implementation using an SMT solver.

Findings

Finite dependency spaces can be constructed for certain PBES subclasses.

The proposed method is implemented and tested on examples including a downsized McCarthy 91 function.

The approach enables decidable membership problems for previously undecidable cases.

Abstract

A parameterised Boolean equation system (PBES) is a set of equations that defines sets satisfying the equations as the least and/or greatest fixed-points. Thus this system is regarded as a declarative program defining predicates, where a program execution returns whether a given ground atomic formula holds or not. The program execution corresponds to the membership problem of PBESs, which is however undecidable in general. This paper proposes a subclass of PBESs which expresses universal-quantifiers free formulas, and studies a technique to solve the problem on it. We use the fact that the membership problem is reduced to the problem whether a proof graph exists. To check the latter problem, we introduce a so-called dependency space which is a graph containing all of the minimal proof graphs. Dependency spaces are, however, infinite in general. Thus, we propose some conditions for equivalence relations to preserve the result of the membership problem, then we identify two vertices as the same under the relation. In this sense, dependency spaces possibly result in a finite graph. We show some examples having infinite dependency spaces which are reducible to finite graphs by equivalence relations. We provide a procedure to construct finite dependency spaces and show the soundness of the procedure. We also implement the procedure using an SMT solver and experiment on some examples including a downsized McCarthy 91 function.