Propositional Dynamic Logic with Storing, Recovering and Parallel Composition | Zendy

Mário Benevides | Zendy; Renata de Freitas | Zendy; Petrúcio Viana | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Propositional Dynamic Logic with Storing, Recovering and Parallel Composition

Author(s) -

Mário Benevides,

Renata de Freitas,

Petrúcio Viana

Publication year - 2011

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2011.03.008

Subject(s) - computer science , axiom , rule of inference , generalization , semantics (computer science) , fragment (logic) , theoretical computer science , operator (biology) , set (abstract data type) , kripke semantics , modal logic , propositional calculus , composition (language) , programming language , algorithm , intermediate logic , mathematics , description logic , modal , mathematical analysis , biochemistry , chemistry , geometry , repressor , transcription factor , polymer chemistry , gene , linguistics , philosophy

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research