Title: An Extension of Proof Graphs for Disjunctive Parameterised Boolean Equation Systems,
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.