## 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)`