PDL Inside the μ-calculus: A Syntactic and an Automata-theoretic Characterization
Facundo Carreiro, Yde Venema, R. Goré, B. van de Kooi, Agi Kurucz · UvA-DARE (University of Amsterdam) · 2014
It is well known that propositional Dynamic Logic (PDL) can be seen as a fragment of the modal μ-calculus. In this paper we provide an exact syntactic characterization of the fragments of the μ-calculus that correspond to PDL and to test-free PDL. In addition we give automata-theoretic characterizations for PDL, with and without tests, which shed light on the relation between these logics and the modal μ-calculus and provide a new framework for the development of the theory of PDL.