OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Axiomatization and computability of a variant of iteration-free PDL with fork

Balbiani, Philippe and Boudou, Joseph Axiomatization and computability of a variant of iteration-free PDL with fork. (2019) Journal of Logical and Algebraic Methods in Programming, 108. 47-68. ISSN 2352-2208

[img]
Preview
(Document in English)

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

Official URL: https://doi.org/10.1016/j.jlamp.2019.06.004

Abstract

We devote this paper to the axiomatization and the computability of a variant of iteration-free PDL with fork. Concerning the axiomatization, our resuts are based on the following: although the program operation of fork 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 fork 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 fork and we use large programs for the proof of the Truth Lemma. Concerning the computability, we prove by a selection procedure that our variant of PDL has a strong finite property, hence is decidable.

Item Type:Article
Additional Information:https://www.sciencedirect.com/science/article/pii/S2352220818300713
HAL Id:hal-02378379
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Funders:
ANR : Agence nationale de la recherche, Programme Modèles Num ériques 2011 (France) - RILA Partenariat Hubert Curien (PHC) (France, Bulgarie)
Statistics:download
Deposited On:15 Nov 2019 14:57

Repository Staff Only: item control page