A method for making proof graph finite on disjunctive parameterised Boolean equation systems

摘要

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 paper studies a technique to solve the membership problem of PBESs, which is undecidable, by extending the notion of proof graphs. 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. However, proof graphs are infinite in general, thus we introduce verticies each of which stands for a set of verticies of the original ones. For a subclass of disjunctive PBESs, we clarify conditions for the extended proof graphs. We also show that examples having no finite proof graph except for extended one. We further propose a method to construct a graph, called a dependency space, that contains an extended proof graph in its sub-graphs.