Specification in PDL with Recursion

Title: Specification in PDL with Recursion
Speaker: Xinxin Liu
Time: 3:00pm, Thursday, May.26
Venue: Lecture Room, Level 3 Building #5, Institute of Software, CAS

Abstract: Propositional Dynamic Logic (PDL) was first introduced in the late 70s as a formalism for reasoning about programs. Soon afterwards the logic was outdated for that purpose through the introduction of the modal mu-calculus, because the latter is much more expressive with just a little higher complexity. Then in recent years PDL became popular again because of its simplicity. In this work we introduce limited use of recursion into PDL, with the purpose of obtaining a language which keeps a good balance between expressiveness and ease of analysis.