OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Dynamic logic of propositional assignments : a well-behaved variant of PDL

Balbiani, Philippe and Herzig, Andreas and Troquard, Nicolas Dynamic logic of propositional assignments : a well-behaved variant of PDL. (2013) In: 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2013), 25 June 2013 - 28 June 2013 (New Orleans, LA, United States).

(Document in English)

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

Official URL: http://dx.doi.org/10.1109/LICS.2013.20


We study a version of Propositional Dynamic Logic (PDL) that we call Dynamic Logic of Propositional Assignments (DL-PA). The atomic programs of DL-PA are assignments of propositional variables to true or to false. We show that DL-PA behaves better than PDL, having e.g. compactness and eliminability of the Kleene star. We establish tight complexity results: both satisfiability and model checking are EXPTIME-complete.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to IEEE editor. The definitive version is available at http://ieeexplore.ieee.org ISSN : 1043-6871 Print ISBN : 978-1-4799-0413-6 The original PDF of the article can be found at : http://ieeexplore.ieee.org/xpl/abstractAuthors.jsp?arnumber=6571546
HAL Id:hal-01240721
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Other partners > Consiglio Nazionale delle Ricerche - CNR (ITALY)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (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:
Deposited On:20 Nov 2015 14:44

Repository Staff Only: item control page