Algebraic characterization of temporal logics on forests.
Szabolcs Iván · arXiv (Cornell University) · 2015
We associate a temporal logic $\mathrm{FL}(\mathcal{L})$ to class $\mathcal{L}$ of (regular) forest languages where a forest is an ordered finite sum of finite unranked trees. Under a natural assumption of the set $\mathcal{L}$ of modalities we derive an algebraic characterization of the forest languages definable in $\mathrm{FL}(\mathcal{L})$, in terms of the iterated Moore product of forest automata. Using this characterization we derive a polynomial-time algorithm to decide definability of the fragment $\mathrm{EF}^*$ of $\mathrm{CTL}$, evaluated on forests.