Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness
Let p be a formular in deterministic propositional dynamic logic. A decision procedure for the satisfiability of p is given along with a construction of a finite model for every satisifiable p. The decision procedure runs in deterministic time 2^cn and the size of the model is bounded by n^2 * 4^n,...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149001 |