Abstract
Classical model checking is not capable of solving the situation of uncertain systems or fault-tolerant systems which occur in the real world commonly. The technique of satisfiability degree (SD) for model checking is a efficient way to solve this problem. Finite paths transition system (FPTS) for calculating satisfiability degree of a LTL logic formula is given. Then, a more general situation about discrete-time Markov chains (DTMCs) is discussed. Then a case named leader election shows the practicability of satisfiability degree for transition system, which cannot be solved by classical model checking.
This work is supported by the Funds NSFC 60973049 and 60635020.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Luo, G.M., Yin, C.Y., Hu, P.: An algorithm for calculating the satisfiability degree. In: Proceedings of the 2009 Sixth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD 2009), vol. 7, pp. 322–326 (2009)
Yin, C.Y., Luo, G.M., Hu, P.: Backtracking search algorithm for satisfiability degree calculation. In: Proceedings of the 2009 Sixth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD 2009), vol. 2, pp. 3–7 (2009)
Hu, P., Luo, G.M., Yin, C.Y.: Computation of satisfiability degree based on CNF. In: Proceedings of the 2009 Sixth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD 2009), vol. 6, pp. 142–146 (2009)
Clarke, E.M., Orna, G., Peled, D.A.: Model Checking, pp. 13–24. The MIT Press, Cambridge (1999)
Huth, M.l., Ryan, M.: Logic in Computer Science Modeling and Reasoning about Systems, 2nd edn., pp. 172–186 (2005)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Intruduction to algorithm, 2nd edn., pp. 540–549 (2002)
Itai, A., Rodeh, M.: Symmetry Breaking in Distributed Networks. Information and Computation 88(1), 60–87 (1990)
Hong, I., Sohn, S.H., Lee, J.K., et al.: DFS algorithm with ranking based on genetic algorithm in UHF portable system. In: 2009 9th International Symposium on Communications and Information Technology, ISCIT 2009, pp. 454–459 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, Y., Luo, G. (2010). Satisfiability Degree Analysis for Transition System. In: Wang, F.L., Deng, H., Gao, Y., Lei, J. (eds) Artificial Intelligence and Computational Intelligence. AICI 2010. Lecture Notes in Computer Science(), vol 6319. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16530-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16530-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16529-0
Online ISBN: 978-3-642-16530-6
eBook Packages: Computer ScienceComputer Science (R0)