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] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)