Por Que Esto?

Technical Report IR-353, Faculty of Mathematics and Computer Science, Vrije Universiteit Amsterdam

Relating Linear and Branching Time
Temporal Models*
Joeri Engelfriet and Jan Treur
Free University Amsterdam,
Department of Mathematics and Computer Science
De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands
Email: {joeri,treur}@cs.vu.nl

1

Introduction

Temporal logic providestechniques to build formal models of dynamics: processes are
described by temporal models that satisfy some set of temporal axioms. This approach may
be used to describe the dynamics of (material) processes in the external world, as well as
mental or computational processes. In our research we focus on formal models for the
behaviour of (interactive) complex reasoning systems by means oftemporal logic. States in
a reasoning system are characterized by the (incomplete) information that has been obtained
so far; usually they are called information states.
The world the system is reasoning about can be described using a language, called the
object-level language. The information states are formalized by models of the object-level
language together with a satisfaction relation whichdescribes which formulae are true in a
particular information state (object-level model). We do not a priori pose any restrictions on
the language or the models. A behavioural pattern of such a reasoning system can be
described by a sequence of information states, formalized by a temporalized model. This has
led us to the introduction of temporalized logic in which (two-valued) temporaloperators are
applied to object-level formulae to describe their truth over time.
A characteristic of dynamics is that there is often a number of possible alternative
behavioural patterns. During the process in some way or another a choice between these
alternatives is made. These (intended) behavioural patterns can be formalized by a set of
* This work has been carried out in the context of SKBSand the ESPRIT III Basic Research project 6156

DRUMS II.

1

Technical Report IR-353, Faculty of Mathematics and Computer Science, Vrije Universiteit Amsterdam

possible (intended) linear time temporal models of the temporal theory involved. A slightly
different way of formalization of the variety of patterns is by one branching time temporal
model of a temporal theory, where each branchrepresents one of the patterns.
Formalization by a set of linear time models has the advantage of a very simple model
structure. But the disadvantage is that the possible choices and the time points at which they
should be made are not covered explicitly in the formalization itself. Branching time models
represent these choices as points where the flow of time branches. Given that both thelinear
time and branching time approach are formalizations of (more or less) the same
phenomenon, it is natural to study formal connections between the two approaches.
Examples of natural questions that arise are:
(a) Is there a clear connection between the semantic consequence relation based on linear
time models and the one based on branching time models ?
(b) Can a correspondence beestablished between linear time temporal theories and
branching time theories ?
(c)

Are there interesting classes of temporal theories for which any branch of a
branching time model is a linear time model of the (or a corresponding) theory?

(d) Is there a universal (algebraic) construction of a branching time model out of any set
of linear time models ?
(e) Are interesting classes of temporalformulae persistent under such a construction ?
(f) Is each branching time model the result of such a construction ?
(g) Given a temporal theory, is there a branching time model that contains all other
models as submodels (final model) ?
This paper introduces (general) temporalized logic (similar to [6]) and discusses answers on
these questions for this logic. It turns out that the answers...