More Web Proxy on the site http://driver.im/

article

Framed temporal logic programming

Authors:

Maciej KoutnyAuthors Info & Claims

Science of Computer Programming, Volume 70, Issue 1

Pages 31 - 61

https://doi.org/10.1016/j.scico.2007.09.001

Published: 01 January 2008 Publication History

Abstract

A Projection Temporal Logic is discussed and some of its laws are given. After that, an executable temporal logic programming language, called Framed Tempura, is formalized. A minimal model-based approach for framing in temporal logic programming is presented. Since framing destroys monotonicity, canonical models-used to define the semantics of non-framed programs-are no longer appropriate. To deal with this, a minimal model theory is developed, using which the temporal semantics of framed programs is captured. The existence of a minimal model for a given framed program is demonstrated. A synchronous communication mechanism for concurrent programs is provided by means of the framing technique and minimal model semantics.

References

[1]

Barringer, H., Fisher, M., Gabbay, D., Gough, G. and Owens, R., METATEM: A framework for programming in temporal logic. In: LNCS, vol. 430. Springer-Verlag.

[2]

Bidoit, N., Negation in rule-based data base languages: A survey. Theoretical Computer Science. v78. 3-83.

[3]

Bowman, H., Cameron, H., King, P. and Thompson, S., Specication and prototyping of structrued multimedia documents using interval temporal logic. In: Applied Logic Series, Kluwer.

[4]

Bowman, H. and Thompson, S., A Tableau method for interval temporal logic with projection. In: LNAI, vol. 1397. Springer-Verlag.

[5]

Bowman, H. and Thompson, S., A decision procedure and complete axiomatisation of finite interval temporal logic with projection. Journal of Logic and Computation. v13. 195-239.

[6]

Z. Duan, An extended interval temporal logic and a framing technique for temporal logic programming, Ph.D. Thesis, University of Newcastle upon Tyne, 1996

[7]

Duan, Z., Temporal Logic and Temporal Logic Programming. 2006. ISBN:7-03-016651-5/TP.3158. Science Press, Beijing.

[8]

Duan, Z., Holcombe, M. and Bell, A., A logic for biological systems. BioSystems. v55. 93-105.

[9]

Duan, Z. and Koutny, M., A framed temporal logic programming language. Journal of Computer Science and Technology. v19. 341-351.

[10]

Duan, Z., Koutny, M. and Holt, C., Projection in temporal logic programming. In: Pfenning, F. (Ed.), LNAI, vol. 822. Springer-Verlag. pp. 333-344.

[11]

Duan, Z., Yang, X. and Koutny, M., Semantics of framed temporal logic programs. In: LNCS, vol. 3668. Springer-Verlag. pp. 356-370.

Digital Library

[12]

Emerson, E.A. and Clarke, E.M., Using branching temporal logic to synthesize synchronization skeletons. Science of Computer Programming. v2. 241-266.

[13]

Fisher, M., Towards a semantics for concurrent MTETATEM. In: LNAI, vol. 897. Springer-Verlag.

[14]

Fujita, M., Kono, S., Tanaka, H. and Moto-oka, T., Tokio: Logic programming language based on temporal logic and its compilation to PROLOG. In: LNCS, vol. 225. Springer-Verlag. pp. 695-709.

[15]

D.M. Gabbay, Theoretical foundations for non-monotonic reasoning in expert systems, Research Report 84/11, Dept. of Computing, Imperial College, 1984

[16]

R.W.S. Hale, Programming in temporal logic, Ph.D. Thesis, Cambridge University, 1988

[17]

A practical theory of programming. Science of Computer Programming. v14. 133-158.

[18]

Hoare, C.A.R., Communicating Sequential Processes. 1985. Prentice Hall International.

[19]

Kroger, F., Temporal Logic of Programs. 1987. Springer-Verlag.

[20]

Lamport, L., The temporal logic of actions. ACM Transaction on Programming Languages and Systems. v16.

[21]

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

[22]

Milner, R., Communication and Concurrency. 1989. Prentice Hall.

[23]

Moszkowski, B., Executing Temporal Logic Programs. 1986. Cambridge University Press.

[24]

Moszkowski, B., Some very compositional temporal properties. In: Programming Concepts, Methods and Calculi, Elsevier Science B.V., North-Holland. pp. 307-326.

[25]

L. Ness, L.0: A parallel executable temporal logic language, in: Proceeding of ACM SIGSOFT, International Workshop on Formal Methods in Software Development, 1990

[26]

Tang, C.S., Toward a unified logic basis for programming languages. In: Proceedings of IFIP Congress, Elsevier Science Publishers B.V., North-Holland. pp. 425-429.

[27]

Tang, C.S., A temporal logic language oriented toward software engineering,¿introduction to XYZ system (I). Chinese Journal of Advanced Software Research. v1. 1-27.

Cited By

