A Program Refinement Framework Supporting Reasoning about Knowledge and Time

Abstract. This paper develops a highly expressive semantic framework for program refinement that supports both temporal reasoning and reasoning about the knowledge of a single agent. The framework generalizes a previously developed temporal refinement framework by amalgamating it with a logic of quantified local propositions, a generalization of the logic of knowledge. The combined framework provides a formal setting for development of knowledge-based programs, and addresses two problems of existing theories of such programs: lack of compositionality and the fact that such programs often have only implementations of high computational complexity. Use of the framework is illustrated by a control theoretic example concerning a robot operating with an imprecise position sensor.

• Type: Conference
• Year: 2000
• Where: FOSSACS
• Authors: Kai Engelhardt, Ron van der Meyden, Yoram Moses
• Keywords: Expressive Semantic Framework, FOSSACS 2000, Quantified Local Propositions, Software Engineering, Temporal Refinement Framework