Local and symbolic bisimulation using tabled constraint logic programming

Basu, Samik ; Mukund, Madhavan ; Ramakrishnan, C. R. ; Ramakrishnan, I. V. ; Verma, Rakesh (2001) Local and symbolic bisimulation using tabled constraint logic programming In: 17th International Conference on Logic Programming (ICLP 2001 ), 26 Nov - 01 Dec 2001, Paphos, Cyprus.

Full text not available from this repository.

Official URL: https://link.springer.com/chapter/10.1007/3-540-45...

Related URL: http://dx.doi.org/10.1007/3-540-45635-X_19


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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag.
ID Code:114216
Deposited On:25 May 2018 04:55
Last Modified:25 May 2018 04:55

Repository Staff Only: item control page