Markus Latte, Separation Result for XCTL --- Part II
Separation Results for XCTL --- Part II
XCTL[A] is an extension of CTL which refines the temporal 'until' and 'release' operators with formal languages in A. In this way, XCTL can express non-regular properties, in contrast to CTL. The separation of XCTL[DCFL] from XCTL[CFL] is challenging because ordinary automata-theoretical arguments are hardly applicable.
In the first part, the separation was proven for the EF/AG-fragment. The second part revises the proof techniques to gain a separation for the whole logic.