A Model Checker for Value-Passing Mu-Calculus Using Logic Programming
- 225 Downloads
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.
Unable to display preview. Download preview PDF.
- [CES86]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.Google Scholar
- [Cha00]William Chan. Temporal logic queries. In Computer Aided Verification (CAV), 2000.Google Scholar
- [FGK+96]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.Google Scholar
- [GL88]M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In International Conference on Logic Programming, pages 1070–1080, 1988.Google Scholar
- [Mat98]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.Google Scholar
- [Mil89]R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.Google Scholar
- [MRRV00]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.Google Scholar
- [RH97]J. Rathke and M. Hennessy. Local model checking for value-passing processes. In International Symposium on Theoretical Aspects of Computer Software, 1997.Google Scholar
- [RRR+97]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.Google Scholar
- [RRS+00]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.
- [vRS91]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.Google Scholar
- [XSB]The XSB logic programming system. Available from http://xsb.sourceforge.net.