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.