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 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. Local checking can often outperform the traditional global checking by several orders of magnitude even for finite-state systems, as our experimental results show. Surprisingly, even when the systems are equivalent where the entire state space may need to be explored, the performance of our local checker is comparable to hand-coded equivalence checking algorithms implemented in other verification tools.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. We use a a constraint meta-interpreter over disequality constraints that evaluates tabled constraint logic programs to support the symbolic bisimulation checker. We present experimental results to illustrate the practical efficacy of our logic programming based symbolic bisimulation checker. Finally, we show that our symbolic bisimulation checker, despite the overheads imposed by the constraint meta-interpreter, actually outperforms non-symbolic checkers even for relatively small finite-state systems.
Bibtex Entry:
@inproceedings{BMRRV:ICLP01, author = {Samik Basu and Madhavan Mukund and C. R. Ramakrishnan and I. V. Ramakrishnan and Rakesh M. Verma}, title = {Local and Symbolic Bisimulation Using Tabled Constraint Logic Programming}, booktitle = {International Conference on Logic Programming ({ICLP})}, address = {Paphos, Cyprus}, month = {November}, series = {Lecture Notes in Computer Science}, volume = {2237}, publisher = {Springer}, pages = {166--180}, year = {2001} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)