Abstract: 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.
Publication Year: 2010
Publication Date: 2010-08-11
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot