Flat Fragments of CTL and CTL*: Separating the Expressive and Distinguishing211 Powers

摘要

The authors study both the expressive and the distinguishing powers of flat211u001etemporal logics. These are fragments obtained by restricting the first argument 211u001eof the Until operator in propositions. Both the linear and the braching-time 211u001ecases are considered.