|Time:|| 12 - 1:20 p.m.
|Speaker:|| Uri Abraham
Department of Computer Science
Ben-Gurion University of the Negev
Department of Mathematical Sciences
Carnegie Mellon University
A standard approach to model concurrency uses the notions of ``state'' and
``history'' to describe behaviors of embedded systems (which comprise
several processes that operate independently). Then state formulas and
temporal logic is used to specify and to argue about such systems. This
approach is very useful (e.g. for model checking) and has found many
applications. We present, however, a different approach in which the
notion of ``event'' rather than ``state'' is primary. Our models are the
standard ``Tarskian'' models that mathematical logicians usually
employ --- namely structures consisting of a universe, relations, and
functions. To motivate our approach we describe a simple Cache coherence
protocol. We will argue that the specification of this protocol finds a
more natural expression within such Tarskian structures.
|Organizer's note:|| Please bring your lunch.