TY - GEN
T1 - A model checker for value-passing mu-calculus using logic programming
AU - Ramakrishnan, C. R.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2001
PY - 2001
Y1 - 2001
N2 - 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 mucalculus as the property specification logic. In this paper, we explore the use of data variables in the property logic. In particular, we present valuepassing 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.
AB - 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 mucalculus as the property specification logic. In this paper, we explore the use of data variables in the property logic. In particular, we present valuepassing 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.
UR - https://www.scopus.com/pages/publications/84871949948
U2 - 10.1007/3-540-45241-9_1
DO - 10.1007/3-540-45241-9_1
M3 - Conference contribution
AN - SCOPUS:84871949948
SN - 9783540417682
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 13
BT - Practical Aspects of Declarative Languages - 3rd International Symposium, PADL 2001, Proceedings
A2 - Ramakrishnan, I.V.
PB - Springer Verlag
T2 - 3rd International Symposium on Practical Aspects of Declarative Languages, PADL 2001
Y2 - 11 March 2001 through 12 March 2001
ER -