×

Model checking of linear-time properties in multi-valued systems. (English) Zbl 1428.68188

Summary: In this paper, we study the model-checking problem of linear-time properties in multi-valued systems. Safety properties, invariant properties, liveness properties, persistence and dual-persistence properties in multi-valued logic systems are introduced. Some algorithms related to the above multi-valued linear-time properties are discussed. The verification of multi-valued regular safety properties and multi-valued \(\omega\)-regular properties using lattice-valued automata are thoroughly studied. Since the law of non-contradiction (i.e., \(a \wedge \neg a = 0\)) and the law of excluded-middle (i.e., \(a \vee \neg a = 1\)) do not hold in multi-valued logic, the linear-time properties introduced in this paper have new forms compared to those in classical logic. Compared to those classical model-checking methods, our methods to multi-valued model checking are accordingly more direct: We give an algorithm for showing \(TS \models P\) for a model \(\mathit{TS}\) and a linear-time property \(P\), which proceeds by directly checking the inclusion \(\operatorname{Traces}(TS)\subseteq P\) instead of \(\operatorname{Traces}(\mathit{TS}) \cap \neg P = \emptyset\). A new form of multi-valued model checking with membership degree is also introduced. In particular, we show that multi-valued model checking can be reduced to classical model checking. The related verification algorithms are also presented. Some illustrative examples and a case study are also provided.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B50 Many-valued logic
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

