The linear time-branching time spectrum

Abstract

In this paper eleven semantics in the linear time - branching time spectrum are presented in a uniform, modelindependenl way. Restricted to the domain of finitely branching, concrete, sequential processes, most semantics found in the literature that can be defined uniformly in terms of action relations coincide with one of these eleven. Several testing scenarios, motivating these semantics, are presented, phrased in terms of 'button pushing experiments' on generative and reactive machines. Finally nine of these semantics are applied to a simple language for finite, concrete, sequential, nondeterministic processes, and for each of them a complete axiomatization is provided.