Browse Prior Art Database

Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness

IP.com Disclosure Number: IPCOM000128135D
Original Publication Date: 1981-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 21 page(s) / 49K

Publishing Venue

Software Patent Institute

Related People

Mordechai Ben-Ari: AUTHOR [+5]

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 axioms for propositional dynamic logic. KEYWORDS: deterministic propositional dynamic logic, propositional dynamic logic, decision procedure, tableau method, completeness. This research was partially supported by grants from the National Science and Engineering Research Council of Canada, NSF Grant #MCS 7719754, the Israeli Academy of Sciences and Humanities, and the Basic Research Foundation.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 10% of the total text.

Page 1 of 21

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness

Mordechai Ben-Ari, Department of Mathematical Sciences, Division of Computer Sciences, Tel Aviv University, Ramat Aviv, Israel.

Joseph Y. Halpern, Mathematics Department, Harvard University, Cambridge, Massachusetts 02138

Amir Pnueli, Department of Mathematical Sciences, Division of Computer Sciences, Tel Aviv University, Ramat Aviv, Israel.

December 17, 1980.

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 axioms for propositional dynamic logic.

KEYWORDS: deterministic propositional dynamic logic, propositional dynamic logic, decision procedure, tableau method, completeness.

This research was partially supported by grants from the National Science and Engineering Research Council of Canada, NSF Grant #MCS 7719754, the Israeli Academy of Sciences and Humanities, and the Basic Research Foundation.

1. Introduction 2

Dynamic logic, an outgrowth of modal logic, was introduced by Pratt [51 as a logical theory capable of expressing properties of computer programs. Fischer and Ladner [11 have investigated the purely logical properties of the propositional fragment of dynamic logic (PDL). Their principal results are a decision procedure for satisfiability and a proof of the finite model property: if a formula in PDL is satisfiable then it is satisfiable a finite model, in fact one of size 2n. These results were re-derived and extended by Pratt [6, 71 who gave a 2cn deterministic time algorithm for PDL using tableau techniques. Segerberg [81 proposed an axiomatization for PDL, which was later shown to be complete by various researchers (see [2] for an elementary proof and further references).

Deterministic PDL (DPDL) is the logical theory with the same syntax as PDL but with its semantics restricted so that in each state an atomic program .specifies at most on successor state. Parikh [3] has given a decision procedure for DPDL as a corollary to the decision procedure for a very strong theory: second order process logic. However, that procedure is of non-elementary complexity and cannot be considered practical for DPDL.

Massachusetts Institute of Technology Page 1 Dec 31, 1981

Page 2 of 21

Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness

We give a 2cn deterministic time decision procedure for satisfiability'in DPDL. This agrees with the lower bound shown by Parikh [4]. The proof uses the notion of a partial D model for a formula p, which is precisely what we end u...