Abstract
In this paper we continue the study of a strict extension of the Computation Tree Logic, called graded-CTL, recently introduced by the same authors. This new logic augments the standard quantifiers with graded modalities, being able thus to express “There exist at least k” or “For all but k” futures, for some constant k. One can thus describe properties useful in system design, which cannot be expressed with CTL, like a sort of redundant liveness property asking whether there is more than one path satisfying that “something good eventually happens”, making thus the system more tolerant to possible faults. Graded-CTL formulas can also be used to determine whether there are more than a given number of bad behaviors of a system: this, in the model-checking framework, means that one can verify the existence of a user-defined number of counterexamples for a given specification and generate them, in a unique run of the model-checker.
Here we show both theoretical and applicative contributions. On the theoretical side we give a simple algorithm to decide this logic, and we prove that the satisfiability problem is ExpTime-complete when the constants of the quantifiers are represented in unary. On the applicative side we propose symbolic algorithms to solve the model checking problem. One of the main characteristics of these algorithms is that, though the computation of “distinct” counterexamples has inherently high complexity when the model is represented symbolically, we have designed them to make the generation of multiple counterexamples as easy and quick as possible. The symbolic algorithms have been implemented using BDD data structures, and have been integrated into the well known NuSMV model checker, that has been modified to accept specifications expressed in graded-CTL. The test results we report are very comfortable in the sense that both the running time and the size of the BDDs produced are comparable to those obtained with specifications expressed in classical CTL.
Work partially supported by M.I.U.R. grant ex-60%:“Metodi formali per la verifica automatica di sistemi” and by the National Research Project (PRIN’07) “Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems”.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), pp. 428–439. IEEE Computer Society Press, Los Alamitos (1990)
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Formal Methods in System Design 10(2/3), 171–206 (1997)
Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. Formal Methods in System Design 28(1), 37–56 (2006)
Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. In: LICS 2009 (2009)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Corradini, F., De Nicola, R., Labella, A.: Models of nondeterministic regular expressions. J. Comput. Syst. Sci. 59(3), 412–449 (1999)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Emerson, E.A.: Usig branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266 (1982)
Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. International Journal on Software Tools for Technololy Transfer 9(5), 429–445 (2007)
Copty, F., Irron, A., Weissberg, O., Kropp, N.P., Kamhi, G.: Efficient debugging in a formal verification environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 275–292. Springer, Heidelberg (2001)
Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Workshop on Model Based Development: Features, Components and Architectures (ECBS 2003), pp. 214–223 (2003)
Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Systems 4(4), 331–352 (1992)
Fine, K.: In so many possible worlds. Notre Dame Journal of Formal Logic 13(4), 516–520 (1972)
Ferrante, A., Napoli, M., Parente, M.: CTL model-checking with graded quantifiers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 18–32. Springer, Heidelberg (2008)
Ferrante, A., Napoli, M., Parente, M.: Model checking for graded CTL. Fundamenta Informaticae (to appear, 2010); Journal version of [FNP 2008]
Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. Information and Computation 150(2), 132–152 (1999)
Ganzinger, H., Meyer, C., Veanes, M.: The two–variable guarded fragment with transitive relations. In: LICS, pp. 24–34 (1999)
Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991)
Grädel, E., Otto, M., Rosen, E.: Two–variable logic with counting is decidable. In: LICS, pp. 306–317 (1997)
Gentilini, R., Piazza, C., Policriti, A.: Symbolic graphs: Linear solutions to connectivity related problems. Algorithmica 50(1), 120–158 (2007)
Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: KR, pp. 335–346 (1991)
Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 286–299. Springer, Heidelberg (2006)
Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded μ–calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423–437. Springer, Heidelberg (2002)
Marrero, W.: Using bdds to decide ctl. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 222–236. Springer, Heidelberg (2005)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first–order two–variable logic with counting. SIAM Journal of Computing 29(4), 1083–1117 (2000)
Pan, G., Sattler, U., Vardi, M.Y.: Bdd-based decision procedures for the modal logic k. Journal of Applied Non-classical Logics 49 (2005)
Somenzi, F.: Cudd: Cu decision diagram package, release 2.4.1 (2005), http://vlsi.colorado.edu/~fabio/CUDD
Tobies, S.: PSPACE reasoning for graded modal logics. Journal Log. Comput. 11(1), 85–106 (2001)
Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. of Computer and System Sciences 32(2), 183–221 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrante, A., Napoli, M., Parente, M. (2009). Graded-CTL: Satisfiability and Symbolic Model Checking. In: Breitman, K., Cavalcanti, A. (eds) Formal Methods and Software Engineering. ICFEM 2009. Lecture Notes in Computer Science, vol 5885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10373-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-10373-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10372-8
Online ISBN: 978-3-642-10373-5
eBook Packages: Computer ScienceComputer Science (R0)