The Decidability of RPTL

In this paper we look at regular path temporal logic, RPTL, a modal logic which combines the ability to quantify over (finite) paths described by regular expressions (a property which characterises PDL) with the addition of temporal operators. The formulation of RPTL was inspired by agent programming verification considerations. In this paper we prove the decidabilty of RPTL and establish complexity bounds on the satisfiability problem for RPTL by translating it into the theory of alternating tree automata on infinite trees.