A note on knowledge-based programs and specifications

TL;DR

This paper examines the monotonicity properties of knowledge-based programs, showing that they satisfy one form of monotonicity but not another, which can be advantageous in certain specifications.

Contribution

It clarifies the monotonicity properties of knowledge-based programs and argues that their non-satisfaction of a certain property can be beneficial.

Findings

Knowledge-based programs satisfy the first monotonicity property.

They do not satisfy the second, which can be a feature.

Standard programs also fail the second property under broader specifications.

Abstract

Knowledge-based program are programs with explicit tests for knowledge. They have been used successfully in a number of applications. Sanders has pointed out what seem to be a counterintuitive property of knowledge-based programs. Roughly speaking, they do not satisfy a certain monotonicity property, while standard programs (ones without tests for knowledge) do. It is shown that there are two ways of defining the monotonicity property, which agree for standard programs. Knowledge-based programs satisfy the first, but do not satisfy the second. It is further argued by example that the fact that they do not satisfy the second is actually a feature, not a problem. Moreover, once we allow the more general class of knowledge-based specifications, standard programs do not satisfy the monotonicity property either.