ファイル置き場 Sendai Logic Homepage Program 0601

(1)

Sendai Logic Workshop

日時 ₂₀₁₂年₆月₁日（金）_14:00∼_17:30 ＊_19:00から懇親会場所東北大学大学院理学研究科理学合同棟₁₂₀₁

第一講演（_14:00∼_15:00）

CTLと周辺の論理の公理化について鹿島亮

（東京工業大学大学院情報理工学研究科）

アブストラクト Computation Tree Logic (CTL)は，時間の推移に伴って状態が変化するシステムの記述に用いられる様相論理（時相論理）の代表である。本講演の目的は，_CTLとその周辺の論理に対するヒルベルト流公理化と完全性について初歩から解説し，講演者の最近の仕事（_ECTLの公理化）や取り組みたい問題（様相μ 計算の完全性の別証明）について説明することである。予備知識は古典命題論理の完全性定理程度で十分の予定。

第二講演（_15:15∼_16:15）

Wadgeゲームのバリエーションと_Wadge階層根元多佳子

（北陸先端科学技術大学院大学情報科学研究科）

アブストラクト _{Wadge (3)}により定義された_Wadge階層は連続関数による逆像について閉じたクラスの成す階層で、_Borel階層や_Hausdorffの集合差による階層よりもより細かい集合の階層を与える。この階層の各クラスの集合操作による記述はLouveau (2)により与えられたが、非常に煩雑であ

る。_Wadge階層で真に同じ次数をもつ集合は_Wadgeゲームにより特徴づけられるが、_{Duparc (1)}

ではこのゲームのバリエーションにより_Wadgeクラスの次数の記述の簡略化を与えている。本講演では₍₁₎の内容を中心に、_Wadgeゲームと_Wadge階層に関する研究を紹介する。

参考文献：

(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.

1

(2)

第三講演（_16:30∼_17:30）

Programming with Infinitesimals: A While-Language for Hybrid System Modeling

(Joint Work with Kohei Suenaga, Kyoto University) 蓮尾一郎

（東京大学大学院情報理工学系研究科）

アブストラクト 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. References:

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.

2