×

Simulation for lattice-valued doubly labeled transition systems. (English) Zbl 1316.68063

Summary: During the last decades, a large amount of multi-valued transition systems, whose transitions or states are labeled with specific weights, have been proposed to analyze quantitative behaviors of reactive systems. To set up a unified framework to model and analyze systems with quantitative information, in this paper, we present an extension of doubly labeled transition systems in the framework of residuated lattices, which we will refer to as lattice-valued doubly labeled transition systems (LDLTSs). Our model can be specialized to fuzzy automata over complete residuated lattices, fuzzy transition systems, and multi-valued Kripke structures. In contrast to the traditional yes/no approach to similarity, we then introduce lattice-valued similarity between LDLTSs to measure the degree of closeness of two systems, which is a value from a residuated lattice. Further, we explore the properties of robustness and compositionality of the lattice-valued similarity. Finally, we extend the Hennessy-Milner logic to the residuate lattice-valued setting and show that the obtained logic is adequate and expressive with lattice-valued similarity.

MSC:

68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

MAGIC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, L.; Ingólfsdóttir, A.; Larsen, K. G.; Srba, J., Reactive Systems: Modelling, Specification and Verification (2007), Cambridge University Press · Zbl 1141.68043
[2] de Alfaro, L.; Faella, M.; Henzinger, T., Model checking discounted temporal properties, Theor. Comput. Sci., 345, 1, 139-170 (2005) · Zbl 1079.68062
[3] Baier, C.; Katoen, J. P., Principles of Model Checking (2008), MIT Press
[4] ter Beek, M. H.; Fantechi, A.; Gnesi, S.; Mazzanti, F., A state/event-based model-checking approach for the analysis of abstract system properties, Sci. Comput. Program., 76, 2, 119-135 (2011) · Zbl 1213.68392
[5] Bělohlávek, R., Fuzzy Relational Systems: Foundations and Principles (2002), Kluwer · Zbl 1067.03059
[6] Bou, F.; Esteva, F.; Godo, L., On the minimum many-valued modal logic over a finite residuated lattice, J. Log. Comput., 21, 5, 739-790 (2011) · Zbl 1252.03040
[7] Cao, Y. Z.; Chen, G. Q.; Kerre, E., Bisimulations for fuzzy-transition systems, IEEE Trans. Fuzzy Syst., 19, 3, 540-552 (2011)
[8] Cao, Y. Z.; Ying, M. S., Observability and decentralized control of fuzzy discrete-event systems, IEEE Trans. Fuzzy Syst., 14, 2, 202-216 (2006)
[9] Chaki, S.; Clarke, E. M.; Ouaknine, J., Concurrent software verification with states, events, and deadlocks, Form. Asp. Comput., 17, 461-483 (2005) · Zbl 1103.68609
[10] Chechik, M.; Gurfinkel, A.; Devereaux, B., Data structures for symbolic multi-valued model-checking, Form. Methods Syst. Des., 29, 3, 295-344 (2006) · Zbl 1109.68063
[11] Ćirić, M.; Ignjatović, J.; Damljanović, N., Bisimulations for fuzzy automata, Fuzzy Sets Syst., 186, 100-139 (2012) · Zbl 1237.68113
[12] Ćirić, M.; Ignjatović, J.; Jancic, I., Computation of the greatest simulations and bisimulations between fuzzy automata, Fuzzy Sets Syst., 208, 22-42 (2012) · Zbl 1252.68168
[13] Clarke, E. M.; Grumberg, O.; Peled, D., Model Checking (1999), MIT Press
[14] Dai, S. S.; Pei, D. W.; Guo, D. H., Robustness analysis of full implication inference method, Int. J. Approx. Reason., 54, 653-666 (2013) · Zbl 1316.68175
[15] Esteva, F.; Godo, L., Monoidal t-norm based logic: towards a logic for left-continuous t-norms, Fuzzy Sets Syst., 124, 271-288 (2001) · Zbl 0994.03017
[16] Fantechi, A.; Lapadula, A.; Mazzanti, F., A logical verification methodology for service-oriented computing, ACM Trans. Softw. Eng. Methodol., 21, 3 (2012)
[17] Flaminio, T.; Godo, L.; Marchioni, E., Logics for belief functions on MV-algebras, Int. J. Approx. Reason., 54, 491-512 (2013) · Zbl 1264.03049
[18] Fitting, M., Many-valued modal logics (I) and (II), Fundam. Inform.. Fundam. Inform., Fundam. Inform., 17, 55-73 (1992) · Zbl 0772.03006
[19] Hájek, P., Metamathematics of Fuzzy Logics (1998), Kluwer Academic Publishers: Kluwer Academic Publishers Boston · Zbl 0937.03030
[20] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021
[21] Julius, A. A.; D’Innocenzo, A.; DiBenedetto, M. D., Approximate equivalence and synchronization of metric transition systems, Syst. Control Lett., 58, 94-101 (2009) · Zbl 1155.93336
[22] Kroupa, T., States in Łukasiewicz logic correspond to probabilities of rational polyhedra, Int. J. Approx. Reason., 53, 435-446 (2012) · Zbl 1260.03050
[23] Kupferman, O.; Lustig, Y., Lattice automata, (Proceedings of VWCAI2007. Proceedings of VWCAI2007, Lect. Notes Comput. Sci., vol. 4349 (2007)), 199-213 · Zbl 1132.68455
[24] Kupferman, O.; Lustig, Y., Latticed simulation relations and games, Int. J. Found. Comput. Sci., 21, 2, 167-189 (2010) · Zbl 1200.68155
[25] Larsen, K. G.; Fahrenberg, U.; Thrane, C. R., Metrics for weighted transition systems: axiomatization and complexity, Theor. Comput. Sci., 412, 3358-3369 (2011) · Zbl 1216.68191
[26] Li, Y. M.; Li, D. C.; Pedrycz, W., An approach to measure the robustness of fuzzy reasoning, Int. J. Intell. Syst., 20, 4, 393-413 (2005) · Zbl 1101.68880
[27] Li, Y. M., Approximation and robustness of fuzzy finite automata, Int. J. Approx. Reason., 47, 247-257 (2008) · Zbl 1184.68319
[28] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall New York · Zbl 0683.68008
[29] Nicola, R. D.; Vaandrager, F. W., Three logics for branching bisimulation, J. ACM, 42, 2, 458-487 (1995) · Zbl 0886.68064
[30] Pei, D. W., Formalization of implication based fuzzy reasoning method, Int. J. Approx. Reason., 53, 837-846 (2012) · Zbl 1246.03049
[31] Pei, D. W.; Yang, R., Hierarchical structure and applications of fuzzy logical systems, Int. J. Approx. Reason., 54, 1483-1495 (2013) · Zbl 1316.03013
[32] Pei, D. W.; Wang, G. J., The completeness and application of the formal system \(L^\ast \), Sci. China, Ser. F, 45, 1, 40-50 (2002) · Zbl 1182.03053
[33] Qiu, D. W., Automata theory based on completed residuated lattice-valued logic (I) and (II), Sci. China, Ser. F. Sci. China, Ser. F, Sci. China, Ser. F, 45, 442-452 (2002) · Zbl 1161.68549
[34] Qiu, D. W., Pumping lemma in automata theory based on complete residuated lattice-valued logic: A note, Fuzzy Sets Syst., 157, 2128-2138 (2006) · Zbl 1121.03048
[35] Qiu, D. W., A note on Trilla’s CHC models, Artif. Intell., 171, 239-254 (2007) · Zbl 1168.06302
[36] Shoham, S.; Grumberg, O., Multi-valued model checking games, J. Comput. Syst. Sci., 78, 414-429 (2012) · Zbl 1257.68105
[37] Thrane, C. R.; Fahrenberg, U.; Larsen, K. G., Quantitative analysis of weighted transition systems, J. Log. Algebr. Program., 79, 7, 689-703 (2010) · Zbl 1204.68137
[38] Wu, L. H.; Qiu, D. W., Automata theory based on complete residuated lattice-valued logic: Reduction and minimization, Fuzzy Sets Syst., 161, 12, 1635-1656 (2010) · Zbl 1192.68426
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.