Boudou, Joseph
Exponential-Size Model Property for PDL with Separating Parallel Composition.
(2015)
In: Mathematical Foundations of Computer Science (MFCS 2015), 24 August 2015 - 28 August 2015 (Milan, Italy).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 210kB |
Official URL: https://doi.org/10.1007/978-3-662-48057-1_10
Abstract
Propositional dynamic logic is extended with a parallel program having a separating semantic: the program (α || β) executes α and β on two substates of the current state. We prove that when the composition of two substates is deterministic, the logic has the exponential-size model property. The proof is by a piecewise filtration using an adaptation of the Fischer-Ladner closure. We conclude that the satisfiability of the logic is decidable in NEXPTIME.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to Springer editor. This papers appears in volume 9234 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN 978-3-662-48056-4 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-662-48057-1_10 |
| HAL Id: | hal-02559772 |
| Audience (conference): | International conference proceedings |
| 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 (France) |
| Statistics: | download |
| Deposited On: | 21 Apr 2020 10:04 |
Repository Staff Only: item control page
