Logical analysis of demonic nondeterministic programs
The work
| Authors | Stéphane Demri; Ewa Orłowska |
|---|---|
| Type | article |
| Year | 1996 |
| Citekey | demri1996logical |
Where it appeared
| Published in | Theoretical Computer Science |
|---|---|
| Publisher | Elsevier BV |
| Volume | 166 |
| Issue | 1-2 |
| Pages | 173--202 |
Identifiers
| DOI | 10.1016/0304-3975(95)00190-5 |
|---|---|
| OpenAlex | W2073882281 |
Access
| Landing page | https://doi.org/10.1016/0304-3975(95)00190-5 |
|---|---|
| Free full text | https://hal.science/hal-03193705 |
Abstract
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(*)).
A copy is held
pdf, 1.6 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-16 00:00 UTC |
| Approved by | a person 2026-08-16 22:17 UTC |
Filed under
Cite it as
@article{demri1996logical,
title = {Logical analysis of demonic nondeterministic programs},
author = {Stéphane Demri and Ewa Orłowska},
year = {1996},
journal = {Theoretical Computer Science},
volume = {166},
number = {1-2},
pages = {173--202},
publisher = {Elsevier BV},
doi = {10.1016/0304-3975(95)00190-5},
}
This record lives at https://refs.drheap.org/demri1996logical/ and will keep doing so.