Event Entry
What and Who
Logic, Bisimulations and Processes
Date, Time and Location
Abstract
behavior, or processes, and thus form a research field of common interest
to logicians and theoretical computer scientists. Roughly speaking,
LTSs are graph-like structures. A bisimulation between them is
a relation connecting states from both structures so as to mimic
steps that can be made in one state by steps from the other state,
in such a way that the resulting states are again in the relation.
Process algebra studies concurrent (communicating) processes in an
algebraic fashion. Atomic actions, algebraic operations and equational
axioms are used to study processes. Typically, a distributed system or
concurrent protocol can be described as the concurrent execution of a
number of elementary subprocesses, possibly employing communication.
LTSs provide convenient models of processes. Process algebra axioms
induce various notions of equivalence between processes, including
bisimulations.
In modal logic LTSs are known under the name of Kripke models. Here,
bisimulations enter the picture as truth-preserving relations between
models: bisimilar systems satisfy the same modal formulas. Modal languages
are uniquely identified by the fact that there formulas are preserved by
bisimulations.
In the talk I will survey the basic theory underlying the various
algebraic and logical approaches to LTSs and bisimulations, and discuss
connections between the approaches.
Contact