| A Logic for Signal Inserted Timed Frames (1996) | |||||||||||||||
Abstract | |||||||||||||||
| We propose a first-order predicate logic TFL of timed frames extended with signals. This logic combines a simple syntax with a high expressivity; it can distinguish frames that are not the same as sets of transitions and states. We show how Dicky logic and CTL can be embedded in TFL. 1 Introduction In recent years, a multitude of process algebras have evolved. Bergstra and Ponse [8, 9] proposed to study basic properties of such process algebras on the level of frames, which are labelled, directed graphs. Essentially, frames are transition systems without explicit start and termination nodes. Frames can be converted into processes by means of process extraction, which means that two states are singled out, which represent the start state and the successful termination state respectively. Thus, the algebra of frames constitutes a common platform for the study of basic properties of process algebras. In [7], frames have been extended with discrete time, following [4], and with signals, ... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||