Flat fragments of CTL and CTL: separating the expressive and distinguishing powers

Abstract

We study both the expressive and the distinguishing powers of flat temporal logics. These are fragments obtained by restricting the first argument of the Until operator to propositional formulae. Both the linear-time and the branching-time cases are considered. Keywords:temporal logic, LTL, CTL, expressiveness, bisimulation