Markus Latte, Separation Results for XCTL
Separation Results for XCTL
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.
For regular, visibly pushdown and deterministic context-free
languages, the separation of the respective XCTL can be proven by
automata-theoretic techniques. However, these techniques introduce
non-determinism on the automata side. As non-determinism is also the
difference between DCFL and CFL, these techniques seem to be
inappropriate to separate XCTL[DCFL] from XCTL[CFL]. Nevertheless, we
show the separation of DCFL from CFL for the EF/AG-fragment of XCTL.