Article

A Program Refinement Framework Supporting Reasoning about Knowledge and Time

Authors:

Kai Engelhardt,

Ron van der Meyden,

Yoram MosesAuthors Info & Claims

FOSSACS '00: Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000

Pages 114 - 129

Published: 25 March 2000 Publication History

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.

References

[1]

R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.

[2]

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.

[3]

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.

[4]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT-Press, 1995.

[5]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Knowledge-based programs. Distributed Computing, 10(4):199-225, 1997.

[6]

J. Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549-587, July 1990.

[7]

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.

[8]

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.

[9]

C. C. Morgan. Programming from Specifications. Prentice Hall, 1990.

[10]

J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287-306, Dec. 1987.

[11]

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.

[12]

Y. Moses and M. R. Tuttle. Programming simultaneous actions using common knowledge. Algorithmica, 3:121-169, 1988.

[13]

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.

[14]

M. Utting and C. Fidge. A real-time re_nement calculus that changes only time. In H. Jifeng, J. Cooke, and P. Wallis, editors, BCS-FACS Seventh Refinement Workshop. Springer-Verlag, 1996.

[15]

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.

[16]

R. van der Meyden and Y. Moses. On refinement and temporal annotations. http://www.cse.unsw.edu.au/~{}meyden/research/temprefine.ps.

[17]

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.

[18]

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.

Cited By

Gammie P(2011)Verified synthesis of knowledge-based programs in finite synchronous environmentsProceedings of the Second international conference on Interactive theorem proving10.5555/2033939.2033950(87-102)Online publication date: 22-Aug-2011
https://dl.acm.org/doi/10.5555/2033939.2033950
Halpern JPetride S(2010)A knowledge-based analysis of global function computationDistributed Computing10.1007/s00446-010-0111-723:3(197-224)Online publication date: 1-Nov-2010
https://dl.acm.org/doi/10.1007/s00446-010-0111-7

A Program Refinement Framework Supporting Reasoning about Knowledge and Time
1. Theory of computation

Recommendations

A logical framework for reasoning about logical specifications
A generic web-based knowledge discovery framework for case-based reasoning
A Time Refinement Framework Based on iUML-B State Machine
Event-B is a formal modeling language that is very suitable for software engineering, but it lacks the ability of modeling time. Researchers have proposed some methods for modeling time constraints in Event-B. The limitations with existing methods are ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FOSSACS '00: Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000

March 2000

390 pages

ISBN:3540672575

Editor:
Jerzy Tiuryn

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 March 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gammie P(2011)Verified synthesis of knowledge-based programs in finite synchronous environmentsProceedings of the Second international conference on Interactive theorem proving10.5555/2033939.2033950(87-102)Online publication date: 22-Aug-2011
https://dl.acm.org/doi/10.5555/2033939.2033950
Halpern JPetride S(2010)A knowledge-based analysis of global function computationDistributed Computing10.1007/s00446-010-0111-723:3(197-224)Online publication date: 1-Nov-2010
https://dl.acm.org/doi/10.1007/s00446-010-0111-7

View Options

View options

Figures

Tables

Media

View Table of Conten