学部後期課程
過去（2023年度）の授業の情報です
学内のオンライン授業の情報漏洩防止のため，URLやアカウント、教室の記載は削除しております。
最終更新日：2025年4月21日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
最終更新日：2025年4月21日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
応用数学XB
オートマトンと単項2階論理とモデル検査
命題の正しさは決定可能か。すなわち，理論を固定したとき，与えられた命題が正しいかどうかを機械的に判定できるか。1階論理で既に一般的には決定不可能である。しかし言語を限定すると決定可能になることがある。決定可能な例として1階論理のPresburger算術や単項2階論理のS1SおよびS2Sについて述べる。オートマトンや木オートマトンの性質に帰着することで証明される。関連する話題として時相論理のモデル検査問題について述べる。並列プロセス等の仕様を記述するための体系として時相論理はよく用いられる。与えられた状態遷移系において仕様の正しさを検証するのがモデル検査問題である。
Is the correctness of logical formulas decidable? Namely, we are concerned with the problem to mechanically decide whether a formula is correct in a fixed theory. This is generally undecidable at the level of first-order logic. However, there are decidable cases if the languages are restricted. Examples are Presburger arithmetic in first-order logic as well as S1S and S2S in monadic second-order logic. These are proved by reducing the problem to the properties of automata and tree automata. A related topic is the model checking problem in temporal logic, that is commonly used as frameworks to describe specifications, such as those of concurrent processes. The model checking problem involves the verification of correctness of specifications in a given state transition systems.
Is the correctness of logical formulas decidable? Namely, we are concerned with the problem to mechanically decide whether a formula is correct in a fixed theory. This is generally undecidable at the level of first-order logic. However, there are decidable cases if the languages are restricted. Examples are Presburger arithmetic in first-order logic as well as S1S and S2S in monadic second-order logic. These are proved by reducing the problem to the properties of automata and tree automata. A related topic is the model checking problem in temporal logic, that is commonly used as frameworks to describe specifications, such as those of concurrent processes. The model checking problem involves the verification of correctness of specifications in a given state transition systems.
時間割／共通科目コード
コース名
教員
学期
時限
0505098
FSC-MA4760L1
応用数学XB
長谷川 立
金曜2限
マイリストに追加
マイリストから削除
講義使用言語
日本語、英語
単位
2
実務経験のある教員による授業科目
NO
他学部履修
可
開講所属
理学部
授業計画
1階論理の例としてPresburger算術の決定可能性を示す。オートマトンに帰着することで証明される。2階論理の例としてS1SやS2Sの決定可能性を示す。S1Sの決定可能性を示すには無限語の上のオートマトンが必要になる。Buchiオートマトンやその他の無限語の上のオートマトンを扱う。S2Sの決定可能性を示すには無限木の上の木オートマトンが必要になる。パリティゲームと呼ばれる無限ゲームの決定性が鍵になる。関係した話題として時相論理のモデル検査問題について解説する。状態遷移系 (Kripke構造) の上で時相論理式が成り立つか判定する問題である。やはりゲームの決定性を用いて調べることができる。LTL・様相μ計算等の時相論理について述べる。
As an example of first-order theory, the decidability of Presburger arithmetic is shown. It is verified by reduction to automata. For the second-order logic, the decidability of S1S and S2S is shown. To proved the former, automata over infinite words are necessary. Buchi automata and other types of automata over infinite words are introduced. For S2S, tree automata over infinite trees are necessary. A key for verification is the determinacy of infinite games called parity games. The model checking problem of temporal logic is also explained. This is the problem to decide whether a given formula is correct in a state transition system (Kripke structure). It is verified also via determinacy of games. Several systems of temporal logic are discussed, including LTL and modal mu-calculus.
授業の方法
講義による。留学生がいる場合は日本語・英語で行う（両方で説明するという意味）。
If foreign students are enrolled in the course, the lectures will be conducted in both of Japanese and English.
成績評価方法
レポートによる
教科書
特に指定しない。
参考書
田中一之「計算理論と数理論理学」（共立出版）
履修上の注意
講義中にある程度解説するが，オートマトンやTuring機械や計算複雑性についての基礎は知っていた方がわかりやすいだろう。
