Deterministic propositional dynamic logic: Finite models, complexity, and completeness

Mordechai Ben-Ari; Joseph Y Halpern; Amir Pnueli

doi:10.1016/0022-0000(82)90018-6

Back

Deterministic propositional dynamic logic: Finite models, complexity, and completeness

Journal article

an open version is available

Peer reviewed

Deterministic propositional dynamic logic: Finite models, complexity, and completeness

Mordechai Ben-Ari, Joseph Y Halpern and Amir Pnueli

Journal of Computer and System Sciences, Vol.25(3), pp.402-417

1982

DOI: https://doi.org/10.1016/0022-0000(82)90018-6

Files and links (1)

url

https://doi.org/10.1016/0022-0000(82)90018-6View

Published (Version of record)https://www.elsevier.com/about/policies/open-access-licenses/elsevier-user-licenseOther, Open Access

Abstract

Let p be a formula 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 satisfiable p. The decision procedure runs in deterministic time 2cn and the size of the model is bounded by n2 · 4n, where n is the length of p. Finally, a complete axiomatization for deterministic propositional dynamic logic is given, based on the Segerberg axoms for propositional dynamic logic.

Details

Title: Deterministic propositional dynamic logic: Finite models, complexity, and completeness
Creators: Mordechai Ben-Ari (null) - 972WIS_INST___78
Joseph Y Halpern (null)
Amir Pnueli (null) - 972WIS_INST___83
Resource Type: Journal article
Publication Details: Journal of Computer and System Sciences, Vol.25(3), pp.402-417; 1982
Number of pages: 16
Language: English
DOI: https://doi.org/10.1016/0022-0000(82)90018-6
Grant note: This research was partially supported by grants from the National Science and Engineering Research Council of Canada, the Israeli Academy of Sciences and Humanities, and the Basic Research Foundation.
Record Identifier: 993264644803596

Metrics

2 Record Views