Logical analysis of demonic nondeterministic programs

A logical framework is presented for representing and reasoning about nondeterministic programs that may not terminate. We propose a logic PDL(; ;, |, d(∗)) which is an extension of dynamic logic such that the program constructors related to demonic operations are introduced in its language. A complete and sound Hilbert-style proof system is given and it is shown that PDL(; ;, |, d(∗)) is decidable. In the second part of this paper, a translation is defined between PDL(; ;, |, d(∗)) and a relational logic. A sound and complete Rasiowa-Sikorski-style proof system for the relational logic is given. It provides a natural deduction-style method of reasoning for PDL(; ;, |, d(∗)).

Authors

• Stéphane Demri
• Ewa Orłowska

Keywords

No keywords are indexed for this paper.