Using Counterfactuals in Knowledge-Based Programming

By Joseph Y. Halpern & Yoram Moses

Knowledge-based programs, first introduced by Halpern and Fagin [and further developed by Fagin, Halpern, Moses, and Vardi, are intended to provide a high-level framework for the design and specification of protocols. The idea is that, in knowledge-based programs, there are explicit tests for knowledge. Thus, a knowledge-based program might have the form

if K(x = 0) then y := y + 1 else skip,

where K(x = 0) should be read as "you know x = 0" and skip is the action of doing nothing. We can informally view this knowledge-based program as saying "if you know that x = 0, then set y to y + 1 (otherwise do nothing)".
Knowledge-based programs are an attempt to capture the intuition that what an agent does depends on what it knows. They have been used successfully (...) both to help in the design of new protocols and to clarify the understanding of existing protocols. However, as we show here, there are cases when, used naively, knowledge-based programs exhibit some quite counterintuitive behavior. We then show how this can be overcome by the use of counterfactuals. In this introduction, we discuss these issues informally, leaving the formal details to later sections of the paper.
Source: CLE

Posted by Tony Marmo at 00:01 GMT

Updated: Friday, 4 March 2005 19:06 GMT

Share This Post

Post Comment | Permalink