\(R\)-generability, and definability in branching time logics (Q1197983)

We study the power of branching time temporal logics such as \(\text{CTL}^*\) to define properties of computation paths related to the condition of \(R\)-generability introduced by Emerson. This condition ensures that neither past behaviour, nor fairness or scheduling criteria are necessary to determine the admissible computations, and it is thus of some practical significance. As shown by Emerson \(R\)-generability can be analysed in terms of the conditions of suffix, fusion, and limit closure. In general \(R\)-generability and the three closure conditions are undefinable. However, a slightly more refined analysis reveals that relativised definability results are in fact possible. The main results are summarised as follows: 1. Limit closure in undefinable, even when relativised to frames that are both fusion and suffix closed. 2. Fusion closure is definable for frames that are both limit and suffix closed. 3. Suffix closure is definable for frames that are either limit or fusion closed. Moreover, the conditions in both (2) and (3) are necessary.