A Model Checker for Value-Passing Mu-Calculus Using Logic Programming

C. R. Ramakrishnan


Abstract:

Recent advances in logic programming have been successfully used to build practical verification toolsets, as evidenced by the XMC system. Thus far, XMC has supported value-passing process languages, but has been limited to using the propositional fragment of modal mu-calculus as the property specification logic. In this paper, we explore the use of data variables in the property logic. In particular, we present value-passing modal mu-calculus, its formal semantics and describe a natural implementation of this semantics as a logic program. Since logic programs naturally deal with variables and substitutions, such an implementation need not pay any additional price--- either in terms of performance, or in complexity of implementation--- for having the added flexibility of data variables in the property logic. Our preliminary implementation supports this expectation.


Bibtex Entry:

@inproceedings{Ram:PADL01,
author = {C. R. Ramakrishnan},
title = {A Model Checker for Value-Passing Mu-Calculus Using Logic Programming},
booktitle = {Practical Aspects of Declarative Languages ({PADL})},
address = {Las Vegas, Nevada},
month = {March},
series = {Lecture Notes in Computer Science},
volume = {1990},
publisher = {Springer},
pages = {1--13},
year = {2001}
}


Full Paper: [pdf]


Home | Papers

C. R. Ramakrishnan
(cram@cs.sunysb.edu)