loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 24th Annual IEEE Symposium on Logic In Computer Science
Graded Computation Tree Logic
Los Angeles, California
August 11-August 14
ISBN: 978-0-7695-3746-7
In modal logics, graded (world) modalities have been deeply investigated as a useful framework for generalizing standard existential and universal modalities in such a way that they can express statements about a given number of immediately accessible worlds. These modalities have been recently investigated with respect to the mu-calculus, which have provided succinctness, without affecting the satisfiability of the extended logic, i.e., it remains solvable in ExpTime. A natural question that arises is how logics that allow reasoning about paths could be affected by considering graded path modalities. In this paper, we investigate this question in the case of the branching-time temporal logic CTL (GCTL, for short). We prove that, although GCTL is more expressive than CTL, the satisfiability problem for GCTL remains solvable in ExpTime. This result is obtained by exploiting an automata-theoretic approach. In particular, we introduce the class of partitioning alternating Büchi tree automata and show that the emptiness problem for them is ExpTime-Complete. The satisfiability result turns even more interesting as we show that GCTL is exponentially more succinct than graded mu-calculus.
Index Terms:
Temporal logics, graded modalities, minimality, conservativeness, satisfiability, automata-theoretic approach
Citation:
Alessandro Bianco, Fabio Mogavero, Aniello Murano, "Graded Computation Tree Logic," lics, pp.342-351, 2009 24th Annual IEEE Symposium on Logic In Computer Science, 2009
Usage of this product signifies your acceptance of the Terms of Use.