[logic-ml] Sendai Logic Workshop のご案内

[higurashi3873 at yahoo.co.jp]

Logic-ml $B$N3'MM!$(B

$B$3$s$P$s$O!$ElKLBg3X$NKYH*2B9($G$9!%(B
$B2<5-$NMWNN$G!$ElKLBg3X!JEDCf0lG78&!K$K$F8&5f2q$r9T$$$^$9$N$G!$6=L#$N$"$kJ}$O$<$R$4;22C$/$@$5$$!%(B
$B;09V1i$4$6$$$^$9!%(B

*************************************************************************
Sendai Logic Workshop

$BF|;~!'(B6$B7n(B1$BF|!J6b!K(B14:00$B!A(B17:30
$B>l=j!'ElKLBg3X(B $BKL at DMU;3%-%c%s%Q%9(B $BM}3X9gF1Eo(B 1201$B9f<<(B


$B-!(B14:00$B!A(B15:00
$B9V1i<T!'</Eg(B $BN<(B $B!JEl5~9)6HBg3XBg3X1!(B $B>pJsM}9)3X8&5f2J!K(B
$B%?%$%H%k!'(BCTL$B$H<~JU$NO at M}$N8xM}2=$K$D$$$F(B

$B%"%V%9%H%i%/%H!'(B
Computation Tree Logic (CTL) $B$O!$;~4V$N?d0\$KH<$C$F>uBV$,JQ2=$9$k%7%9%F%`$N5-=R$KMQ$$$i$l$kMMAjO at M}!J;~AjO at M}!K$NBeI=$G$"$k!#(B
$BK\9V1i$NL\E*$O!$(BCTL$B$H$=$N<~JU$NO at M}$KBP$9$k%R%k%Y%k%HN.8xM}2=$H40A4 at -$K$D$$$F=iJb$+$i2r at b$7!$9V1i<T$N:G6a$N;E;v!J(BECTL$B$N8xM}2=!K$d<h$jAH$_$?$$LdBj!JMMAj&L7W;;$N40A4 at -$NJL>ZL@!K$K$D$$$F at bL@$9$k$3$H$G$"$k!#(B
$BM=HwCN<1$O8EE5L?BjO at M}$N40A4 at -DjM}DxEY$G==J,$NM=Dj!#(B




$B-"(B15:15$B!A(B16:15
$B9V1i<T!':,85(B $BB?2B;R(B $B!JKLN&@hC<2J3X5;=QBg3X1!Bg3X(B $B>pJs2J3X8&5f2J!K(B
$B%?%$%H%k!'(BWadge $B%2!<%`$N%P%j%(!<%7%g%s$H(B Wadge $B3,AX(B

$B%"%V%9%H%i%/%H!'(B
Wadge [3] $B$K$h$jDj5A$5$l$?(B Wadge $B3,AX$OO"B34X?t$K$h$k5UA|$K$D$$$FJD$8$?%/%i%9$N at .$93,AX$G!"(BBorel $B3,AX$d(B
Hausdorff $B$N=89g:9$K$h$k3,AX$h$j$b$h$j:Y$+$$=89g$N3,AX$rM?$($k!#(B
$B$3$N3,AX$N3F%/%i%9$N=89gA`:n$K$h$k5-=R$O(B Louveau [2] $B$K$h$jM?$($i$l$?$,!"(B $BHs>o$KHQ;($G$"$k!#(B
Wadge $B3,AX$G??$KF1$8<!?t$r$b$D=89g$O(B Wadge $B%2!<%`$K$h$jFCD'$E$1$i$l$k$,!"(BDuparc [1]
$B$G$O$3$N%2!<%`$N%P%j%(!<%7%g%s$K$h$j(B Wadge $B%/%i%9$N<!?t$N5-=R$N4JN,2=$rM?$((B
$B$F$$$k!#(B
$BK\9V1i$G$O(B [1] $B$NFbMF$rCf?4$K!"(BWadge $B%2!<%`$H(B Wadge $B3,AX$K4X$9$k8&5f$r>R2p$9$k!#(B

$B;29MJ88%!'(B
[1] J. Duparc, Wadge Hierarchy and Veblen Hierarchy. Part I: Borel
Sets of Finite Rank. Journal of Symbolic Logic 66(1), pp. 56-86, 2001
[2] A. Louveau, Some results in the Wadge hierarchy of Borel sets,
Cabal seminar 79-81, Lecture
Notes in Mathematics, vol. 1019, Springer Verlag, 1983, pp. 28-55.
[3] W.W. Wadge, Reducibility and determinateness on the Baire space.,
Ph.D. thesis, Berkeley, 1984.




$B-#(B16:30$B!A(B17:30
$B9V1i<T!'O!Hx(B $B0lO:(B $B!JEl5~Bg3XBg3X1!(B $B>pJsM}9)3X7O8&5f2J!K(B
$B%?%$%H%k!'(BProgramming with Infinitesimals: A While-Language for Hybrid
System Modeling
(Joint Work with Kohei Suenaga, Kyoto University)

$B%"%V%9%H%i%/%H!'(B
We add, to the common combination of a WHILE-language and a
Hoare-style program logic, a constant dt that represents an
infinitesimal (i.e. infinitely small) value. The outcome is a
framework for modeling and verification of hybrid systems: hybrid
systems exhibit both continuous and discrete dynamics and getting them
right is a pressing challenge. We rigorously define the semantics of
programs in the language of nonstandard analysis, on the basis of
which the program logic is shown to be sound and relatively complete.
If the time allows, our recent prototype automatic prover will also be
demonstrated.

$B;29MJ88%!'(B
Kohei Suenaga and Ichiro Hasuo.
Programming with Infinitesimals: A While-Language for Hybrid System Modeling.
Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.

*************************************************************************


$B0J>e$G$9!%(B
$B%;%_%J!<>pJs$O2<5- at gBf%m%8%C%/$N%[!<%`%Z!<%8$+$i$b$4Mw$$$?$@$1$^$9!%(B
https://sites.google.com/site/sendailogichomepage/

$BKYH*!!2B9((B
-- --
$BElKLBg3XBg3X1!!!M}3X8&5f2J(B
$B?t3X at l96!!;:3X41O"7H8&5f0w(B
E-mail: higurashi3873 at yahoo.co.jp