Set Graphs VI: Logic Programming and Bisimulation.
Agostino Dovier · 2014
Abstract. We analyze the declarative encoding of the set-theoretic graph property known as bisimulation. 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 partic-ularly interesting since it allows two alternative high-level characteriza-tions. We analyze the encoding style of these modelings in various dialects of Logic Programming. Moreover, the notion also admits a polynomial-time maximum fix point procedure that we implemented in Prolog. Sim-ilar graph problems which are NP hard or not yet perfectly classified (e.g., graph isomorphism) can benefit from the encodings presented. 1