OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization

Balbiani, Philippe and Boudou, Joseph Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization. (2015) Journal of Logic and Computation, 25. 1. ISSN 0955-792X

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
505kB

Official URL: http://dx.doi.org/10.1093/logcom/exv035

Abstract

We devote this paper to the axiomatization/completeness of PRSPDL0 - a variant of iteration-free PDL with parallel composition. Our results are based on the following: although the program operation of parallel composition is not modally definable in the ordinary language of PDL, it becomes definable in a modal language strengthened by the introduction of propositional quantifiers. Instead of using axioms to define the program operation of parallel composition in the language of PDL enlarged with propositional quantifiers, we add an unorthodox rule of proof that makes the canonical model standard for the program operation of parallel composition and we use large programs for the proof of the Truth Lemma.

Item Type:Article
HAL Id:hal-01739996
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:07 Mar 2018 10:59

Repository Staff Only: item control page