Flat fragments of CTL and CTL: separating the expressive and distinguishing powers
Dennis R. Dams · Logic Journal of IGPL · 1999
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