Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/LICS.2013.20 | LICS |
Keywords | Field | DocType |
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 | Atomic formula,Discrete mathematics,Autoepistemic logic,Computer science,Zeroth-order logic,Well-formed formula,Propositional formula,Propositional variable,Dynamic logic (modal logic),Intermediate logic | Conference |
ISSN | Citations | PageRank |
1043-6871 | 23 | 1.19 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Philippe Balbiani | 1 | 959 | 88.63 |
| Andreas Herzig | 2 | 655 | 48.55 |
| Nicolas Troquard | 3 | 266 | 29.54 |