SPIN
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alpern, B.; Schneider, F., Defining liveness, Inf. Process. Lett., 21, 181-185 (1985) · Zbl 0575.68030
[2] Baier, C.; Katoen, J. P., Principles of Model Checking (2008), MIT Press, Cambridge, Massacasetts · Zbl 1179.68076
[3] Birkhoff, G., Lattice theory (1973), Amer. Math. Soc., Providence: Amer. Math. Soc., Providence Rhode Island, USA · Zbl 0126.03801
[4] Bloc, L.; Borowik, P., Multi-Valued Logics (1992), Springer-Verlag: Springer-Verlag Berlin · Zbl 0791.03007
[5] Bruns, G.; Godefroid, P., Model checking partial state spaces with 3-valued temporal logics, Proceedings of the 11th International Conference on Computer-Aided Verification (CAV99), (Trento, Italy). Lecture Notes in Computer Science, volume 1633, 274-287 (1999), Springer · Zbl 1046.68583
[6] Bruns, G.; Godefroid, P., Generalized model checking: reasoning about partial state spaces, (Palamidessi, C., Proceedings of the 11th International Conference on Concurrency Theory (CONCUR00). Proceedings of the 11th International Conference on Concurrency Theory (CONCUR00), Lecture Notes in Computer Science, volume 1877 (2000), Springer), 168-182 · Zbl 0999.68524
[8] Chechik, M., On Interpreting Results of Model-Checking with Abstraction (2000), University of Toronto, Department of Computer Science, CSRG technical report 417
[9] Chechik, M.; Deverux, B.; Gurfinkel, A., Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Proceedings of the 8th SPIN Workshop on Model Checking Software, Toronto, Canada. Proceedings of the 8th SPIN Workshop on Model Checking Software, Toronto, Canada, Lecture Notes in Computer Science, volume 2057, 16-36 (2001), Springer · Zbl 0985.68031
[10] Chechik, M.; Devereux, B.; Gurfinkel, A.; Easterbrook, S., Multi-valued symbolic model-checking, ACM Trans. Softw. Eng. Methodol., 12, 4, 371-408 (2003)
[11] Ciric, M.; Droste, M.; Ignjatovic, J.; Vogler, H., Determinization of weighted finite automata over strong bimonoids, Inf. Sci., 180, 18, 3497-3520 (2010) · Zbl 1205.68198
[12] Chechik, M.; Easterbrook, S.; Petrovykh, V., Model-checking over multi-valued logics, Proceedings of Formal Methods Europe (FME01). Proceedings of Formal Methods Europe (FME01), Lecture Notes in Computer Science, 2021, 72-98 (2001), Springer Verlag, Berlin · Zbl 0977.68704
[13] Chechik, M.; Gurfinkel, A.; Devereux, B.; Lai, A.; Easterbrook, S., Data structures for symbolic multi-valued model-checking, Formal Methods Syst. Des., 29, 295-344 (2006) · Zbl 1109.68063
[14] Demri, S.; DSouza, D., An automata-theoretic approach to constraint LTL, Inf. Comput., 205, 3, 380-415 (2007) · Zbl 1113.03015
[15] Droste, M.; Kuich, W.; Rahonis, G., Multi valued MSO logics over words and trees, Fundam. Inform., 84, 305-327 (2008) · Zbl 1157.03016
[17] Droste, M.; Meinecke, I., Weighted automata and weighted MSO logics for average and long-time behaviors, Inf. Comput., 220-221, 44-59 (2012) · Zbl 1279.68148
[18] Droste, M.; Vogler, H., Weighted automata and multi-valued logics over arbitrary bounded lattices, Theor. Comput. Sci., 418, 14-36 (2012) · Zbl 1245.03060
[19] Eilenberg, S., Automata, Languages and Machines, Vol. a, Vol B (1974), Academic Press, New York · Zbl 0317.94045
[20] Fitting, M., Many-valued modal logics, Fundam. Inform., 15, 3-4, 335-350 (1991)
[21] Godefroid, P.; Jagadeesan, R., On the expressiveness of 3-valuedmodels, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI03). Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI03), Lecture Notes in Computer Science, 2575, 206-222 (2003), Springer · Zbl 1022.68075
[22] Grätzer, G., General Lattice Theory (2003), Birkhäuser-Verlag, Basel · Zbl 0385.06015
[23] Hájek, P., Metamathematics of Fuzzy Logic (1998), Kluwer Academic Publisher, Dordrecht · Zbl 0937.03030
[24] Hazelhurst, S., Compositional Model Checking of Partially Ordered State Spaces (1996), Department of Computer Science, University of British Columbia, Phd thesis
[25] Holzmann, G., The model checker SPIN, IEEE Trans. Softw. Eng., 23, 5, 279-295 (1997)
[26] Hopcroft, J. E.; Ullman, J. D., Introduction to Automata Theory, Languages and Computation (1979), Addison-Wesley, New York · Zbl 0426.68001
[27] Howard, J. H.; Kazar, M. L.; Nochols, S. G.; Nochols, D. A.; Satyanarayanan, M.; Sidebotham, R. N.; West, M. J., Scale and performance in a distributed file system, ACM Trans. Comput. Syst., 6, 1, 51-81 (1988)
[28] Huth, M.; Jagadeesan, R.; Schmidt, D. A., Modal transition systems: a foundation for three-valued program analysis, Proceedings of the 10th European Symposium on Programming (ESOP01). Proceedings of the 10th European Symposium on Programming (ESOP01), Lecture Notes in Computer Science, 2028, 155-169 (2001), Springer · Zbl 0987.68849
[29] Khoussainov, B.; Nerode, A., Automata Theory and Its Applications (2001), Birkäuser, Boston · Zbl 1083.68058
[30] Kuich, W.; Rahonis, G., Fuzzy regular languages over finite and infinite words, Fuzzy Sets Syst., 157, 1532-1549 (2006) · Zbl 1092.68053
[31] Kuich, W.; Salomaa, A., Semirings, Automata, Languages, EATCS Monographs on Theoretical Computer Science, 5 (1986), Springer-Verlag, Berlin/Heidelberg/New York/Tokyo · Zbl 0582.68002
[32] Kupferman, O.; Lustig, Y., Lattice automata, Proceedings of VWCAI2007. Proceedings of VWCAI2007, Lecture Notes in Computer Science, 4349, 199-213 (2007), Springer · Zbl 1132.68455
[33] Kupferman, O.; Vardi, M. Y., Model checking of safety properties, Formal Methods Syst. Des., 19, 291-314 (2001) · Zbl 0995.68061
[34] Lamport, L., Proving the correctness of multiprocess programs, IEEE Trans. Softw. Eng., 3, 125-143 (1977) · Zbl 0349.68006
[35] Li, Y. M.; Li, Z. H., Free semilattices and strongly free semilattices generated by partially ordered sets, Northeastern Math. J., 9, 3, 359-366 (1993) · Zbl 0805.06004
[36] Li, Y. M.; Pedrycz, W., Fuzzy finite automata and fuzzy regular expressions with membership values in lattice-ordered monoids, Fuzzy Sets Syst., 156, 68-92 (2005) · Zbl 1083.68059
[37] Li, Y. M.; Pedrycz, W., Minimization of lattice finite automata and its application to the decomposition of lattice languages, Fuzzy Sets Syst., 158, 1423-1436 (2007) · Zbl 1123.68063
[38] Li, Y. M., Finite automata theory with membership values in lattices, Inf. Sci., 181, 1003-1017 (2011) · Zbl 1209.68302
[39] Li, Y. M.; Li, L. J., Model checking of linear-time properties based on possibility measure, IEEE Trans. Fuzzy Syst., 21, 5, 842-854 (2013)
[40] Li, Y.; Li, Y.; Ma, Z., Computation tree logic model checking based on possibility measures, Fuzzy Sets Syst., 262, 44-59 (2015) · Zbl 1361.68148
[41] Li, Y.; Ma, Z., Quantitative computation tree logic model checking based on generalized possibility measures, IEEE Trans. Fuzzy Syst., 23, 6, 2034-2047 (2015)
[43] Manna, Z.; Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems: Safety (1995), Springer, Berlin
[44] McMillan, K., Symbolic Model Checking (1993), Kluwer, Academic · Zbl 1132.68474
[45] Rozier, K. Y., Linear temporal logic symbolic model checking, Comput. Sci. Rev., 5, 2, 163-203 (2011) · Zbl 1298.68176
[46] Shoham, S.; Grumberg, O., Compositional verification and 3-valued abstractions join forces, Inf. Comput., 208, 2, 178-202 (2010) · Zbl 1191.68416
[47] Vardi, M. Y.; Wolper, P., Reasoning about infinite computations, Inf. Comput., 115, 1-37 (1994) · Zbl 0827.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.