Abstract
Multi-valued model-checking is an extension of classical model-checking to reasoning about systems with uncertain information, which are common during early design stages. The additional values of the logic are used to capture the degree of uncertainty. In this paper, we show that the multi-valued μ-calculus model-checking problem is reducible to several classical model-checking problems. The reduction allows one to reuse existing model-checking tools and algorithms to solve multi-valued model-checking problems. This paper generalizes, extends and corrects previous work in this area, done in the context of 3-valued models, symbolic model-checking, and De Morgan algebras.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)
Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning about Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Transactions on Computers 8(C-35), 677–691 (1986)
Chan, W.: Temporal-Logic Queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)
Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model- Checking. ACM Transactions on Software Engineering and Methodology (2003) (accepted for publication.)
Chechik, M., Devereux, B., Easterbrook, S., Lai, A., Petrovykh, V.: Efficient Multiple- Valued Model-Checking Using Lattice Representations. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 451–465. Springer, Heidelberg (2001)
Chechik, M., Devereux, B., Gurfinkel, A.: χChek: A Multi-Valued Model-Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 505–509. Springer, Heidelberg (2002)
Chechik, M., Easterbrook, S.: Model-Checking Over Multi-Valued Logics. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 72–98. Springer, Heidelberg (2001)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier Science Publishers, Amsterdam (1990)
Fitting, M.: Many-Valued Modal Logics. Fundamenta Informaticae 15(3-4), 335–350 (1991)
Fitting, M.: Many-Valued Modal Logics II. Fundamenta Informaticae 17, 55–73 (1992)
Fitting, M.C.: Intuitionistic Logic Model Theory and Forcing. North-Holand Publishing Co, Amsterdam (1969)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-Based Model Checking Using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)
Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206–222. Springer, Heidelberg (2002)
Gurfinkel, A., Chechik, M., Devereux, B.: Temporal Logic Query Checking: A Tool for Model Exploration. IEEE Transactions on Software Engineering (2003) (accepted for publication)
Huth, M., Jagadeesan, R., Schmidt, D.: A Domain Equation for Refinement of Partial Systems. In: Mathematical Structures in Computer Science (2003) (accepted for publication)
Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Huth, M., Pradhan, S.: An Ontology for Consistent Partial Model Checking. Electronic Notes in Theoretical Computer Science 23 (2003)
Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, NewYork (1952)
Konikowska, B., Penczek, W.: Model Checking for Multi-Valued CTL*. In: Fitting, M., Orlowska, E. (eds.) Multi-Valued Logics (2002) (to appear)
Konikowska, B., Penczek, W.: Reducing Model Checking from Multi-Valued CTL* to CTL*. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 226. Springer, Heidelberg (2002)
Kozen, D.: Results on the Propositional μ-calculus. Theoretical Computer Science 27, 334–354 (1983)
Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS 1988), pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)
Milner, R.: Communication and Concurrency. Prentice-Hall, New York (1989)
Müller-Olm, M., Schmidt, D., Steffen, B.: Model-Checking:A Tutorial Introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)
Rasiowa, H.: An Algebraic Approach to Non-Classical Logics. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1978)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gurfinkel, A., Chechik, M. (2003). Multi-valued Model Checking via Classical Model Checking. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-45187-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40753-9
Online ISBN: 978-3-540-45187-7
eBook Packages: Springer Book Archive