Propositional Dynamic Logic (re)visited
Yde Venema, University of Amsterdam
Propositional dynamic logic (PDL) is a well-known modal logic which originates from the wave of so-called process logics that emerged in the 1970s. Characteristic to PDL is that its collection of modalities is given as the set of regular expressions over some set of atomic programs and (possibly) so-called test program. The main results on PDL, such as a sound and complete axiomatisation and the decidability and computational complexity of its satisfiability problem, were obtained relatively soon after its introducton. In the talk I will review some results on PDL that have been discovered (or re-discovered) in more recent years. Topics to be discussed include the relation of PDL with other fixpoint logics, expressive completeness results and cut-free proof systems. The main issue that I want to address concerns the Craig interpolation property for PDL, a long-standing problem that can finally be settled. I will finish with mentioning some open problems.
The talk is based on work with and by many co-authors.