Propositional Dynamic Logic with Storing, Recovering and Parallel Composition
The work
| Authors | Mario Folhadela Benevides; Renata de Freitas; Petrúcio Viana |
|---|---|
| Editors | |
| Type | article |
| Year | 2011 |
| Citekey | benevides2011propositional |
Where it appeared
| Published in | Electronic Notes in Theoretical Computer Science |
|---|---|
| Publisher | Elsevier BV |
| Volume | 269 |
| Pages | 95--107 |
Identifiers
| DOI | 10.1016/j.entcs.2011.03.008 |
|---|---|
| OpenAlex | W1965702335 |
Access
| Landing page | https://doi.org/10.1016/j.entcs.2011.03.008 |
|---|---|
| Free full text | https://www.sciencedirect.com/science/article/pii/S157106611100065X/pdf |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
This work extends Propositional Dynamic Logic (PDL) with parallel composition operator and four atomic programs which formalize the storing and recovering of elements in data structures. A generalization of Kripke semantics is proposed that instead of using set of possible states it uses structured sets of possible states. This new semantics allows for representing data structures and using the five new operator one is capable of reasoning about the manipulation of these data structures. The use of the new language (PRSPDL) is illustrated with some examples. We present sound and complete set of axiom schemata and inference rules to prove all the valid formulas for a restricted fragment called RSPDLo.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 15:55 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{benevides2011propositional,
title = {Propositional Dynamic Logic with Storing, Recovering and Parallel Composition},
author = {Mario Folhadela Benevides and Renata de Freitas and Petrúcio Viana},
year = {2011},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier BV},
volume = {269},
pages = {95--107},
doi = {10.1016/j.entcs.2011.03.008},
}
This record lives at https://refs.drheap.org/benevides2011propositional/ and will keep doing so.