TY - JOUR

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

AU - Hattori, Takashi

PY - 1994/8

Y1 - 1994/8

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

AN - SCOPUS:0028482493

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 -