$B3'MM!"(B

$B:#=5$N?eMK!J#57n#2#5F|!K$K!"5~ETBg3X?tM}2r@O8&5f=j$G0J2<$NCLOC2q$,3+:E(B $B$5$l$^$9!#9V1i<T$O!"8=:_5R0w65<x$H$7$F?tM}8&$KBZ:_$5$l$F$$$k!"%"%`%9%F(B $B%k%@%`Bg$N(BYde Venema$B$5$s$G$9!#$I$&$>$4MhD0$/$@$5$$!#(B

$BD9C+@n???M(B $B5~ETBg3X?tM}2r@O8&5f=j(B --

$BCLOC2q$N$40FFb(B

$BF|;~(B: $B!!(B5$B7n(B 25$BF|(B($B?e(B) 16:30-17:30 $B>l=j(B: $B!!?tM}8&(B110$B9f<<(B (16:00$B$h$j(B1$B3,%m%S!<$G(Btea) $B9V1i<T(B: Yde Venema $B;a(B $B=jB0(B: $B!!5~Bg!&?tM}8&(B & University of Amsterdam

$BBjL\(B: Coalgebra, its Logic, and some of its Mathematical Environments

Abstract: Computers and other electronic equipment are becoming more and prominent, both in our daily life, and in society as a whole. When we are confronted with undesired or incomprehensible behavior of for instance our mobile phone, we will naively start reasoning about the system, modelling it as a state-based evolving system, that we can only observe as a black box. Clearly, when it comes to specifying and reasoning about the behavior of critical software systems, a sophisticated mathematical theory is needed.

The theory of coalgebra, which has emerged from theoretical computer science in the last two decades, provides a general, mathematical framework for reasoning about such state-based evolving systems. It combines mathematical simplicity with wide applicability, due to its categorical foundations: many features such as input/output, nondeterminism, probability, and interaction can be encoded in the coalgebraic type which formally is a functor over Set (or some other base category). Coalgebra allows us to give precise mathematical definitions of notions such as behavior or observational equivalence of systems. Logic naturally enters the picture since we want to specify and reason about behavior in a formal way.

In the talk, we will give a very informal introduction and motivation of coalgebra and coalgebraic logic. We then briefly explain the dualities between algebra and coalgebra, and discuss the principle of coinduction. In the second part of the talk we describe some of the mathematical environments of the theory, and sketch how ideas from coalgebraic logic can be used to generalize results in topology (the Vietoris construction) and automata theory (Rabin's Theorem).

$BCLOC2q$N0FFb!'(B http://www.kurims.kyoto-u.ac.jp/ja/seminar/danwakai.html

$B?tM}2r@O8&5f=j$X$N%"%/%;%9!'(B http://www.kurims.kyoto-u.ac.jp/ja/access-01.html

--