Temporal and Modal Logics for Parallelism and security

A course by Markus Roggenbach and Lutz Schröder at the Universität Bremen 2001/2002.

Reactive systems admit descriptions in temporal logics by statements such as `coffee will eventually be dispensed after insertion of a coin'. The systems under consideration (not only coffee vending machines...) are regarded as black boxes: we are interested in their reactions to external input, rather than in their internal realization. The employed logics vary mostly with respect to the observations they rely on. For instance, one may assume that only events as such are recorded, or one may additionally regard causal relationships between events or the branching time between different system behaviours as observable. Underlying models of parallel computations are chosen accordingly.

Security policies, on the other hand, typically need to enforce properties such as `Victor cannot be left alone near the fridge', which may be conveniently expressed in certain modal logics. Here, the relevant system states are regarded as `possible worlds' in the sense of modal logic, each world allowing only a restricted set of actions.

The course will provide an introduction to several brands of such logics for parallelism and security, with the emphasis being on temporal logics. The practical usability of these methods will be demonstrated by example models both in the lectures and in the accompanying tutorials.

Slides

Author: Dr. Lutz Schröder

wg bkb

Last updated: November 27, 2002