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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.
R. I. Brafman, J.-C. Latombe, Y. Moses, and Y. Shoham. Applications of a logic of knowledge to motion planning under uncertainty. Journal of the ACM, 44(5):633–668, Sept. 1997.
K. Engelhardt, R. van der Meyden, and Y. Moses. Knowledge and the logic of local propositions. In I. Gilboa, editor, Theoretical Aspects of Rationality and Knowledge, Proceedings of the Seventh Conference (TARK 1998), pages 29–41. Morgan Kaufmann, July 1998.
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT-Press, 1995.
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Knowledge-based programs. Distributed Computing, 10(4):199–225, 1997.
J. Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549–587, July 1990.
I. Hayes. Separating timing and calculation in real-time refinement. In J. Grundy, M. Schwenke, and T. Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science, pages 1–16. Springer-Verlag, 1998.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
C. C. Morgan. Programming from Specifications. Prentice Hall, 1990.
J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, Dec. 1987.
Y. Moses and O. Kislev. Knowledge-oriented programming. In Proceeding of the 12th Annual ACM Symposium on Principles of Distributed Computing (PODC 93), pages 261–270, New York, USA, Aug. 1993. ACM Press.
Y. Moses and M. R. Tuttle. Programming simultaneous actions using common knowledge. Algorithmica, 3:121–169, 1988.
B. Sanders. A predicate transformer approach to knowledge and knowledge-based protocols. In Proceeding of the 10th Annual ACM Symposium on Principles of Distributed Computing (PODC 91), pages 217–230, 19–21 Aug. 1991.
M. Utting and C. Fidge. A real-time refinement calculus that changes only time. In H. Jifeng, J. Cooke, and P. Wallis, editors, BCS-FACS Seventh Refinement Workshop. Springer-Verlag, 1996.
R. van der Meyden. Knowledge based programs: On the complexity of perfect recall in finite environments. In Y. Shoham, editor, Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, pages 31–50. Morgan Kaufmann, Mar. 17–20 1996.
R. van der Meyden and Y. Moses. On refinement and temporal annotations. http://www.cse.unsw.edu.au/~meyden/research/temprefine.ps.
R. van der Meyden and Y. Moses. Top-down considerations on distributed systems. In Proceedings 12th International Symposium on Distributed Computing, DISC’98, volume 1499 of LNCS, pages 16–19, Sept. 1998. Springer-Verlag.
M. Y. Vardi. Implementing knowledge-basd programs. In Y. Shoham, editor, Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, pages 15–30. Morgan Kaufmann, Mar. 17–20 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Engelhardt, K., van der Meyden, R., Moses, Y. (2000). A Program Refinement Framework Supporting Reasoning about Knowledge and Time. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_8
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive