DocumentCode
626283
Title
Dynamic Logic of Propositional Assignments: A Well-Behaved Variant of PDL
Author
Balbiani, Philippe ; Herzig, Andreas ; Troquard, Nicolas
Author_Institution
IRIT, Univ. de Toulouse, Toulouse, France
fYear
2013
fDate
25-28 June 2013
Firstpage
143
Lastpage
152
Abstract
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.
Keywords
computability; computational complexity; formal verification; DL-PA; EXPTIME-complete; Kleene star compactness; Kleene star eliminability; PDL; dynamic logic of propositional assignments; model checking; propositional variable assignment; satisfiability; Abstracts; Complexity theory; Computational modeling; Cost accounting; Handheld computers; Model checking; Radiation detectors;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
Conference_Location
New Orleans, LA
ISSN
1043-6871
Print_ISBN
978-1-4799-0413-6
Type
conf
DOI
10.1109/LICS.2013.20
Filename
6571546
Link To Document