Browse Prior Art Database

On The Expressive Power of Dynamic Logic, II

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

Publishing Venue

Software Patent Institute

Related People

Joseph Y. Halpern: AUTHOR [+3]

Abstract

In this paper we study the expressive power of nondeterminism in dynamic logic. In particular, we show that fir-st 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 [MW1, and for the propositional case CHR]. Berman and Tiuryn have recently extended the present result to the case with equality. By contrast, Meyer and Tiuryn have shown in [MT1 that in the r.e. case, deterministic and nondeterministic dynamic logic coincide.

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

Page 1 of 12

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

On The Expressive Power of Dynamic Logic, II

Joseph Y. Halpern M.L T. Laboratory for Computer Science and Aik-en Computation Laboratory, Harvard University

1. Introduction

In this paper we study the expressive power of nondeterminism in dynamic logic. In particular, we show that fir-st 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 [MW1, and for the propositional case CHR]. Berman and Tiuryn have recently extended the present result to the case with equality. By contrast, Meyer and Tiuryn have shown in [MT1 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 [HRI.

2. Syntax and Semantics

We give a brief description of the syntax and semantics of DL and DDL. The reader is referred to [Harl for more details.

Syntax: Just as in first-order predicate calculus, we have predicate symbols

P, and function symbols.f, g, . , each with an associated arity, variables x, y, z, xO, xl, .., and logical symbols 3, V, and DL also uses a few special symbols in programs, namely U, and o (pronounce "diamond").

Terms are formed exactly as in first-order predicate calculus. Formulas and programs are defined inductively.

(a) Any formula of first-order predicate calculus is a formula.

M (variablo := is a (basic) program.

(0 If p, q are formulas, and a, b are programs, then pVq$ -p, 3xp, and p are formulas, and a;b, aub, and a* are programs.

(d) If p is a quantifier-free formula of predicate calculus, p? is a program. V as an abbreviation for -,3-1; similarly, [] (pronounced "boie') is an abbreviation for -no-n.

Massachusetts Institute of Technology Page 1 Dec 31, 1981

Page 2 of 12

On The Expressive Power of Dynamic Logic, II

Semantics. A state U,s) consists of two parts: I is a structure which consists of a domain, dom(l), and an interpretation of all the function and predicate symbols over this domain, and s is a ratuation which assigns values in the domain to all the variables.

Given a structure 1, p, is a mapping from programs to binary relations on valuations which describes the input-output behavior of programs in structure I, and v, is a mapping from formulas to sets of valuations, the ones valuations where the formulas is "true". Ve usuall y write U,s) I-- p instead of s e irI(p). We define both p, and ir, inductively.

(a) For p a formula of first-order predicate calculus, (1,s) I-- p is defined as usual.

M For basic progra...