OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

Boudou, Joseph Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition. (2016) In: International Joint Conference on Automated Reasoning (IJCAR 2016), 27 June 2016 - 2 July 2016 (Coimbra, Portugal).

[img]
Preview
(Document in English)

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

Official URL: https://doi.org/10.1007/978-3-319-40229-1_26

Abstract

PPDL det extends propositional dynamic logic (PDL) with parallel composition of programs. This new construct has separation semantics: to execute the parallel program (α||β) the initial state is separated into two substates and the programs α and β are executed on these substates. By adapting the elimination of Hintikka sets procedure, we provide a decision procedure for the satisfiability problem of PPDL det. We prove that this decision procedure can be executed in deterministic exponential time, hence that the satisfiability problem of PPDL det is EXPTIME-complete.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 9706 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN 978-3-319-40228-4 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-319-40229-1_26
HAL Id:hal-01757357
Audience (conference):International conference proceedings
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:22 Mar 2018 13:10

Repository Staff Only: item control page