On the Expressive Power of Dynamic Logic. II,
Abstract
In this paper we study the expressive power of nondeterminism in dynamic logic. In particular, we show that first order regular dynamic logic without equality (hereafter abbreviated DL) is more expressive than its deterministic counterpart (DDL). This result has already been shown for the quantifier-free case (MW) and for the propositional case (HR). Berman and Tiuryn have recently extended the present result to the case with equality. By contrast, Meyer and Tiuryn have shown in (MT) that in the r.e. case, deterministic and nondeterministic dynamic logic coincide. The proof hinges on showing that in a precise sense a deterministic regular program cannot search a full binary tree. Because of this, the truth of a first-order DDL formula, even with first-order quantification, cannot depend on every value in a full binary tree. From this it will follow that DDL is less expressive than DL. The kernel of the proof presented here can already be found in (HR). (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1981
- Accession Number
- ADA107430
Entities
People
- Joseph Halpern
Organizations
- Massachusetts Institute of Technology