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

摘要

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.