Local and symbolic bisimulation using tabled constraint logic programming. (English) Zbl 1053.68582

Basu, Samik; Mukund, Madhavan; Ramakrishnan, C. R.; Ramakrishnan, I. V.; Verma, Rakesh

Codognet, Philippe (ed.), Logic programming. 17th international conference, ICLP 2001, Paphos, Cyprus, November 26 – December 1, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42935-2). Lect. Notes Comput. Sci. 2237, 166-180 (2001).

Summary: 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 and short (less than 10 lines) encoding of finite-state bisimulation checker as a tabled logic program. In a goal-directed system 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 represented by symbolic transition systems. We show how the two variants of symbolic bisimulation (late and early equivalences) can be formulated as a tabled constraint 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.
For the entire collection see [Zbl 0977.00040].

MSC:

68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N17	Logic programming

Software:

XSB