Computer Science – Logic in Computer Science
Scientific paper
2009-06-14
Computer Science
Logic in Computer Science
The author of this paper, Volker Weber, died after submitting it to CSL 2009. The version published here incorporates a few sm
Scientific paper
We classify the complexity of the satisfiability problem for extensions of CTL and UB. The extensions we consider are Boolean combinations of path formulas, fairness properties, past modalities, and forgettable past. Our main result shows that satisfiability for CTL with all these extensions is still in 2-EXPTIME, which strongly contrasts with the nonelementary complexity of CTL* with forgettable past. We give a complete classification of combinations of these extensions, yielding a dichotomy between extensions with 2-EXPTIME-complete and those with EXPTIME-complete complexity. In particular, we show that satisfiability for the extension of UB with forgettable past is complete for 2-EXPTIME, contradicting a claim for a stronger logic in the literature. The upper bounds are established with the help of a new kind of pebble automata.
No associations
LandOfFree
On the Complexity of Branching-Time Logics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On the Complexity of Branching-Time Logics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the Complexity of Branching-Time Logics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-341779