Abstract
This article introduces the concept of multi-valued model-checking and describes a multi-valued symbolic model-checker, ΧChek. Multi-valued model-checking is a generalization of classical model-checking, useful for analyzing models that contain uncertainty (lack of essential information) or inconsistency (contradictory information, often occurring when information is gathered from multiple sources). Multi-valued logics support the explicit modeling of uncertainty and disagreement by providing additional truth values in the logic.This article provides a theoretical basis for multi-valued model-checking and discusses some of its applications. A companion article [Chechik et al. 2002b] describes implementation issues in detail. The model-checker works for any member of a large class of multi-valued logics. Our modeling language is based on a generalization of Kripke structures, where both atomic propositions and transitions between states may take any of the truth values of a given multi-valued logic. Properties are expressed in ΧCTL, our multi-valued extension of the temporal logic CTL.We define the class of logics, present the theory of multi-valued sets and multi-valued relations used in our model-checking algorithm, and define the multi-valued extensions of CTL and Kripke structures. We explore the relationship between ΧCTL and CTL, and provide a symbolic model-checking algorithm for ΧCTL. We also address the use of fairness in multi-valued model-checking. Finally, we discuss some applications of the multi-valued model-checking approach.
- Anderson, A. and Belnap, N. 1975. Entailment. Vol. 1. Princeton University Press.]]Google Scholar
- Back, R.-J. and von Wright, J. 1998. Refinement Calculus: A Systematic Approach. Springer-Verlag.]] Google ScholarDigital Library
- Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., and Somenzi, F. 1993. Algebraic decision diagrams and their applications. In IEEE /ACM International Conference on Computer-Aided Disign (ICCAD'93) (Santa Clara, CA). IEEE Computer Society Press, pp. 188--191.]] Google ScholarDigital Library
- Baier, C. and Clarke, E. M. 1998. The algebraic Mu-calculus and MTBDDs. In Proceedings of the 5th Workshop on Logic, Language, Information and Computation, (WoLLIC'98), pp. 27--38.]]Google Scholar
- Baier, C., Clarke, E. M., Hartonas-Garmhausen, V., Kwiatkowska, M. Z., and Ryan, M. 1997. Symbolic model checking for probabilistic processes. In Automata, Languages and Programming, 24th Annual Colloquium, (Bologna, Italy). P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, eds., Lecture Notes in Computer Science, vol. 1256, Springer, pp. 430--440.]] Google ScholarDigital Library
- Belnap, N. 1977. A useful four-valued logic. In Modern Uses of Multiple-Valued Logic, Donn and Epstein, eds., Reidel, pp. 30--56.]]Google Scholar
- Berney, G. and dos Santos, S. 1985. Elevator Analysis, Design and Control. IEE Control Engineering Series 2. Peter Peregrinus Ltd.]]Google Scholar
- Birkhoff, G. 1967. Lattice Theory (3rd Edition). Americal Mathematical Society, Providence, RI.]]Google Scholar
- Bolc, L. and Borowik, P. 1992. Many-Valued Logics. Springer-Verlag.]] Google ScholarDigital Library
- Bruns, G. and Godefroid, P. 1999. Model checking partial state spaces with 3-valued temporal logics. In Proceedings of the 11th International Conference on Computer-Aided Verification (CAV'99), (Trento, Italy). Lecture Notes in Computer Science, vol. 1633, Springer, pp. 274--287.]] Google ScholarDigital Library
- Bruns, G. and Godefroid, P. 2000. Generalized model checking: Reasoning about partial state spaces. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00), C. Palamidessi, eds., Lecture Notes in Computer Science, vol. 1877, Springer, pp. 168--182.]] Google ScholarDigital Library
- Chan, W. 2000. Temporal-logic queries. In Proceedings of the 12th Conference on Computer Aided Verification (CAV'00), E. Emerson and A. Sistla, eds., Lecture Notes in Computer Science, vol. 1855, Springer, pp. 450--463.]] Google ScholarDigital Library
- Chechik, M., Devereux, B., and Easterbrook, S. 2001a. Implementing a multi-valued symbolic model-checker. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), Lecture Notes in Computer Science, vol. 2031, Springer, pp. 404--419.]] Google ScholarDigital Library
- Chechik, M., Devereux, B., and Gurfinkel, A. 2001b. Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In Proceedings of the 8th SPIN Workshop on Model Checking Software, Toronto, Canada. Lecture Notes in Computer Science, vol. 2057, Springer, pp. 16--36,]] Google ScholarDigital Library
- Chechik, M., Devereux, B., and Gurfinkel, A. 2002a. ΧChek: a multi-valued model-checker. In Proceedings of the 14th International Conference on Computer-Aided Verification (CAV'02), Copenhagen, Denmark. Lecture Notes in Computer Science, Springer, pp. 505--509.]] Google ScholarDigital Library
- Chechik, M. and Ding, W. 2002. Lightweight reasoning about program correctness. Inf. Syst. Frontiers, 4, 4, pp. 363--377.]] Google ScholarDigital Library
- Chechik, M., Gurfinkel, A., Devereux, B., Lai, A., and Easterbrook, S. 2002b. Symbolic data structures for multi-valued model-checking. CSRG Tech Report 446, University of Toronto. Submitted for publication.]]Google Scholar
- Chechik, M. and MacCaull, W. 2003. CTL model-checking over logics with non-classical negation. In Proceedings of the 33rd IEEE International Symposium on Multi-Valued Logics (ISMVL'03) (Tokyo, Japan). pp. 293--300,]] Google ScholarDigital Library
- Clarke, E., Emerson, E., and Sistla, A. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8, 2, pp. 244--263.]] Google ScholarDigital Library
- Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press.]] Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1977. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'77) (Los Angeles, CA). ACM Press, pp. 238--252.]] Google ScholarDigital Library
- Dams, D. 1996. Abstract Interpretation and Partition Refinement for Model Checking. PhD Thesis, Eindhoven University of Technology, The Netherlands.]]Google Scholar
- Dams, D., Gerth, R., and Grumberg, O. 1997. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 2, 19, pp. 253--291.]] Google ScholarDigital Library
- Davey, B. and Priestley, H. 1990. Introduction to Lattices and Order. Cambridge University Press.]]Google Scholar
- Devereux, B. 2002. Strong next-time operators for multiple-valued μ-calculus. In Proceedings of FLOC'02 Workshop on Fixpoints in Computer Science (FICS) (Copenhagen, Denmark), pp. 40--43.]]Google Scholar
- Dunn, J. 1999. A comparative study of various model-theoretic treatments of negation: a history of formal negation. In What is Negation, D. Gabbay and H. Wansing, eds., Kluwer Academic Publishers.]]Google Scholar
- Easterbrook, S. and Chechik, M. 2001. A framework for multi-valued reasoning over inconsistent viewpoints. In Proceedings of the International Conference on Software Engineering (ICSE'01) (Toronto, Canada), IEEE Computer Society Press, pp. 411--420.]] Google ScholarDigital Library
- Fitting, M. 1991a. Many-valued modal logics. Fund. Info., 15, 3--4, pp. 335--350.]] Google ScholarDigital Library
- Fitting, M. C. 1991b. Kleene's logic, generalized. J. Log. Comput., 1, 6, pp. 797--810.]]Google ScholarCross Ref
- Fitting, M. 1992. Many-valued modal logics II. Fund. Info., 17, pp. 55--73.]] Google ScholarDigital Library
- Gaines, B. R. 1979. Logical foundations for database systems. Intern. J. Man-Mach. Studies, 11, 4, pp. 481--500.]]Google ScholarCross Ref
- Ginsberg, M. 1987. Multi-valued logic. In Readings in Nonmonotonic Reasoning, M. Ginsberg, ed., Morgan-Kaufmann Publishing, pp. 251--255.]] Google ScholarDigital Library
- Ginsberg, M. L. 1988. Multivalued logics: a uniform approach to reasoning in artificial intelligence. Comput. Intell., 4, 3, pp. 265--316.]]Google ScholarCross Ref
- Godefroid, P., Huth, M., and Jagadeesan, R. 2001. Abstraction-based model checking using modal transition systems. In Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01) (Aalborg, Denmark), K. Larsen and M. Nielsen, eds., Lecture Notes in Computer Science, vol. 2154, Springer, pp. 426--440.]] Google ScholarDigital Library
- Godefroid, P. and Jagadeesan, R. 2003. On the expressiveness of 3-valued models. In Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'03), Lecture Notes in Computer Science, vol. 2575, Springer, pp. 206--222.]] Google ScholarDigital Library
- Goguen, J. 1967. L-fuzzy sets. J. Math. Anal. Applic., 18, 1, pp. 145--174.]]Google ScholarCross Ref
- Gurfinkel, A. 2002. Multi-valued symbolic model-checking: fairness, counter-examples, running time. Master's Thesis, Department of Computer Science, University of Toronto.]]Google Scholar
- Gurfinkel, A. and Chechik, M. 2003a. Generating counterexamples for multi-valued model-checking. In Proceedings of Formal Methods Europe (FME'03), Pisa, Italy.]]Google Scholar
- Gurfinkel, A. and Chechik, M. 2003b. Multi-valued model-checking via classical model-checking. In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), Marseille, France.]]Google Scholar
- Gurfinkel, A., Chechik, M., and Devereux, B. 2003. Temporal logic query checking: a tool for model exploration. IEEE Trans. Softw. Eng. 29, 10, pp. 898--914.]]Google ScholarDigital Library
- Hähnle, R. 1994. Automated Deduction in Multiple-Valued Logics, International Series of Monographs on Computer Science. vol. 10, Oxford University Press.]]Google Scholar
- Hazelhurst, S. 1996. Compositional Model Checking of Partially Ordered State Spaces. PhD Thesis, Department of Computer Science, University of British Columbia.]] Google ScholarDigital Library
- Hehner, E. 1993. A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer-Verlag, New York.]] Google ScholarDigital Library
- Huth, M., Jagadeesan, R., and Schmidt, D. 2003. A domain equation for refinement of partial systems. Math. Struct. Comput. Sci. Accepted for publication.]] Google ScholarDigital Library
- Huth, M., Jagadeesan, R., and Schmidt, D. A. 2001. Modal transition systems: a foundation for three-valued program analysis. In Proceedings of the 10th European Symposium on Programming (ESOP'01), Lecture Notes in Computer Science, vol. 2028, Springer, pp. 155--169.]] Google ScholarDigital Library
- Huth, M. and Pradhan, S. 2003. An ontology for consistent partial model checking. Elect. Notes Theoret. Comput. Sci., 23.]]Google Scholar
- Huth, M. and Ryan, M. 2000. Logic in Computer Science: Modeling and Reasoning About Systems. Cambridge University Press.]] Google ScholarDigital Library
- Kleene, S. C. 1952. Introduction to Metamathematics. Van Nostrand, New York.]]Google Scholar
- Konikowska, B. and Penczek, W. 2003. Model checking for multi-valued computation tree logics. In Beyond Two: Theory and Applications of Multiple Valued Logic, M. Fitting and E. Orlowska, eds., Physica-Verlag, pp. 193--210.]] Google ScholarDigital Library
- Kozen, D. 1983. Results on the propositional μ-calculus. Theoret. Comput. Sci., 27, pp. 334--354.]]Google ScholarCross Ref
- Larsen, K. and Thomsen, B. 1988. A modal process logic. In Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS'88), IEEE Computer Society Press, pp. 203--210.]]Google Scholar
- Lukasiewicz, J. 1970. Selected Works. North-Holland, Amsterdam, Holland.]]Google Scholar
- McMillan, K. 1993. Symbolic Model Checking. Kluwer Academic.]] Google ScholarDigital Library
- Michalski, R. S. 1977. Variable-valued logic and its applications to pattern recognition and machine learning. In Computer Science and Multiple-Valued Logic: Theory and Applications, D. C. Rine, eds., North-Holland, Amsterdam, pp. 506--534.]]Google Scholar
- Plath, M. and Ryan, M. 1999. SFI: a feature integration tool. In Tool Support for System Specification, Development and Verification, R. Berghammer and Y. Lakhnech, eds., Advances in Computer Science, Springer, pp. 201--216.]]Google Scholar
- Rasiowa, H. 1978. An Algebraic Approach to Non-Classical Logics. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland.]]Google Scholar
- Sagiv, M., Reps, T., and Wilhelm, R. 1999. Parametric shape analysis via 3-valued logic. In Proceedings of the 26th Annual ACM Symposium on Principles of Programming Languages. ACM, New York, NY, pp. 105--118.]] Google ScholarDigital Library
- Sasao, T. and Butler, J. 1996. A method to represent multiple-output switching functions using multi-valued decision diagrams. In Proceedings of IEEE International Symposium on Multiple-Valued Logic (ISMVL'96) (Santiago de Compostela, Spain). pp. 248--254.]] Google ScholarDigital Library
- Sofronie-Stokkermans, V. 2001. Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators. An Intern. J. Multip. Val. Log. 6, 3--4, pp. 289--344.]]Google Scholar
- Srinivasan, A., Kam, T., Malik, S., and Brayton, R. 1990. Algorithms for discrete function manipulation. In IEEE/ACM International Conference on Computer-Aided Design (ICCAD'90) (Santa Clara, CA). IEEE Computer Society, pp. 92--95.]]Google Scholar
Index Terms
- Multi-valued symbolic model-checking
Recommendations
Multi-valued model checking in dense-time
ECSQARU'05: Proceedings of the 8th European conference on Symbolic and Quantitative Approaches to Reasoning with UncertaintyIn this paper we introduce $\mathcal{X}$TCTL, a dense-time extension of the multi-valued Computation Tree Logic ($\mathcal{X}$CTL) in [1]. Alternatively, $\mathcal{X}$TCTL is a multi-valued extension of TCTL [2] over quasi-boolean algebras. A multi-...
On the limits of refinement-testing for model-checking CSP
AbstractRefinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates. By ...
Counter-example generation in symbolic abstract model-checking
The boundaries of model-checking have been extended through the use of abstraction. These techniques are conservative, in the following sense: when the verification succeeds, the verified property is guaranteed to hold; but when it fails, it may result ...
Comments