Rosenschein, S. J., & Kaelbling, L. P. (1986, January). The synthesis of digital machines with provable epistemic properties. In Theoretical aspects of reasoning about knowledge (pp. 83-98). Morgan Kaufmann.
Researchers using epistemic logic as a formal framework for studying knowledge properties of artificial-intelligence (AI) systems often interpret the knowledge formula to mean that machine encodes in its state as a syntactic formula or can derive it inferentially. If is defined instead in terms of the correlation between the state of the machine and that of its environment, the formal properties of modal system S5 can be satisfied without having to store representations of formulas as data structures. In this paper, we apply the correlational definition of knowledge to machines with composite structure and describe the semantics of knowledge representations in terms of correlation-based denotation functions. In particular, we describe how epistemic properties of synchronous digital machines can be analyzed, starting at the level of gates and delays, by modeling the machine’s components as agents in a multiagent system and reasoning about the flow of information among them. We also introduce Rex, a language for computing machine descriptions recursively, and explain how it can be used to construct machines with provable informational properties.