-------------------------------------------------

■日時: 2010年10月27日（水）15:00〜16:00
■場所: 南山大学瀬戸キャンパスH棟1階H-104教室
■講演者：Irek Ulidowski (Senior Lecturer)University of Leicester, UK
研究分野：Models of Reversible Computation, Process Calculi, Structured Operational　Semantics, Modelling in Ubiquitous Computing, Operational semantics for Service Oriented Computing, Term Rewriting
　　http://www.cs.le.ac.uk/people/iu3/
■講演題目: Reverse Bisimulations on Stable Event Structures
■アブストラクト:
Most of the equivalences in the theory of concurrency are defined for
systems that typically compute only forward. If one assumes that the
systems can equally execute forward and in the reverse direction, such as
for example bio-chemical systems, then the standard equivalences and results
(for the forward only computation) can be extended naturally by taking reverse
computation into account. In this talk we shall consider stable event
structures as the model for forward/reverse computation and equivalences on
such event structures.

The relationships between various equivalences on stable event structures,
including interleaving bisimulation (IB), step bisimulation (SB) and
hereditary history-preserving (HH) bisimulation, have been investigated by
van Glabbeek and Goltz. Since HH bisimulation may be characterised by
the use of reverse as well as forward transitions, it is of interest to
investigate forms of IB and SB (and other more complex bisimulations)
where both forward and reverse transitions are allowed.

Bednarczyk asked whether SB with reverse steps (which we shall call reverse
SB and write RSB) is as strong as HH bisimulation. This question remained
open until very recently. We give various characterisations of RSB, showing
that forward steps do not add extra power. We strengthen Bednarczyk's
result that, in the absence of auto-concurrency, reverse IB is as strong as
HH bisimulation, by showing that we need only exclude auto-concurrent
events at the same depth in the configuration.

Finally, we present a lattice of many forms of bisimulations where both
forward and reverse observations are allowed. The lattice has HH at the top
and IB at the bottom, and we briefly explain the relationships between
other forms of bisimulations.

■お問合せ先
南山大学
情報理工学部 ソフトウェア工学科 講師　横山哲郎（tetsuo@nanzan-u.ac.jp）
情報理工学部事務室（suuri-common@nanzan-u.ac.jp）

以上