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 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.
Research supported in part by NSF grants EIA-9705998 and CCR-9876242.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.
William Chan. Temporal logic queries. In Computer Aided Verification (CAV), 2000.
W. Chen and D. S. Warren. Tabled evaluation with delaying for general ogic programs. Journal of the ACM, 43(1):20–74, January 1996.
J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M Sighireanu. CADP (CAESAR/ALDEBERAN development package): protocol validation and verification toolbox. In Computer Aided Verificaon (CAV), volume 1102 of Lecture Notes in Computer Science, pages 437–440, 1996.
M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In International Conference on Logic Programming, pages 1070–1080, 1988.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
R. Mateescu. Local model checking of an alternation-free value-based modal mu-calculus. In Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI), 1998.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
M. Mukund, C. R. Ramakrishnan, I. V. Ramakrishnan, and R. Verma. Symbolic bisimulation using tabled constraint logic programming. In International Workshop on Tabulation in Parsing and Deduction (TAPD), 2000.
J. Rathke and M. Hennessy. Local model checking for value-passing processes. In International Symposium on Theoretical Aspects of Computer Software, 1997.
Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. L. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV’ 97), Haifa, Israel, July 1997. Springer-Verlag.
C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V.N. Venkatakrishnan. XMC: A logicprogramming-based verification toolset. In Computer Aided Verification (CAV), 2000. XMC is available from http://www.cs.sunysb.edu/$¡m$lmc.
A. van Gelder, K. A. Ross, and J. S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3), 1991.
The XSB logic programming system. Available from http://xsb.sourceforge.net.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramakrishnan, C.R. (2001). A Model Checker for Value-Passing Mu-Calculus Using Logic Programming. In: Ramakrishnan, I.V. (eds) Practical Aspects of Declarative Languages. PADL 2001. Lecture Notes in Computer Science, vol 1990. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45241-9_1
Download citation
DOI: https://doi.org/10.1007/3-540-45241-9_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41768-2
Online ISBN: 978-3-540-45241-6
eBook Packages: Springer Book Archive