Abstract
Graded path quantifiers have been recently introduced and investigated as a useful framework for generalizing standard existential and universal path quantifiers in the branching-time temporal logic CTL (GCTL), in such a way that they can express statements about a minimal and conservative number of accessible paths. These quantifiers naturally extend to paths the concept of graded world modalities, which has been deeply investigated for the μ- Calculus (Gμ- Calculus) where it allows to express statements about a given number of immediately accessible worlds. As for the ”non-graded” case, it has been shown that the satisfiability problem for GCTL and the Gμ- Calculus coincides and, in particular, it remains solvable in ExpTime. However, GCTL has been only investigated w.r.t. graded numbers coded in unary, while Gμ- Calculus uses for this a binary coding, and it was left open the problem to decide whether the same result may or may not hold for binary GCTL. In this paper, by exploiting an automata theoretic-approach, which involves a model of alternating automata with satellites, we answer positively to this question. We further investigate the succinctness of binary GCTL and show that it is at least exponentially more succinct than Gμ- Calculus.
Work partially supported by MIUR PRIN Project n.2007-9E5KM8.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Apostol, T.M.: Introduction to Analytic Number Theory. Springer, Heidelberg (1976)
Bianco, A., Mogavero, F., Murano, A.: Graded Computation Tree Logic. In: LICS 2009, pp. 342–351 (2009)
Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The Complexity of Enriched μ-Calculi. LMCS 4(3:11), 1–27 (2008)
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)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time. JACM 33(1), 151–178 (1986)
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.: Graded-CTL: Satisfiability and Symbolic Model Checking. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 306–325. Springer, Heidelberg (2009)
Fine, K.: In So Many Possible Worlds. NDJFL 13, 516–520 (1972)
De Giacomo, G., Lenzerini, M.: Concept Language with Number Restrictions and Fixpoints, and its Relationship with Mu-calculus. In: ECAI 1994, pp. 411–415 (1994)
Grädel, E.: On The Restraining Power of Guards. JSL 64(4), 1719–1742 (1999)
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)
Kupferman, O., Vardi, M.Y.: Memoryful Branching-Time Logic. In: LICS 2006, pp. 265–274. IEEE Computer S., Los Alamitos (2006)
Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata Theoretic Approach to Branching-Time Model Checking. JACM 47(2), 312–360 (2000)
Lamport, L.: “Sometime” is Sometimes “Not Never”: On the Temporal Logic of Programs. In: POPL 1980, pp. 174–185 (1980)
Lange, M.: A Purely Model-Theoretic Proof of the Exponential Succinctness Gap between CTL+ and CTL. IPL 108(5), 308–312 (2008)
Lutz, C.: Complexity and Succinctness of Public Announcement Logic. In: AAMAS 2006, pp. 137–143 (2006)
Miyano, S., Hayashi, T.: Alternating Finite Automata on ω-Words. TCS 32, 321–330 (1984)
Muller, D.E., Schupp, P.E.: Alternating Automata on Infinite Trees. TCS 54(2-3), 267–276 (1987)
Pnueli, A.: The Temporal Logic of Programs. In: FOCS 1977, pp. 46–57 (1977)
Pnueli, A.: The Temporal Semantics of Concurrent Programs. TCS 13, 45–60 (1981)
Rabin, M.O.: Decidability of Second-Order Theories and Automata on Infinite Trees. BAMS 74, 1025–1029 (1968)
Tobies, S.: PSpace Reasoning for Graded Modal Logics. JLC 11(1), 85–106 (2001)
Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS 1986, pp. 332–344 (1986)
Vardi, M.Y., Wolper, P.: Automata-Theoretic Techniques for Modal Logics of Programs. JCSS 32(2), 183–221 (1986)
Wilke, T.: CTL+ is Exponentially More Succinct than CTL. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 110–121. Springer, Heidelberg (1999)
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
Bianco, A., Mogavero, F., Murano, A. (2010). Graded Computation Tree Logic with Binary Coding. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-15205-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15204-7
Online ISBN: 978-3-642-15205-4
eBook Packages: Computer ScienceComputer Science (R0)