Efficient model checking using tabled resolution

Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David S. Warren

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We demonstrate the feasibility of using the XSB tabled logic programming system as a programmable fixed-point engine for implementing efficient local model checkers. In particular, we present XMC, an XSB-based local model checker for a CCS-like value-passing language and the alternation-free fragment of the modal mu-calculus. XMC is written in under 200 lines of XSB code, which constitute a declarative specification of CCS and the modal mu-calculus at the level of semantic equations. In order to gauge the performance of XMC as an algorithmic model checker, we conducted a series of benchmarking experiments designed to compare the performance of XMC with the local model checkers implemented in C/C++ in the Concurrency Factory and SPIN specification and verification environments. After applying certain newly developed logic-programming-based optimizations (along with some standard ones), XMC's performance became extremely competitive with that of the Factory and shows promise in its comparison with SPIN.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 9th International Conference, CAV 1997, Proceedings
EditorsOrna Grumberg
PublisherSpringer Verlag
Pages143-154
Number of pages12
ISBN (Print)3540631666, 9783540631668
DOIs
StatePublished - Jan 1 1997
Event9th International Conference on Computer-Aided Verification, CAV 1997 - Haifa, Israel
Duration: Jun 22 1997Jun 25 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1254
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Computer-Aided Verification, CAV 1997
CountryIsrael
CityHaifa
Period6/22/976/25/97

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Efficient model checking using tabled resolution'. Together they form a unique fingerprint.

Cite this