MetateM: An introduction

Formal Aspects of Computing - Tập 7 Số 5 - Trang 533-549 - 1995
Howard Barringer1, Michael Fisher2, Dov M. Gabbay3, Graham Gough1, Richard Owens4
1Dept. of Comput. Sci., Univ. of Manchester, Manchester
2Department of Computing, Manchester Metropolitan University, Manchester, UK M 5GD#TAB#
3Dept. of Computing, Imperial College of Science, Technology & Medicine, London#TAB#
4Nomura Research Institute Europe Ltd., London#TAB#

Tóm tắt

Abstract

In this paper a methodology for the use of temporal logic as an executable imperative language is introduced. The approach, which provides a concrete framework, calledMetateM, for executing temporal formulae, is motivated and illustrated through examples. In addition, this introduction provides references to further, more detailed, work relating to theMetateMapproach to executable logics.

Từ khóa


Tài liệu tham khảo

10.1016/0004-3702(84)90008-0

10.1016/S0747-7171(89)80070-7

Baudinet M., 1989, Temporal Logic Programming is Complete and Expressive, 10.1145/75277.75301

Baudinet M.: A Simple Proof of the Completeness of Temporal Logic Programming. In L Fariñas del Cerro and M. Penttonen editors Intensional Logics for Programming. Oxford University Press 1992.

Barringer H. Fisher M. Gabbay D. Gough G. and Owens R.: MetateM : A Framework for Programming in Temporal Logic. In Proceedings of REX Workshop on Stepwise Refinement of Distributed Systems: Models Formalisms Correctness Mook Netherlands June 1989. (Published in Lecture Notes in Computer Science volume 430 Springer Verlag).

Barringer H. Fisher M. Gabbay D. Gough G. and Owens R.: MetateM : An Imperative Approach to Temporal Logic Programming. Formal Aspects of Computing 7(E) pp. 111–155.

Barringer H. Fisher M. and Gough G.: Fair SMG and Linear Time Model Checking. In Proceedings of Workshop on Automatic Verification Methods for Finite State Systems Grenoble France June 1989. (Published in Lecture Notes in Computer Science volume 407 Springer-Verlag).

Barringer H., 1991, Meta-Reasoning in Executable Temporal Logic

Barringer H. and Gabbay D.: Executing temporal logic: Review and prospects (Extended Abstract). In Proceedings of Concurrency '88 1988.

Brzoska C., 1995, Executable Modal and Temporal Logics, volume 897 ofLecture Notes in Artificial Intelligence

10.1016/0167-6423(83)90017-5

Fisher M. and Barringer H.: Concurrent MetateM Processes — A Language for Distributed AI. In Proceedings of the European Simulation Multiconference Copenhagen Denmark June 1991.

Finger M., 1993, MetateM at Work: Modelling Reactive Systems Using Executable Temporal Logic

Fisher M.: A Normal Form for First-Order Temporal Formulae. In Proceedings of Eleventh International Conference on Automated Deduction (CADE) Saratoga Springs New York June 1992. (Published in Lecture Notes in Computer Science volume 607 Springer-Verlag).

Fisher M., 1993, Parallel Architectures and Languages, Europe (PARLE)

Fisher M.: A Survey of Concurrent MetateM — The Language and its Applications. In First International Conference on Temporal Logic (ICTL) Bonn Germany July 1994. (Published in Lecture Notes in Computer Science volume 827 Springer-Verlag).

Fujita M. Kono S. Tanaka T. and Moto-oka T.: Tokio: Logic Programming Language based on Temporal Logic and its compilation into Prolog. In 3rd International Conference on Logic Programming London July 1986. (Published in Lecture Notes in Computer Science volume 225 Springer-Verlag).

Finger M. McBrien P. and Owens R.: Databases and Executable Temporal Logic. In Proceedings of the ESPRIT Conference November 1991.

Fisher M., 1992, Technical Report UMCS-92-2-1

Fisher M. and Owens R.: From the Past to the Future: Executing Temporal Logic Programs. In Proceedings of Logic Programming and Automated Reasoning (LPAR) St. Petersberg Russia July 1992. (Published in Lecture Notes in Computer Science volume 624 Springer-Verlag).

Fisher M., 1995, Executable Modal and Temporal Logics, volume 897 ofLecture Notes in Artificial Intelligence

Fisher M. and Owens M.: editors. Executable Modal and Temporal Logics volume 897 of Lecture Notes in Artificial Intelligence. Springer-Verlag February 1995.

Frühwirth T., 1995, Executable Modal and Temporal Logics, volume 897 ofLecture Notes in Artificial Intelligence

Fisher M. and Wooldridge M.: Executable Temporal Logic for Distributed A.I. In Twelfth International Workshop on Distributed A.I. Hidden Valley Resort Pennsylvania May 1993.

Gabbay D.: Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In B. Banieqbal H. Barringer and A. Pnueli editors Proceedings of Colloquium on Temporal Logic in Specification Altrincham U.K. 1987. (Published in Lecture Notes in Computer Science volume 398 Springer-Verlag).

Gabbay D.: Modal and Temporal Logic II (A Temporal Prolog Machine). In T. Dodd R. Owens and S. Torrance editors Logic Programming—Expanding the Horizon. Intellect Books Ltd 1991.

Gough G. D.: Decision Procedures for Temporal Logic. Master's thesis Department of Computer Science University of Manchester October 1984.

Hale R., 1987, Temporal Logics and their Applications, chapter 3, 91

Hale R., 1987, Parallel Architectures and Languages Europe (PARLE), Eindhoven, The Netherlands

Hrycej T.: Temporal Prolog. In Yves Kodratoff editor Proceedings of the European Conference on Artificial Intelligence (ECAI). Pitman Publishing August 1988.

Hrycej T., 1993, A temporal extension of Prolog, The Journal of Logic Programming, 15, 113, 10.1016/0743-1066(93)90016-A

Jaffir J. and Lassez J-L.: Constraint Logic Programming. In Proceedings of the Fourteenth ACM Symposium on the Principles of Programming Languages pages 111–119 Munich West Germany January 1987.

10.1007/3-540-15648-8_16

Merz S., 1995, Executable Modal and Temporal Logics, volume 897 ofLecture Notes in Artificial Intelligence

Moszkowski B.: Reasoning about digital circuits. Technical report Stanford University 1983.

10.5555/6240

Manna Z. and Wolper P.: Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems 6(1) January 1984.

Noël P., 1991, A Method for the Determinisation of Propositional Temporal Formulae

Orgun M. and Ma W.: An Overview of Temporal and Modal Logic Programming. In First International Conference on Temporal Logic (ICTL) Bonn Germany July 1994. (Published in Lecture Notes in Computer Science volume 827 Springer-Verlag).

Orgun M. and Wadge W.: Theory and Practice of Temporal Logic Programming. In L Fariñas del Cerro and M. Penttonen editors Intensional Logics for Programming. Oxford University Press 1992.

Orgun M., 1992, Towards a unified theory of intensional logic programming, The Journal of Logic Programming, 13, 413, 10.1016/0743-1066(92)90055-8

Pnueli A. and Rosner R.: On the Synthesis of a Reactive Module. In Proceedings of the Sixteenth ACM Symposium on the Principles of Programming Languages (POPL) pages 179–190 1989.

Pnueli A. and Rosner R.: On the Synthesis of an Asynchronous Reactive Module. In Proceedings of the Sixteenth International Colloquium on Automata Languages and Programs (ICALP) 1989.

10.5555/67760.67764

Torsun I. S., 1990, Internal Report