授業の目的 【日本語】
Goals of the Course(JPN) | | 本講義では、並行計算の形式体系であるMilnerのCCSについて学ぶ。CCSの操作的意味論は
通信から観測される双模倣等価性として定式化される。この等価性がCCSの演算子に関して
保存されることが示される。さらに、同期通信テストに基づく操作意味論の統一的な枠組みについて
示す。 |
|
|
授業の目的 【英語】
Goals of the Course | | This course discusses the process calculi that have been studied to
formulate concurrency, mainly focusing on Milner’s CCS (Calculus for
Communicating Systems). The operational semantics is understood as
the bisimularity of communication capability. CCS is shown to hold
algebraic properties with respect to its operations. We further
discuss the testing charcterization of concurrent systems as a uniform framework
to identify concurrent behavior. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | 並行計算を表現する通信プロセス計算の体系について習得する。
並行計算では、非決定的で非停止の振る舞いが意味を持つ。
このような計算体系においてはオートマトンのような受理言語では
振る舞いを定式化できない。同期テストという観点で並行システムの
振る舞いをどのように特徴づけられるかについて学ぶ。 |
|
|
到達目標 【英語】
Objectives of the Course | | This lecture provides a calculus for concurrent systems.
In concurrency, nondeterminism and nontermination are quite common
where interactions with the environment shall be used for operational
characterization. We see that the testing framework explains various
operational semantics to exhibit the nice algebraic properties. |
|
|
授業の内容や構成
Course Content / Plan | | 並行計算をラベル付き遷移システムとしてモデル化する。
複数のラベル付き遷移システムがラベルの同期による相互作用を及ぼしながら計算が進行する。
並行計算を特徴づける概念として，双模倣性から導かれる等価関係について習得する。
双模倣性は余帰納的な概念，ゲーム意味論によって特徴づけられることを示す。
〔計画〕
1. イントロダクション
2. 強等価性
3. 弱等価性
4. プロセス計算の意味階層
5. テストによる枠組み
6.. 総合討論 | Concurrency is modelled in terms of labelled transition systems with
communication. We show process calculi as the formal systems for
analysing concurrent systems and their logical characterisation.
Also, we discuss the timed extension of processes.
1. Introduction
2. Strong bisimularity
3. Weak bisimularity
4. Process calculi and behavioral equivalences
5. Testing framework.
6. Discussions |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | |
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 各回の演習課題を５０％と最終レポート課題を５０％，合計１００点満点で６０点以上を合格とする。 | | Exercises. |
|
|
教科書・参考書
Textbook/Reference book | | Davide Sangiorgi: Introduction to Bisimulation and Coinduction
Cambridge University Press, 2011
Doi: 10.1017/CBO9780511777110 | Davide Sangiorgi: Introduction to Bisimulation and Coinduction
Cambridge University Press, 2011
Doi: 10.1017/CBO9780511777110 |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | |
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|