TCCT : Timed Calculus with Controllable Timers

本発表では，時間付きプロセス計算系TCCT を導入する．本計算系がモデル化の対象としているのは，様々なイベントが発生する中においてイベントの発生時刻や種類等の履歴がその後の状況に重要な影響を及ぼしうるような現象を制御するための機構である．上記のような現象において重要な要素であるイベント発生時刻や発生後の経過時間といった発生イベントの時間に関する情報を扱うためには，1 つのプロセスに対して複数の時間に関する制約を精密に制御することが必要である．したがって，本計算系においては，プロセスに対してラベル付きタイマを付与することができ，各タイマをそのラベルを指定することで個別に制御することが可能である．多くのプロセス計算では，対象としているものすべてをプロセスで表現する．一般的に，時間付きシステムは巨大で非常に複雑であるため，それらを表現したプロセスも同じように巨大で複雑なものになる．しかしながら，TCCT では，そのようなシステムは，単にイベント発生源と見なされる．このことは考察対象の簡潔化に役立ち，結果として，扱うプロセスもより簡潔なものとなる．本発表では，単に本計算系を形式的な計算モデルとして論じるだけでなく，本計算系を用いてある認識デバイスを実装し，その実用性も示す．また，本計算系の数学的な性質として，プロセスのある適当なクラスに対して，通常の双模倣性（bisimulation）に基づいた等式が，任意の文脈において保たれることを示す．

A timed process calculus TCCT is introduced, to model computing mechanisms which deal with complicated time critical situations, where various events occur and each event occurrence can be affected by when and what events occurred so far. We often encounter this kind of phenomena, for which it seems signi?cant to introduce a formal computing model.Considering the nature of the model, it is crucial at which time points and with what time intervals events occur. In order to deal with such temporal information, it is necessary to nicely control multiple time constraints on a single process. Therefore we de?ne the process calculus TCCT so that a multiple number of labelled timers can be assigned to a single process and separately release each timer by referring to its label. In most conventional process calculi, it is assumed that everything in question can be described as processes, no matter how large the system is. There the main purpose of discussion is usually to analyse the ways of communication between such processes. In the real world, timed systems are very large and complicated, and, so are the processes which model them. In this calculus, however, such systems are considered only as an event generator, which is useful to simplify the situation and in the result to get simpler processes. This perspective is also a contribution of the calculus.In addition, in this paper we show the practical feasibility of the calculus by actually using TCCT to implement a certain recognising device, besides discussing the calculus merely as a formal computing model. Finally with regard to a mathematical property of the calculus, it is demonstrated that an equality based on the conventional bisimulation is preserved by all contexts for a reasonable class of processes.