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@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@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@M}!J;~AjO@M}!K$NBeI=$G$"$k!#(B $BK\9V1i$NL\E*$O!$(BCTL$B$H$=$N<~JU$NO@M}$KBP$9$k%R%k%Y%k%HN.8xM}2=$H40A4@-$K$D$$$F=iJb$+$i2r@b$7!$9V1i<T$N:G6a$N;E;v!J(BECTL$B$N8xM}2=!K$d<h$jAH$_$?$$LdBj!JMMAj&L7W;;$N40A4@-$NJL>ZL@!K$K$D$$$F@bL@$9$k$3$H$G$"$k!#(B $BM=HwCN<1$O8EE5L?BjO@M}$N40A4@-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@.$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-@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@l96!!;:3X41O"7H8&5f0w(B E-mail: [email protected]