Dealing with the ramification problem in the extended propositional dynamic logic

This paper presents a solution to the ramification problem in the presence of nondeterministic effect and nondeterministic choice of actions based on the extended propositional dynamic logic. We first show that the causation-based approach can be re-coded in the extended dynamic logic. Then by taking advantage of the extra expressive power of dynamic logic for compound actions and programs, any complex ramifications involved in an automatic system can be expressed and specified. Specially, Thielscher's and Shanahan's benchmark examples can be more effectively elaborated.