Local and symbolic bisimulation using tabled constraint logic programming

Abstract

Bisimulation is a fundamental notion that characterizes behavioral equivalence of concurrent systems. In this paper, we study the problem of encoding efficient bisimulation checkers for finite- as well as infinite-state systems as logic programs. We begin with a straightforward andshort (less than 10 lines) encoding of finite-state bisimulation checker as a tabledlogic program. In a goal-directedsystem like XSB, this encoding yields a local bisimulation checker: one where state space exploration is done only until a dissimilarity is revealed. More importantly, the logic programming formulation of local bisimulation can be extended to do symbolic bisimulation for checking the equivalence of infinite-state concurrent systems representedb y symbolic transition systems. We show how the two variants of symbolic bisimulation (late andearly equivalences) can be formulatedas a tabledconstrain t logic program in a way that precisely brings out their differences. Finally, we show that our symbolic bisimulation checker actually outperforms non-symbolic checkers even for relatively small finite-state systems.