By considering the multi-valued bisimulation quotients, smaller multi-valued models are obtained. This minimization can be exploited for efficient multi-valued model checking. In this paper, we illustrate an application of the multi-valued bisimulation quotients. Further, we present some definitions of partitions of multi-valued Kripke structures. Finally, as the main contribution, in order to generate the multi-valued bisimulation quotient, we provide a series of algorithms and analysis the time complexity of it.
PeledD., ClarkeE., GrumbergO., Model checking, The MIT Press, 1999.
2.
PanH., ZhangM., WuH. and ChenY., Quantitative analysis of lattice-valued kripke structures, Fundamenta Informaticae135 (2014), 269–293.
3.
PanH., ZhangM. and ChenY., Bisimulation For Latticevalued Transition Systems, 2012 IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering.
4.
CaoY.Z., ChenG.Q. and KerreE., Bisimulations for Fuzzy-Transition Systems, IEEE Transactions on Fuzzy Systems19(3) (2011), 540–552.
5.
WuH.Y. and DengY.X., Logical characterizations of simulation and bisimulation for fuzzy transition systems, Fuzzy Sets and Systems301(6) (2016), 19–36.
6.
BelohlavekR., Fuzzy Relational Systems, Foundations and Principles, Kluwer, 2012.
7.
JonnsonB. and TarskiA., Boolean algebras with operators, American Journal of Mathematics74(1) (1952), 127–116.
8.
QiuD.W., Automata theory based on complete residuated latticeąłvalued logic(I) and (II), Sci China, Ser F44 (2001), 419–429; Sci China, Ser F 45 (2002), 442–452.
9.
KroupaT., States in Lukasiewicz logic correspond to probabilities of rational polyhedra, Int J Approx Reason5 (2012), 435–446.
10.
LiY.M., DrosteM. and LeiL.H., Model checking of lineartime properties in multi-valued systems, Information Sciences377 (2017), 51–74.
11.
LiY., LiY. and MaZ., Computation tree logic model checking based on possibility measures, Fuzzy Sets Syst262 (2015), 44–59.
12.
LiY. and MaZ., Quantitative computation tree logic model checking based on generalized possibility measures, IEEE Trans Fuzzy Syst23(6) (2015), 2034–2047.
13.
FengY., YuN.K. and YingM.S., Model checking quantum Markov chains, Journal of Computer and System Sciences79 (2013), 1181–1198.
14.
LiY.M. and LiL.J., Model checking of linear-time properties based on possibility measure, IEEE Trans Fuzzy Syst21(5) (2013), 842–854.
15.
BaierC., KatoenJ.P., Principles of model checking, The MIT Press, 2007.
16.
HartS. and SharirM., Probabilistic propositional temporal logics, Information and Control (1986), 97–155.
ChechikM., EasterbrookS., PetrovykhV., Model-checking over multi-valued logics, Lecture Notes in Computer Science, 2021, Springer Verlag, Berlin, 2001, pp. 72–98
.
19.
ChechikM., DevereuxB., GurfinkelA. and EasterbrookS., Multivalued symbolic model-checking, on Software Engineering and Methodology12(4) (2003), 371–408.
20.
ChechikM., DeveruxB. and GurfinkelA., Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Proceedings of the 8th SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, Toronto, Canada, vol. 2057, Springer, 2001, pp. 16–36.
21.
PaigefR. and TarjantR., Three partition refinement algorithms, Society for Industrial and Applied Mathematics16(6) (1987), 973–989.
