{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:56:32Z","timestamp":1721894192823},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2003,10]]},"abstract":"\n This article introduces the concept of multi-valued model-checking and describes a multi-valued symbolic model-checker, \u03a7Chek. Multi-valued model-checking is a generalization of classical model-checking, useful for analyzing models that contain\n uncertainty<\/jats:italic>\n (lack of essential information) or\n inconsistency<\/jats:italic>\n (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 \u03a7CTL, 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 \u03a7CTL and CTL, and provide a symbolic model-checking algorithm for \u03a7CTL. We also address the use of fairness in multi-valued model-checking. Finally, we discuss some applications of the multi-valued model-checking approach.\n <\/jats:p>","DOI":"10.1145\/990010.990011","type":"journal-article","created":{"date-parts":[[2004,7,20]],"date-time":"2004-07-20T16:39:33Z","timestamp":1090341573000},"page":"371-408","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":131,"title":["Multi-valued symbolic model-checking"],"prefix":"10.1145","volume":"12","author":[{"given":"Marsha","family":"Chechik","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"given":"Benet","family":"Devereux","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"given":"Steve","family":"Easterbrook","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]}],"member":"320","published-online":{"date-parts":[[2003,10]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Anderson A. and Belnap N. 1975. Entailment. Vol. 1. Princeton University Press.]] Anderson A. and Belnap N. 1975. Entailment. Vol. 1. Princeton University Press.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/551462"},{"key":"e_1_2_1_3_1","first-page":"188","volume-title":"IEEE \/ACM International Conference on Computer-Aided Disign (ICCAD'93)","author":"Bahar R.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_4_1","first-page":"27","volume-title":"Proceedings of the 5th Workshop on Logic, Language, Information and Computation, (WoLLIC'98)","author":"Baier C.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Baier C. Clarke E. M. Hartonas-Garmhausen V. Kwiatkowska M. Z. and \n Ryan M\n . \n 1997\n . 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. \n 1256 Springer pp. \n 430\n --\n 440\n .]] 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.]]","DOI":"10.1007\/3-540-63165-8_199"},{"key":"e_1_2_1_6_1","first-page":"30","volume-title":"Reidel","author":"Belnap N.","year":"1977","unstructured":"Belnap , N. 1977 . A useful four-valued logic. In Modern Uses of Multiple-Valued Logic, Donn and Epstein, eds ., Reidel , pp. 30 -- 56 .]] Belnap, N. 1977. A useful four-valued logic. In Modern Uses of Multiple-Valued Logic, Donn and Epstein, eds., Reidel, pp. 30--56.]]"},{"key":"e_1_2_1_7_1","series-title":"IEE Control Engineering Series 2","volume-title":"Elevator Analysis, Design and Control","author":"Berney G.","unstructured":"Berney , G. and dos Santos , S. 1985. Elevator Analysis, Design and Control . IEE Control Engineering Series 2 . Peter Peregrinus Ltd .]] Berney, G. and dos Santos, S. 1985. Elevator Analysis, Design and Control. IEE Control Engineering Series 2. Peter Peregrinus Ltd.]]"},{"key":"e_1_2_1_8_1","volume-title":"Lattice Theory","author":"Birkhoff G.","unstructured":"Birkhoff , G. 1967. Lattice Theory ( 3 rd Edition). Americal Mathematical Society , Providence, RI .]] Birkhoff, G. 1967. Lattice Theory (3rd Edition). Americal Mathematical Society, Providence, RI.]]","edition":"3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Bolc L. and Borowik P. 1992. Many-Valued Logics. Springer-Verlag.]] Bolc L. and Borowik P. 1992. Many-Valued Logics. Springer-Verlag.]]","DOI":"10.1007\/978-3-662-08494-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Proceedings of the 11th International Conference on Computer-Aided Verification (CAV'99)","volume":"1633","author":"Bruns G.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Bruns G.\n and \n Godefroid P\n . \n 2000\n . 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. \n 1877 Springer pp. \n 168\n --\n 182\n .]] 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.]]","DOI":"10.1007\/3-540-44618-4_14"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733946"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Chechik M. Devereux B. and \n Easterbrook S\n . \n 2001\n a. 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. \n 2031 Springer pp. \n 404\n --\n 419\n .]] 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.]]","DOI":"10.1007\/3-540-45319-9_28"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/3-540-45139-0_3","volume-title":"Proceedings of the 8th SPIN Workshop on Model Checking Software","volume":"2057","author":"Chechik M.","unstructured":"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 ,]] 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,]]"},{"key":"e_1_2_1_15_1","first-page":"505","volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification (CAV'02)","author":"Chechik M.","unstructured":"Chechik , M. , Devereux , B. , and Gurfinkel , A . 2002a. \u03a7Chek: 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 .]] Chechik, M., Devereux, B., and Gurfinkel, A. 2002a. \u03a7Chek: 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.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020883625495"},{"key":"e_1_2_1_17_1","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/850983.855328"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_20_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.]] Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"e_1_2_1_24_1","unstructured":"Davey B. and Priestley H. 1990. Introduction to Lattices and Order. Cambridge University Press.]] Davey B. and Priestley H. 1990. Introduction to Lattices and Order. Cambridge University Press.]]"},{"key":"e_1_2_1_25_1","first-page":"40","volume-title":"Proceedings of FLOC'02 Workshop on Fixpoints in Computer Science (FICS)","author":"Devereux B.","year":"2002","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_26_1","volume-title":"What is Negation","author":"Dunn J.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_27_1","first-page":"411","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE'01)","author":"Easterbrook S.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_28_1","first-page":"3","article-title":"Many-valued modal logics","volume":"15","author":"Fitting M.","year":"1991","unstructured":"Fitting , M. 1991 a. Many-valued modal logics . Fund. Info. , 15 , 3 -- 4 , pp. 335--350.]] Fitting, M. 1991a. Many-valued modal logics. Fund. Info., 15, 3--4, pp. 335--350.]]","journal-title":"Fund. Info."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.6.797"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/167892.167899"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-7373(79)80039-5"},{"key":"e_1_2_1_32_1","first-page":"251","volume-title":"Readings in Nonmonotonic Reasoning","author":"Ginsberg M.","unstructured":"Ginsberg , M. 1987. Multi-valued logic . In Readings in Nonmonotonic Reasoning , M. Ginsberg, ed., Morgan-Kaufmann Publishing , pp. 251 -- 255 .]] Ginsberg, M. 1987. Multi-valued logic. In Readings in Nonmonotonic Reasoning, M. Ginsberg, ed., Morgan-Kaufmann Publishing, pp. 251--255.]]"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1988.tb00280.x"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Godefroid P. Huth M. and \n Jagadeesan R\n . \n 2001\n . 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. \n 2154 Springer pp. \n 426\n --\n 440\n .]] 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.]]","DOI":"10.1007\/3-540-44685-0_29"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Godefroid P.\n and \n Jagadeesan R\n . \n 2003\n . 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. \n 2575 Springer pp. \n 206\n --\n 222\n .]] 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.]]","DOI":"10.1007\/3-540-36384-X_18"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-247X(67)90189-8"},{"key":"e_1_2_1_37_1","volume-title":"Department of Computer Science","author":"Gurfinkel A.","unstructured":"Gurfinkel , A. 2002. Multi-valued symbolic model-checking: fairness, counter-examples, running time. Master's Thesis , Department of Computer Science , University of Toronto .]] Gurfinkel, A. 2002. Multi-valued symbolic model-checking: fairness, counter-examples, running time. Master's Thesis, Department of Computer Science, University of Toronto.]]"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of Formal Methods Europe (FME'03)","author":"Gurfinkel A.","unstructured":"Gurfinkel , A. and Chechik , M . 2003a. Generating counterexamples for multi-valued model-checking . In Proceedings of Formal Methods Europe (FME'03) , Pisa, Italy.]] Gurfinkel, A. and Chechik, M. 2003a. Generating counterexamples for multi-valued model-checking. In Proceedings of Formal Methods Europe (FME'03), Pisa, Italy.]]"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03)","author":"Gurfinkel A.","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1237171"},{"key":"e_1_2_1_41_1","series-title":"International Series of Monographs on Computer Science","volume-title":"Automated Deduction in Multiple-Valued Logics","author":"H\u00e4hnle R.","unstructured":"H\u00e4hnle , R. 1994. Automated Deduction in Multiple-Valued Logics , International Series of Monographs on Computer Science . vol. 10 , Oxford University Press .]] H\u00e4hnle, R. 1994. Automated Deduction in Multiple-Valued Logics, International Series of Monographs on Computer Science. vol. 10, Oxford University Press.]]"},{"key":"e_1_2_1_43_1","volume-title":"A Practical Theory of Programming. Texts and Monographs in Computer Science","author":"Hehner E.","unstructured":"Hehner , E. 1993. A Practical Theory of Programming. Texts and Monographs in Computer Science . Springer-Verlag , New York .]] Hehner, E. 1993. A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004268"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Huth M. Jagadeesan R. and \n Schmidt D. A\n . \n 2001\n . 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. \n 2028 Springer pp. \n 155\n --\n 169\n .]] 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.]]","DOI":"10.1007\/3-540-45309-1_11"},{"key":"e_1_2_1_46_1","unstructured":"Huth M. and Pradhan S. 2003. An ontology for consistent partial model checking. Elect. Notes Theoret. Comput. Sci. 23.]] Huth M. and Pradhan S. 2003. An ontology for consistent partial model checking. Elect. Notes Theoret. Comput. Sci. 23.]]"},{"key":"e_1_2_1_47_1","volume-title":"Computer Science: Modeling and Reasoning About Systems","author":"Huth M.","year":"2000","unstructured":"Huth , M. and Ryan , M . 2000 . Logic in Computer Science: Modeling and Reasoning About Systems . Cambridge University Press .]] Huth, M. and Ryan, M. 2000. Logic in Computer Science: Modeling and Reasoning About Systems. Cambridge University Press.]]"},{"key":"e_1_2_1_48_1","volume-title":"Introduction to Metamathematics","author":"Kleene S. C.","unstructured":"Kleene , S. C. 1952. Introduction to Metamathematics . Van Nostrand , New York .]] Kleene, S. C. 1952. Introduction to Metamathematics. Van Nostrand, New York.]]"},{"key":"e_1_2_1_49_1","first-page":"193","volume-title":"Physica-Verlag","author":"Konikowska B.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_51_1","first-page":"203","volume-title":"Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS'88)","author":"Larsen K.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_52_1","unstructured":"Lukasiewicz J. 1970. Selected Works. North-Holland Amsterdam Holland.]] Lukasiewicz J. 1970. Selected Works. North-Holland Amsterdam Holland.]]"},{"key":"e_1_2_1_53_1","volume-title":"Symbolic Model Checking","author":"McMillan K.","unstructured":"McMillan , K. 1993. Symbolic Model Checking . Kluwer Academic .]] McMillan, K. 1993. Symbolic Model Checking. Kluwer Academic.]]"},{"key":"e_1_2_1_54_1","first-page":"506","volume-title":"North-Holland","author":"Michalski R. S.","year":"1977","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_55_1","first-page":"201","volume-title":"Advances in Computer Science","author":"Plath M.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_56_1","volume-title":"An Algebraic Approach to Non-Classical Logics. Studies in Logic and the Foundations of Mathematics","author":"Rasiowa H.","unstructured":"Rasiowa , H. 1978. An Algebraic Approach to Non-Classical Logics. Studies in Logic and the Foundations of Mathematics . Amsterdam : North-Holland .]] Rasiowa, H. 1978. An Algebraic Approach to Non-Classical Logics. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland.]]"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_2_1_58_1","first-page":"248","volume-title":"Proceedings of IEEE International Symposium on Multiple-Valued Logic (ISMVL'96)","author":"Sasao T.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_59_1","first-page":"3","article-title":"Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators","volume":"6","author":"Sofronie-Stokkermans V.","year":"2001","unstructured":"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.]] 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.]]","journal-title":"An Intern. J. Multip. Val. Log."},{"key":"e_1_2_1_60_1","first-page":"92","volume-title":"IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'90)","author":"Srinivasan A.","unstructured":"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 .]] 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.]]"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/990010.990011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T11:20:33Z","timestamp":1672744833000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/990010.990011"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10]]},"references-count":58,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003,10]]}},"alternative-id":["10.1145\/990010.990011"],"URL":"https:\/\/doi.org\/10.1145\/990010.990011","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,10]]},"assertion":[{"value":"2003-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
