Quantitative Analysis of Lattice-valued Kripke Structures

• Autorzy: Pan H. , Zhang M. , Wu H. , Chen Y

Identyfikatory

DOI

10.3233/FI-2014-1122

• Języki publikacji: EN

Abstrakty

EN

To model and analyze systems with multi-valued information, in this paper, we present an extension of Kripke structures in the framework of complete residuted lattices, which we will refer to as lattice-valued Kripke structures (LKSs). We then show how the traditional trace containment and equivalence relations, can be lifted to the lattice-valued setting, and we introduce two families of lattice-valued versions of the relations. Further, we explore some interesting properties of these relations. Finally, we provide logical characterizations of our relations by a natural extension of linear temporal logic.

Słowa kluczowe

EN

Kripke structure; trace semantics; linear temporal logic; residuated lattice; Heyting algebra

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 135, nr 3
• Strony: 269--293
• Opis fizyczny: Bibliogr. 39 poz., tab.

Twórcy

autor

Pan H.

• College of Computer Science, Shaanxi Normal University, Xi’an 710062, China

autor

Zhang M.

• Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China

autor

Wu H.

• Information Engineer College, Hangzhou Dianzi University, 310018, Hangzhou, China

autor

Chen Y

• Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China

Bibliografia

• [1] Baier, C., Engelen, B., Majster-Cederbaum, M. E.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences, 60(1), 2000, 187–231.
• [2] Baier, C., Pieter, K. J.: Principles of Model Checking, MIT Press, 2008.
• [3] Bou, F., Estev, F., Godo, L., Rodriguez, R.O.: On the minimum many-valued modal logic over a finite residuated lattice. Journal of Logic and Computation, 21(5), 2011, 739–790.
• [4] Bĕlohlávek, R.: Fuzzy Relational Systems: Foundations and Principles, Kluwer, 2002.
• [5] Cĕrny, P., Henzinger, T. A., Radhakrishna, A.: Simulation distance. Theoretical Computer Science, 413, 2012, 21–35.
• [6] Chatterjee, K., Doyen, L., Henzinger, T. A.: Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science, 6(3), 2010.
• [7] Chechik, M., Gurfinkel, A., Devereux, B.,etc: Data structures for symbolic multi-valued model-checking. Formal Methods in System Design, 29(3), 2006, 295– 344.
• [8] Ćirić, M., Ignjatović, J., Damljanović, N., Bašić, M.: Bisimulations for fuzzy automata. Fuzzy Sets and Systems, 186, 2012, 100–139.
• [9] Clarke, E. M., Grumberg, O., Peled, D.: Model checking, MIT Press, 1999.
• [10] Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2), 1997, 253–291.
• [11] de Alfaro L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Transaction on Software Engineering, 35(2), 2009, 258–273.
• [12] Desharnais J., Gupta V., Jagadeesan R., Panangaden P.: Metrics for labelled markov processes. Theoretical Computer Science, 318(3), 2004, 323–354.
• [13] Droste, M., Kuich, W., Vogler, H.(Eds.): Handbook of Weighted Automata in: EATCS Monographs in Theoretical Computer Science, Springer-Verlag, 2009.
• [14] Droste, M., Vogler, H.: Weighted automata and multi-valued logics over arbitrary bounded lattices. Theoretical Computer Science,418, 2012, 14–36.
• [15] Esteva, F., Godo, L.: Monoidal t-norm-based logic: towards a logic for left-continuous t-norms. Fuzzy Sets and Systems, 124, 2001, 271–288.
• [16] Fitting, M. C.: Many-valued modal logics. Fundamenta Informaticae, 15, 1992, 235–254.
• [17] Fitting, M. C.: Many-valued modal logics, II. Fundamenta Informaticae, 17, 1992, 55–73.
• [18] Girard, A., Pappas, G. J.: Approximation metrics for discrete and continuous systems. IEEE Transactions on Automatic Control, 52(5), 2007, 782–798.
• [19] Hájek, P.: Metamathematics of Fuzzy Logic, Kluwer Academic Publishers, Dordrecht, 1998.
• [20] IEEE.: IEEE standard multivalue logic system for VHDL model interoperability (Std logic 1164), 1993.
• [21] Kehagias, A., Konstantinidou, M.: L-fuzzy valued inclusion measure, L-fuzzy similarity and L-fuzzy distance. Fuzzy Sets and Systems, 136, 2003, 313–332.
• [22] Klement, E.P., Pap, E.: Triangular norms. Kluwer Academic Publisher, Dordrecht, 2000.
• [23] Kupferman O., Lustig Y.: Lattice automata, in: Proceedings of VMCAI 2007, LNCS, 4349, 2007, 199–213.
• [24] Kupferman, O., Lustig, Y.: Latticed simulation relations and games. International Journal on the Foundations of Computer Science, 21(2), 2010, 167–189.
• [25] Kwiatkowska, M., Penczek, W.: On designated values in multi-valued CTL *model checking. Fundamenta Informaticae,60, 2004, 211–224.
• [26] Li, Y. M.: Approximation and robustness of fuzzy finite automata. International Journal of Approximate Reasoning, 47(2), 2008, 247–257.
• [27] Liu, H. W., Wang, G. J.: Continuity of triple I methods based on several implications. Computers and Mathematics with Applications, 56, 2008, 2079-2087.
• [28] Lluch-Lafuente, A., Montanari, U.: Quantitative μ-caclulus and CTL defined over constraint semirings. Theoretical Computer Science, 346, 2005, 135–160.
• [29] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
• [30] Milner, R.: Communication and concurrency. Prentice Hall, New York, 1989.
• [31] Pan, H.Y., Zhang, M., Chen, Y. X.: Lattice-Valued Kripke Structures Based on Complete Residuated Lattice. In: the proceeding of 2012 IEEE Sixth International Conference on Software Security and Reliability Companion(SERE2012), 2012, 137-143.
• [32] Pan, H.Y., Cao,Y. Z., Zhang, M., Chen, Y. X.: Simulation for lattice-valued doubly labeled transition systems. International Journal of Approximate Reasoning, 55, 2014, 797-811.
• [33] Pei, D.W.,Wang, G. J.: The completeness and applications of the formal system L* Science in China (Series F), 45(1),2002,40–50.
• [34] Qiu, D.: Automata theory based on complete residuated lattice-valued logic (I). Science in China ( Ser. F), 44(6) (2001) 419–429.
• [35] Qiu, D.: Automata theory based on complete residuated lattice-valued logic (II). Science in China ( Ser. F), 45(6) (2002) 442–452.
• [36] Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Transactions on Programming Languages and Systems,31(4), (2009) 111–151.
• [37] She, Y. H., Wang, G. J.: An axiomatic approach of fuzzy rough sets based on residuated lattices. Computers and Mathematics with Applications, 58, 2009, 189–201.
• [38] Thrane, C., Fahrenberg, U., Larsen, K. G.: Quantitative analysis of weighted transition systems. Journal of Logic and Algebraic Programming, 79(7), 2010, 689–703.
• [39] van Breugel, F., Worrell, J.: Approximating and computing behavioural distances in probabilistic transition systems. Theoretical Computer Science, 360(1-3), 2006, 373–385.