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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com