An Extension of Proof Graphs for Disjunctive Parameterised Boolean Equation Systems

Yutaro Nagae
(Nagoya University)
Masahiko Sakai
(Nagoya University)
Hiroyuki Seki
(Nagoya University)

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.

In Horatiu Cirstea and Santiago Escobar: Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Porto, Portugal, 23rd June 2016, Electronic Proceedings in Theoretical Computer Science 235, pp. 46–61.
Published: 1st January 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: