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
|
(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