A Canonical Model Construction for Iteration-Free PDL with Intersection

Florian Bruse
(University of Kassel)
Daniel Kernberger
(University of Kassel)
Martin Lange
(University of Kassel)

We study the axiomatisability of the iteration-free fragment of Propositional Dynamic Logic with Intersection and Tests. The combination of program composition, intersection and tests makes its proof-theory rather difficult. We develop a normal form for formulae which minimises the interaction between these operators, as well as a refined canonical model construction. From these we derive an axiom system and a proof of its strong completeness.

In Domenico Cantone and Giorgio Delzanno: Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016), Catania, Italy, 14-16 September 2016, Electronic Proceedings in Theoretical Computer Science 226, pp. 120–134.
Published: 13th September 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.226.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org