Advertisement

CTL Model-Checking with Graded Quantifiers

  • Alessandro Ferrante
  • Margherita Napoli
  • Mimmo Parente
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

The use of the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k, has been thoroughly studied in various kinds of logics. In classical logic there are counting quantifiers, in modal logics graded modalities, in description logics number restrictions.

Recently, the complexity issues related to the decidability of the μ-calculus, when the universal and existential quantifiers are augmented with graded modalities, have been investigated by Kupfermann, Sattler and Vardi. They have shown that this problem is ExpTime-complete.

In this paper we consider another extension of modal logic, the Computational Tree Logic CTL, augmented with graded modalities generalizing standard quantifiers and investigate the complexity issues, with respect to the model-checking problem. We consider a system model represented by a pointed Kripke structure \(\mathcal{K}\) and give an algorithm to solve the model-checking problem running in time \(O(|\mathcal{K}|\cdot |\varphi|)\) which is hence tight for the problem (where |ϕ| is the number of temporal and boolean operators and does not include the values occurring in the graded modalities).

In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples (or evidences) to a specification ϕ given in CTL. However these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both NP-hard and coNP-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of this graded-CTL logic, and have proved that the model-checking problem is solvable in polynomial time.

Keywords

Model Checker Modal Logic Linear Temporal Logic Polynomial Space Kripke Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [CCGR99]
    Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. [CG07]
    Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transf. 9(5), 429–445 (2007)CrossRefzbMATHGoogle Scholar
  3. [CGP99]
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  4. [CIW+01]
    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)CrossRefGoogle Scholar
  5. [CLRS01]
    Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press, Cambridge (2001)zbMATHGoogle Scholar
  6. [CPR03]
    Caprara, A., Panconesi, A., Rizzi, R.: Packing cycles in undirected graphs. Journal of Algorithms 48(1), 239–256 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  7. [CV03]
    Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Verification: Theory and Practice, pp. 208–224 (2003)Google Scholar
  8. [DRS03]
    Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: ECBS, pp. 214–223 (2003)Google Scholar
  9. [Fin72]
    Fine, K.: In so many possible worlds. Notre Dame Journal of Formal Logic 13(4), 516–520 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  10. [FNP08]
    Ferrante, A., Napoli, M., Parente, M.: Graded CTL. In: Preparation (2008)Google Scholar
  11. [GMV99]
    Ganzinger, H., Meyer, C., Veanes, M.: The two–variable guarded fragment with transitive relations. In: LICS, pp. 24–34 (1999)Google Scholar
  12. [GOR97]
    Grädel, E., Otto, M., Rosen, E.: Two–variable logic with counting is decidable. In: LICS, pp. 306–317 (1997)Google Scholar
  13. [HB91]
    Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: KR, pp. 335–346 (1991)Google Scholar
  14. [Hol97]
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefGoogle Scholar
  15. [KSV02]
    Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded μ–calculus. In: CADE-18: Proceedings of the 18th International Conference on Automated Deduction, London, UK, pp. 423–437. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. [McM]
    McMillan, K.: The Cadence smv model checker, http://www.kenmcmil.com/psdoc.html
  17. [PST00]
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  18. [QS82]
    Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Proc. of the 5th Colloquium on Intern. Symposium on Programming, London, UK, pp. 337–351. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  19. [Tob01]
    Tobies, S.: PSPACE reasoning for graded modal logics. Journal Log. Comput. 11(1), 85–106 (2001)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Alessandro Ferrante
    • 1
  • Margherita Napoli
    • 1
  • Mimmo Parente
    • 1
  1. 1.Dipartimento di Informatica ed Applicazioni “R.M. Capocelli”University of SalernoItaly

Personalised recommendations