An Alternating Automaton for First-Order Linear Temporal Logic--Tech Report

Yannick Lebrun, Raphaël Khoury, Sylvain Hallé

In this paper we give automata-based representation of LTL-FO${}^{+}$ properties. LTL-FO${}^{+}$ is an extension of LTL that includes first-order quantification over bounded variable, thus…