Chen YShu X(2023)Formal verification of eBPF program security based on PTLProceedings of the 2023 6th International Conference on Artificial Intelligence and Pattern Recognition10.1145/3641584.3641768(1225-1230)Online publication date: 22-Sep-2023
https://dl.acm.org/doi/10.1145/3641584.3641768
Jia YShu X(2022)Visual Model Checking Distributed SystemProceedings of the 2022 5th International Conference on Artificial Intelligence and Pattern Recognition10.1145/3573942.3574023(285-291)Online publication date: 23-Sep-2022
https://dl.acm.org/doi/10.1145/3573942.3574023
Feng XZhang NDuan Z(2022)Implementation of Matlab matfun Toolkit Based on MSVLStructured Object-Oriented Formal Language and Method10.1007/978-3-031-29476-1_4(53-58)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-29476-1_4
Show More Cited By

Index Terms

Framed temporal logic programming

Recommendations

Semantics of framed temporal logic programs
ICLP'05: Proceedings of the 21st international conference on Logic Programming

This paper investigates semantics of framed temporal logic programs. To this end, a projection temporal logic and its executable subset are presented. Based on this language, a framing technique is introduced. The semantics of a non-framed program is ...
A framed temporal logic programming language
Abstract
We discuss the projection temporal logic (PTL), based on a primitive projection operator,prj. A framing technique is also presented, using which a synchronization operator,await, is defined within the underlying logic. A framed temporal logic ...
Logical foundations for more expressive declarative temporal logic programming languages

In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logic programming. TeDiLog is, syntactically, a sublanguage of the well-known ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Science of Computer Programming

Science of Computer Programming Volume 70, Issue 1

January, 2008

87 pages

ISSN:0167-6423

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2007.

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 01 January 2008

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chen YShu X(2023)Formal verification of eBPF program security based on PTLProceedings of the 2023 6th International Conference on Artificial Intelligence and Pattern Recognition10.1145/3641584.3641768(1225-1230)Online publication date: 22-Sep-2023
https://dl.acm.org/doi/10.1145/3641584.3641768
Jia YShu X(2022)Visual Model Checking Distributed SystemProceedings of the 2022 5th International Conference on Artificial Intelligence and Pattern Recognition10.1145/3573942.3574023(285-291)Online publication date: 23-Sep-2022
https://dl.acm.org/doi/10.1145/3573942.3574023
Feng XZhang NDuan Z(2022)Implementation of Matlab matfun Toolkit Based on MSVLStructured Object-Oriented Formal Language and Method10.1007/978-3-031-29476-1_4(53-58)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-29476-1_4
Wang JZhang NDuan Z(2022)Three Algorithms for Converting Control Flow Statements from Python to XD-MAlgorithmic Aspects in Information and Management10.1007/978-3-031-16081-3_40(456-465)Online publication date: 13-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-16081-3_40
Wang YZhang NDuan Z(2021)Design and Implementation of List and Dictionary in XD-M LanguageAlgorithmic Aspects in Information and Management10.1007/978-3-030-93176-6_29(344-355)Online publication date: 20-Dec-2021
https://dl.acm.org/doi/10.1007/978-3-030-93176-6_29
Shu XWang ZGao WWang XZhao L(2020)An MSVL Based Model Checking Method for Multi-threaded C ProgramsStructured Object-Oriented Formal Language and Method10.1007/978-3-030-77474-5_7(88-101)Online publication date: 1-Mar-2020
https://dl.acm.org/doi/10.1007/978-3-030-77474-5_7
Yu BLu XChen HLei MWang X(2020)Runtime Verification of Ethereum Smart Contracts Based on MSVLStructured Object-Oriented Formal Language and Method10.1007/978-3-030-77474-5_10(142-153)Online publication date: 1-Mar-2020
https://dl.acm.org/doi/10.1007/978-3-030-77474-5_10
Zhao LFeng ZWang XShu X(2020)An MSVL-Based Modeling Framework for Back Propagation Neural NetworksStructured Object-Oriented Formal Language and Method10.1007/978-3-030-77474-5_1(3-22)Online publication date: 1-Mar-2020
https://dl.acm.org/doi/10.1007/978-3-030-77474-5_1
Wang MTian CZhang NDuan ZDu H(2019)Verifying a scheduling protocol of safety-critical systemsJournal of Combinatorial Optimization10.1007/s10878-018-0343-137:4(1191-1215)Online publication date: 1-May-2019
https://dl.acm.org/doi/10.1007/s10878-018-0343-1
Yu BLiu JLei MYu YChen H(2019)Parallel Runtime Verification Approach for Alternate Execution of Multiple ThreadsStructured Object-Oriented Formal Language and Method10.1007/978-3-030-41418-4_8(99-109)Online publication date: 5-Nov-2019
https://dl.acm.org/doi/10.1007/978-3-030-41418-4_8
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents