The logic programming encoding of the set-theoretic graph property known as bisimulation is analyzed. This notion is of central importance in non-well-founded set theory, semantics of concurrency, model checking, and coinductive reasoning. From a modeling point of view, it is particularly interesting since it allows two alternative high-level characterizations. We analyze the encoding style of these modelings in various dialects of Logic Programming. Moreover, the notion also admits a polynomial-time maximum fixpoint procedure that we implemented in Prolog. Similar graph problems which are instead NP hard or not yet perfectly classified (e.g., graph isomorphism) can inherit most from the declarative encodings presented.
Graph bisimulation is the key notion for stating equality in non-well-founded-set
theory
The problem of establishing whether two graphs are bisimilar (hence, the sets
‘represented’ by those graphs are equivalent) admits fast polynomial time algorithms that
optimize a naive maximum fixpoint algorithm
The work is partially supported by INdAM GNCS 2014 and 2015 projects. one used for defining other “NP” properties such as graph/subgraph simulation or isomorphism. The second one is based on the notion of coarsest stable partition which is itself similar to the property exploited for computing the minimum deterministic finite automata for a given regular language.
The focus of the paper is the analysis of the programming style to be used for modeling the maximum bisimulation problem in a way as declarative way as possible in some dialects of logic programming, namely, Prolog, Constraint Logic Programming on Finite Domains, Answer Set Programming, Co-inductive Logic Programming, and the set-based constraint logic programming language flogg (read setlog). Although the contribution of this paper is not on the direction of improving existing polynomial time algorithms, the problem is also encoded in Prolog as a (polynomial-time) maximum fixpoint algorithm.
The paper contributes to the series of papers on “Set Graphs” (e.g.,
A preliminary version of this work appeared in
Familiarity with basic notions of set theory, first-order logic, and Logic Programming is
assumed. We introduce some notions needed for understanding the contribution of the
paper; the reader is referred, e.g., to
Sets are made by elements. The extensionality principle (E) states that two sets are equal if and only if they contain the same elements: 8z (z 2 x $ z 2 y) ! x = y (E) (the , apparently missing, direction is a consequence of equality). In “classical” set theory sets are assumed to be well-founded; in particular the 2 relation fulfills the so-called foundation axiom (F A): 8x x 6= ; ! (9y 2 x)(x \ y = ;) (F A) that ensures that a set cannot contain an infinite descending chain x0 3 x1 3 x2 3 of elements. In particular, let us observe that a set x such that x = fxg cannot exist since x is not empty, its unique element y is x itself, and x \ y = fyg 6= ;, contradicting the axiom.
On the other hand, cyclic phenomena are rather common in our experience. For instance,
in Knowledge Representation, a cyclic argument is introduced for modeling the frame
problem in presence of static causal laws
Representing and reasoning on these problems leads us to (cyclic) directed graphs with a
distinguished entry point. Precisely, an accessible pointed graph (apg) hG; i is a directed
graph G = hN; Ei together with a distinguished node 2 N (the point) such that all the
nodes in N are reachable from
Intuitively, an edge a ! b means that the set “represented by b” is an element of the set
“represented by a”. The graph edge ! stands, in a sense, for the Peano symbol 3. The
above idea is used to decorate an apg, namely, assigning a (possibly non-well-founded) set
to each of the nodes
If the graph contains cycles, interpreting edges as membership implies that the set which
decorates the graph is no longer well-founded. Non-well-founded sets are often referred to
as hypersets. To allow their existence, axiom (FA) is removed from the theory and it is
replaced by the Anti Foundation Axiom (AFA)
Each apg has a unique decoration. Therefore two apgs denote the same hyperset if and only if their decoration is the same. The notion introduced to establish formally this fact is the notion of bisimulation.
Let G1 = hN1; E1i and G2 = hN2; E2i be two graphs, a bisimulation between G1 and G2 is a relation b N1 N2 such that: In case G1 and G2 are apgs pointed in 1 and 2, respectively, it is also required that 1 b 2. If there is a bisimulation between G1 and G2 then the two graphs are said to be bisimilar.
Let us consider again the leftmost and center apgs of Figure 2. It is immediate to check
that the relation f(X11; X12); (X11; X22); (X11; X32)g is a bisimulation between them.
Remark 2.1 (Bisimulation and Isomorphism)
Let us observe that if b is required to be a bijective function then it is a graph isomorphism.
Establishing whether two graphs are isomorphic is an NP-problem neither proved to be
NPcomplete nor in P. Establishing whether G1 is isomorphic to a subgraph of G2 (subgraph
isomorphism) is NP-complete
In case G1 and G2 are the same graph G = hN; Ei, a bisimulation on G is a bisimulation
between G and G. It is immediate to see that there is a bisimulation between two apg’s
hG1; 1i and hG2; 2i if and only if there is a bisimulation b on the graph G = hf g [
N1 [ N2; f( ; 1); ( ; 2)g [ E1 [ E2i such that 1 b 2 (see, e.g.,
The graph obtained by collapsing nodes according to the equivalence relation is the one that allows us to obtain the apg decoration, using the following procedure:
Let G = hhN; Ei; i be an apg. For each node i 2 N assign uniquely a variable Xi, then add the equation Xi = fXj : (i; j) 2 Eg. The set of equations obtained defines the set decorating G, that can be retrieved as the solution of X .
Another characterization of the maximum bisimulation is based on the notion of stability. Given a set N , a partition P of N is a collection of non-empty disjoint sets (blocks) B1; B2; : : : such that Si Bi = N . If the number of blocks is k, we say that the partition has size k. Let E be a binary relation on the set N , with E 1 = f(b; a) : (a; b) 2 Eg we denote its inverse relation. If B N , we define E 1(B) = fa 2 N : (a; b) 2 E; b 2 Bg.
A partition P of N is said to be stable with respect to E if and only if (8B1 2 P )(8B2 2 P )(B1
E 1(B2) _ B1 \ E 1(B2) = ;) (2) which is in turn equivalent to stating that there do not exist two blocks B1 2 P and B2 2 P such that: (9x 2 B1)(9y 2 B1) (x 2 E 1(B2) ^ y 2= E 1(B2)) (20)
A partition P refines a partition Q if each block of P is contained in a block of Q. A block B2 of P splits a block B1 of P if B1 is replaced in P by C1 = B1 \ E 1(B2) and C2 = B1 n E 1(B2) and both of them are not empty. In this case B2 is called a splitter (operationally, the split operation can be made even if one of them is empty; in this case it is not added in P and B1 is replaced by itself, leading to a fix point). The split operation produces a refinement of a partition P ; if P is stable with respect to E, no split operation changes P .
It can be shown that given a graph G = hN; Ei, starting from the partition P = fN g,
after at most jN j 1 split operations a procedure halts determining the coarsest stable
partition (CSP) w.r.t. E. Namely, the partition is stable and any other stable partition is a
refinement of it. Moreover, and this is relevant to our purposes, the CSP corresponds to the
partition induced by the maximum bisimulation, hence this algorithm can be employed to
compute it in polynomial time
We first focus on the logic programming declarative encoding of the definition of bisimulation (1) or (10) and of the part needed for the maximum bisimulation on an input apg. We impose that the relation is symmetric and reflexive. In the remaining part of the paper we assume that apg’s are represented by facts node(1). node(2). ... for enumerating the nodes, and facts edge(u,v). where u and v are nodes, for enumerating the edges. For the sake of simplicity, we also assume that node 1 is the point of the apg.1 Prolog. The programming style used in the Prolog encoding is generate & test. The core of the encoding is reported in Figure 3. A bisimulation is represented by a list of pairs of nodes (U; V ). Assuming a “guessed” bisimulation is given as input, for every guessed pair
the morphism property (1) is checked. As usual in Prolog, the “for all” property is implemented by a recursive predicate (although a slightly more compact foreach statement is available in most Prolog systems and will be used in successive encodings).
bis/1 is called by a predicate that guesses a bisimulation of size at least k between nodes, itself called by a meta predicate that increases the value of k until no solution is found. The guess predicate forces all identities, all the pairs between nodes without outgoing edges, and imposes symmetries; this extra part of the code is rather boring and its code has been omitted. As a (weak) search strategy, the guess predicate tries first to insert as much pairs as possible: this will explain the difference of computational times on different benchmarks of the same size.
CLP(FD). The programming style is constraint & generate. In this case the bisimulation is stored in a matrix, say B, of Boolean variables. B[i; j] = 1 means that i b j (B[i; j] = 0 means that :(i b j)). We omit the definitions of the reflexivity predicate that sets B[i; i] = 1 for all nodes i and of the symmetry predicate that sets B[i; j] = B[j; i] for all pairs of nodes i and j. Let us focus on the morphism requirements (1). morphism/2 collects all edges and nodes and calls morphismcheck/4 (Figure 4). This predicate scans each edge (U 1; V 1) and each node U 2 and adds the property that if B[U 1; U 2] = 1 then P(U2;V 2)2E B[V 1; V 2] 1. Let us observe that O(jEjjN j) of these constraints are generated. We omit the definitions of some auxiliary predicates, such as access(X,Y,B,N,BXY) that simply sets BXY = B[X,Y]. The whole encoding is longer and perhaps less intuitive than the Prolog one. However, the search of the maximum bisimulation is not delegated to a meta predicate as in Prolog, but it is encoded directly into the maximize option of the labeling primitive. The “down” search strategy, trying to assign 1 firstly, is similar to the strategy used in the Prolog code.
ASP. ASP encodings allow us to define explicitly the bisimulation relation. Two rules are
added for forcing symmetry and reflexivity. Then a non-deterministic choice is added to
each pair of nodes. The great declarative advantage of ASP in this case is the availability
of constraint rules that allow us to express universal quantification (negation of existential
quantification). The morphism requirement (10) can be therefore encoded as it is, with the
unique addition of the node predicates needed for grounding (Figure 5). Then we define
the notion of representative nodes (the node of smallest index among those equivalent
to it) and minimize the number of them. This has proven to be much more efficient that
maximizing the size of bis. A final remark on the expected size of the grounding. Both
the constraint and the definition of one son bis range over all edges and another free
node: this generates a grounding of size O(jEjjN j).
co-LP. In this section we exploit a less standard logic programming dialect. Coinductive
Logic Programming (briefly co-LP) was introduced by
% Recursively analyze B bis([],_). bis([ (U1,U2) |RB],B) :successors(U1,SU1), successors(U2,SU2), allbis(SU1,SU2,B), bis(RB,B). allbis([],_,_). allbis([V1 | SU1],SU2,B) :member(V2,SU2), member( (V1,V2),B), allbis(SU1,SU2,B).
%%% if U1 bis U2 %%% Collect the successors SU1 of U1 %%% Collect the successors SU2 of U2 %%% Then recursively consider SU1 %%% If V1 is a successor of U1 %%% there is a V2 successor of U2 %%% such that V1 bis V2 successors(X,SX) :- findall(Y,edge(X,Y),SX). bis :- size(N), M is N*N, %%% Define the N * N Boolean length(B,M), domain(B,0,1), %%% Matrix B constraint(B,N), Max #= sum(B), %%% Max is the number of pairs labeling([maximize(Max),ffc,down],B). %%% in the bisimulation constraint(B,N) :- reflexivity(N,B), symmetry(1,2,N,B), morphism(N,B). morphism(N,B) :findall( (X,Y),edge(X,Y),EDGES), foreach( E in EDGES, U2 in 1..N, morphismcheck(E,U2,N,B)). morphismcheck( (U1,V1),U2,N,B) :access(U1,U2,B,N,BU1U2), % Flag BU1U2 stands for (U1 B U2) successors(U2, SuccU2), % Collect all edges (U2,V2) collectlist(SuccU2,V1,N,B,BLIST),% BLIST contains all possible flags BV1V2 BU1U2 #=< sum(BLIST). % If (U1 B U2) there is V2 s.t. (V1 B V2) %% Minimization (max bisimulation) non_rep_node(A) :- node(A;B), bis(A,B), B < A. rep_node(A) :- node(A), not non_rep_node(A). numbernodes(N) :- N = #count{A : rep_node(A)}. #minimize {N : numbernodes(N)}. available for this problem. As a matter of fact, the piece of code reported in Figure 6 encodes the problem and, by looking for the maximum fixpoint, the maximum bisimulation is computed without the need of additional minimization/maximization directives. bis and allbis are declared as coinductive. The definition of successors is the same as in Figure 3 and declared as inductive, as well as the member predicate. bis(U,V) :- successors(U,SU), successors(V,SV),
allbis(SU,SV), allbis(SV,SU). allbis([],_ ). allbis([U|R],SV ) :
member(V,SV), bis(U,V), allbis(R,SV). We focus first on the encoding of the definition of stable partition (2) and finally on the (less declarative) computation of the CSP.
Prolog. The programming style is generate & test. A partition is a list of non-empty lists of nodes (blocks). Sink nodes (if any) are deterministically set in the first block. Possible partitions of increasing size are non-deterministically generated until the first stable one is found. Once the partition is guessed, the verify part is made by a double selection of blocks within the list of blocks. The main predicate that encodes property (2) is the following: stablecond(B1,B2) :- edgeinv(B2,InvB2),
(subseteq(B1,InvB2) ; emptyintersection(B1,InvB2)). where edgeinv collects the nodes that enter into B2 (definable as findall(X, (edge(X,Y), member(Y,B)), REVB)) while the two set-theoretic predicates are defined through list operations.
CLP(FD). In this case the data structure used is a mapping from nodes to blocks indexes, stored as a list of finite domain variables. The set inclusion and empty intersection requirements of (2) are not naturally implemented by a constraint & generate style. As in the previous CLP(FD) encoding maximization is forced by a parameter of the labeling; some symmetry breaking is encoded (e.g.. sink nodes are deterministically forced to stay in partition number one). In Figure 7 we only report the excerpt of the encoding, where we made use of the foreach built-in. With a rough analysis, the number of constraints needed is O(jN j3), but each constraint generated by alledge can be of size jN j itself.
ASP. Also in this case ASP allows a concise encoding (Figure 8). The assignment is
implemented defining the predicate (used as function) inblock/2. The possibility of
reasoning “a posteriori” and the availability of the constraint rule allow us to naturally encode
the property (20). The remaining part of the code is devoted to symmetry breaking and
minimization of the number of blocks. The bottleneck for the grounding stage is the constraint
rule that might generate O(jN j4) ground instantiations.
flogg. The CLP language flogg, originally presented in
We have implemented the maximum fixpoint procedure for computing the coarsest stable
partition in Prolog. Initially nodes are split into (at most) two blocks: internal and not
internal nodes (i.e., sinks). For each node U , a list of pairs U -I is computed by stating that
U is assigned to block I. Then a possible splitter is found and, in case, a split is executed.
The procedure terminates in at most n 1 splitting steps where n is the number of nodes.
The Prolog code is available in
Although the focus of this work is on the expressivity of the declarative encoding (this
problem is solved by fast algorithms in literature, such as
Graph G1 is an acyclic graph with n 1 edges, where n blocks are needed. G2 is a cyclic graph with n nodes and edges. If n is even, just two blocks are sufficient; if n is odd, n+1 blocks are needed. This is why in some experiments we have 2 two columns with this family of graphs.
G3 is a binary tree populated following a breadth-first visit, with n 1 edges. G4 is, in a sense, symmetrical w.r.t. G1: it is a complete graph with n2 edges but just one block is sufficient.
G5 is a multilevel (cyclic) graph.
In Figure 11 the results for the graph G2 (which has been selected as a good representative of the overall situation; e.g., both grounding and search times are sensible G1
G2 (n odd)
G3
G5 in this family of graphs) are graphically summarized. Running times include constraintgeneration/grounding time and search time. As far as the declarative, non procedural encodings presented, the ASP encoding is a clear winner, while, as one might expect, the Prolog implementation of the polynomial time algorithm is still better.
All details for the five families of graphs are reported in the tables in
As anticipated, the ASP encoding is a clear winner. Prolog generate & test and the co-LP interpreter run in reasonable time on very small graphs only (Prolog is used without tabling, tabling the edge predicate allows a speed-up of roughly 4 times). The CLP approach becomes unpractical soon in the case of the complete graph G4 where the n2 edges generate too many constraints for the stack size when n 50 (O(jEjjN j) constraints are added: in this case they are O(n5); moreover each of those constraints includes a sum of n elements). Let us observe that the complete graph G4 produces the highest grounding times in the ASP case. Grounding size is expected O(jEjjN j) = O(n3) in this case. This has been verified experimentally (table not reported); in particular, for G4; n = 200 the grounded file (obtained with the option -t) is of size 275MB. Moreover, by a simple regression analysis of our results, the time needed for grounding is shown to be proportional to n6 for graph G4.
With the enconding of the coarsest stable partition definition (2) the graphs that can be handled by all approaches are smaller, and ASP is still a clear winner. We have omitted the flogg running times. This system proved to be definitely the slowest; just to have an idea, for G1, n = 5 the computation took roughly 5 hours.
We conclude with testing the encoding of the polynomial time procedure of coarsest
stable partition computation by maximum fixpoint and splits. In graphs G2 and G3 tabling
the edge predicate improved the running time of two orders of magnitude (reported times
are those using tabling). As a further consideration, we started finding stack overflow for
n = 5000. Moreover, the experimental complexity detected by a regression analysis of
the results is O(jN j3) in all columns, which is rather good, considering the purely
declarative nature of the encoding (fast solvers such as
We have encoded the two properties characterizing the bisimulation definition, and in particular, solving the maximum bisimulation problem, using some dialects of Logic Programming. As a general remark, the guess & verify style of Prolog (and of ASP) allows us to define the characterizing properties to be verified ‘a posteriori’, on ground atoms. In CLP instead, those properties are added as constraints to lists of values that are currently non instantiated and this makes things much more involved, and has a negative impact on code readability. The expressive power of the constraint rule of ASP allows a natural and compact encoding of “for all” properties and this improves the conciseness of the encoding (and readability in general); recursion must be used instead to it in Prolog and CLP. co-LP (resp., flogg) allows us to write excellent code for property (1) (resp., property (2)). However, since they are implemented adopting meta interpreters (naive in the case of co-LP) their execution times are prohibitive for being used in practice.
The ASP encoding is also the winner from the efficiency point of view, as far as a purely
declarative encoding of the a NP property on graphs is concerned. This would suggest to
the reader that this is the best dialect to be used to encode graph properties if a polynomial
time algorithm is not yet available (or it does not exist at all). This is not the case for
the maximum bisimulation problem where polynomial time algorithms for computing the
coarsest stable partition can be employed. The one implemented in Prolog (available in