An Extension of Proof Graphs for Disjunctive Parameterised Boolean Equation Systems

TL;DR

This paper extends proof graphs for disjunctive parameterised Boolean equation systems, introducing reduced proof graphs and dependency spaces to address the undecidable membership problem by enabling finite representations.

Contribution

It proposes reduced proof graphs and dependency spaces for disjunctive PBESs, providing a method to construct finite graphs for solving the membership problem.

Findings

Reduced proof graphs can be finite for certain PBES subclasses.

A procedure to construct finite reduced dependency spaces is provided.

The method is sound and complete for the classes considered.

Abstract

A parameterised Boolean equation system (PBES) is a set of equations that defines sets as the least and/or greatest fixed-points that satisfy the equations. This system is regarded as a declarative program defining functions that take a datum and returns a Boolean value. The membership problem of PBESs is a problem to decide whether a given element is in the defined set or not, which corresponds to an execution of the program. This paper introduces reduced proof graphs, and studies a technique to solve the membership problem of PBESs, which is undecidable in general, by transforming it into a reduced proof graph. A vertex X(v) in a proof graph represents that the data v is in the set X, if the graph satisfies conditions induced from a given PBES. Proof graphs are, however, infinite in general. Thus we introduce vertices each of which stands for a set of vertices of the original ones, which possibly results in a finite graph. For a subclass of disjunctive PBESs, we clarify some conditions which reduced proof graphs should satisfy. We also show some examples having no finite proof graph except for reduced one. We further propose a reduced dependency space, which contains reduced proof graphs as sub-graphs if a proof graph exists. We provide a procedure to construct finite reduced dependency spaces, and show the soundness and completeness of the procedure.