Time-extraction for temporal logic-logic programming and local process time

Research output: Contribution to journalArticle

Abstract

Temporal logic is useful to describe a variety of computer systems such as operating systems and real-time process control systems, where explicit treatment of time plays an essential role. In the logic, the notion of time is represented by a sequence of states at each point in time, which is called a time stream. In distributed environments, it can allow simple descriptions of processes to deal with each process as if it had its own proper time stream where a proper time stream, called an extracted time stream, consists of the events which are essential to the process and are extracted from the original universal time stream. It is proved that, for given formulas which are interpreted in one of the extracted time streams, there exist certain formulas such that they are interpreted in the universal time stream and are equivalent to the given formulas. This time-extraction is applied to the temporal prolog in order to decompose a program into pieces, each of which works in its own time stream. In the same way as logical formulas, a program with time-extraction can be transformed to an equivalent program without time-extraction. It is also proved that the transformations preserve equivalence in the sense of model-theoretic semantics.

Original languageEnglish
Pages (from-to)40-56
Number of pages17
JournalJournal of Computer and System Sciences
Volume49
Issue number1
DOIs
Publication statusPublished - 1994
Externally publishedYes

Fingerprint

Temporal logic
Logic programming
Temporal Logic
Logic Programming
Computer operating systems
Process control
Computer systems
Semantics
Control systems
Equivalence Transformations
Prolog
Distributed Environment
Process Control
Operating Systems

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Time-extraction for temporal logic-logic programming and local process time. / Hattori, Takashi.

In: Journal of Computer and System Sciences, Vol. 49, No. 1, 1994, p. 40-56.

Research output: Contribution to journalArticle

@article{b52a11fe039746b8b5d34712ecf8224a,
title = "Time-extraction for temporal logic-logic programming and local process time",
abstract = "Temporal logic is useful to describe a variety of computer systems such as operating systems and real-time process control systems, where explicit treatment of time plays an essential role. In the logic, the notion of time is represented by a sequence of states at each point in time, which is called a time stream. In distributed environments, it can allow simple descriptions of processes to deal with each process as if it had its own proper time stream where a proper time stream, called an extracted time stream, consists of the events which are essential to the process and are extracted from the original universal time stream. It is proved that, for given formulas which are interpreted in one of the extracted time streams, there exist certain formulas such that they are interpreted in the universal time stream and are equivalent to the given formulas. This time-extraction is applied to the temporal prolog in order to decompose a program into pieces, each of which works in its own time stream. In the same way as logical formulas, a program with time-extraction can be transformed to an equivalent program without time-extraction. It is also proved that the transformations preserve equivalence in the sense of model-theoretic semantics.",
author = "Takashi Hattori",
year = "1994",
doi = "10.1016/S0022-0000(05)80085-6",
language = "English",
volume = "49",
pages = "40--56",
journal = "Journal of Computer and System Sciences",
issn = "0022-0000",
publisher = "Academic Press Inc.",
number = "1",

}

TY - JOUR

T1 - Time-extraction for temporal logic-logic programming and local process time

AU - Hattori, Takashi

PY - 1994

Y1 - 1994

N2 - Temporal logic is useful to describe a variety of computer systems such as operating systems and real-time process control systems, where explicit treatment of time plays an essential role. In the logic, the notion of time is represented by a sequence of states at each point in time, which is called a time stream. In distributed environments, it can allow simple descriptions of processes to deal with each process as if it had its own proper time stream where a proper time stream, called an extracted time stream, consists of the events which are essential to the process and are extracted from the original universal time stream. It is proved that, for given formulas which are interpreted in one of the extracted time streams, there exist certain formulas such that they are interpreted in the universal time stream and are equivalent to the given formulas. This time-extraction is applied to the temporal prolog in order to decompose a program into pieces, each of which works in its own time stream. In the same way as logical formulas, a program with time-extraction can be transformed to an equivalent program without time-extraction. It is also proved that the transformations preserve equivalence in the sense of model-theoretic semantics.

AB - Temporal logic is useful to describe a variety of computer systems such as operating systems and real-time process control systems, where explicit treatment of time plays an essential role. In the logic, the notion of time is represented by a sequence of states at each point in time, which is called a time stream. In distributed environments, it can allow simple descriptions of processes to deal with each process as if it had its own proper time stream where a proper time stream, called an extracted time stream, consists of the events which are essential to the process and are extracted from the original universal time stream. It is proved that, for given formulas which are interpreted in one of the extracted time streams, there exist certain formulas such that they are interpreted in the universal time stream and are equivalent to the given formulas. This time-extraction is applied to the temporal prolog in order to decompose a program into pieces, each of which works in its own time stream. In the same way as logical formulas, a program with time-extraction can be transformed to an equivalent program without time-extraction. It is also proved that the transformations preserve equivalence in the sense of model-theoretic semantics.

UR - http://www.scopus.com/inward/record.url?scp=0028482493&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0028482493&partnerID=8YFLogxK

U2 - 10.1016/S0022-0000(05)80085-6

DO - 10.1016/S0022-0000(05)80085-6

M3 - Article

VL - 49

SP - 40

EP - 56

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

SN - 0022-0000

IS - 1

ER -