Model Checking for Graded CTL

• Autorzy: Ferrante, A. , Napoli, M. , Parente, M.
• Języki publikacji: EN

Abstrakty

EN

Recently, 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 ([19]). Graded modalities refer to the use of the universal and existential quantifiers with the added capability to express the concept of at least k or all but k, for a non-negative integer k. In this paper we study the Computational Tree Logic CTL, a branching time extension of classical modal logic, augmented with graded modalities and investigate the complexity issues with respect to the model-checking problem. We consider a system model represented by a Kripke structure K and give an algorithm to solve the model-checking problem running in time [...] which is hence tight for the problem (here φ 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 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 graded-CTL, and have proved that the model-checking problem is solvable in polynomial time.

Słowa kluczowe

EN

model checking; Computational Tree Logic; Graded Modalities

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 96, nr 3
• Strony: 323-339
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Ferrante, A.

autor

Napoli, M.

autor

Parente, M.

• Dipartimento di Informatica ed Applicazioni "R.M. Capocelli", Universita di Salerno, Via Ponte don Melillo - 84084 - Fisciano (SA) - Italy,

Bibliografia

• [1] Alur, R., Yannakakis,M.: Model checking of hierarchical state machines, ACM Trans. Program. Lang. Syst., 23(3), 2001, 273-303.
• [2] Caprara, A., Panconesi, A., Rizzi, R.: Packing cycles in undirected graphs, Journal of Algorithms, 48(1), 2003, 239-256.
• [3] Chechik,M., Gurfinkel, A.: A framework for counterexample generation and exploration, Int. J. Softw. Tools Technol. Transf., 9(5), 2007, 429-445, ISSN 1433-2779.
• [4] Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri,M.: NUSMV: A New Symbolic Model Verifier, Computer Aided Verification, 1999, 495-499.
• [5] Clarke, E., Emerson, E.: Usig Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, 2, 1982, 241-266.
• [6] Clarke, E., Grumberg, O., Peled, D.: Model Checking, The MIT Press, 1999.
• [7] Clarke, E., Veith, H.: Counterexamples Revisited: Principles, Algorithms, Applications, Verification: Theory and Practice, 2003, 208-224.
• [8] Clarke, E. M., Emerson, E. A., Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, 8, 1986, 244-263.
• [9] Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient Debugging in a Formal Verification Environment, CHARME '01, Springer-Verlag, London, UK, 2001, ISBN 3-540-42541-1, 275-292.
• [10] Cormen, T., Leiserson, C., Rivest, R., Stein, C.: Introduction to Algorithms - Second Edition, TheMIT Press, 2001.
• [11] Dong, Y., Ramakrishnan, C., Smolka, S.: Model Checking and Evidence Exploration, ECBS, 2003, 214-223.
• [12] Ferrante, A., Napoli, M., Parente, M.: CTLModel-Checking with Graded Quantifiers, ATVA, 2008, 18-32.
• [13] Ferrante, A., Napoli, M., Parente, M.: Symbolic Graded-CTL Model Checking, Submitted for publication, 2009, http://gradedctl.dia.unisa.it/publications/fnp09.pdf.
• [14] Fine, K.: In So Many Possible Worlds, Notre Dame Journal of Formal Logic, 13(4), 1972, 516-520.
• [15] Ganzinger,H.,Meyer, C., Veanes,M.: The Two-VariableGuarded Fragmentwith Transitive Relations, LICS, 1999, 24-34.
• [16] Grädel, E., Otto, M., Rosen, E.: Two-Variable Logic with Counting is Decidable, LICS, 1997, 306-317.
• [17] Hollunder, B., Baader, F.: Qualifying Number Restrictions in Concept Languages, KR, 1991, 335-346.
• [18] Holzmann, G.: The Model Checker SPIN, IEEE Transactions on Software Engineering, 23(5), 1997, 279-295, ISSN 0098-5589.
• [19] Kupferman, O., Sattler, U., Vardi, M.: The Complexity of the Graded μ-Calculus, CADE-18: Proceedings of the 18th International Conference on Automated Deduction, Springer-Verlag, London, UK, 2002, ISBN 3-540-43931-5, 423-437.
• [20] La Torre, S., Napoli, M., Parente, M., Parlato, G.: Verification of scope-dependent hierarchical state machines, Inf. Comput., 206(9-10), 2008, 1161-1177, ISSN 0890-5401.
• [21] McMillan, K.: The Cadence SMV Model Checker, http://www.kenmcmil.com/psdoc.html.
• [22] Pacholski, L., Szwast, W., Tendera, L.: Complexity Results for First-Order Two-Variable Logic with Counting, SIAM Journal of Computing, 29(4), 2000, 1083-1117.
• [23] Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR, Proc. of the 5th Colloquium on Intern. Symposium on Programming, Springer-Verlag, London, UK, 1982, ISBN 3-540-11494-7, 337-351.
• [24] Tobies, S.: PSPACE Reasoning for Graded Modal Logics, Journal Log. Comput., 11(1), 2001, 85-106.