摘要：
首先介绍了动态逻辑PDL（propositional dynamic logic）在程序验证中的作用，以及PDL的结构不变性、有穷模型性、公理化和完全性。在此基础上，将已有的对于导航中推理研究向PDL进行扩充。丰富了原来的逻辑语言并介绍了在新的逻辑语言EPDL下语义，比较了新的语义下的模型类和标准模型类的对应关系。
