授業の目的 【日本語】
Goals of the Course(JPN) | | | 本講義では，並行計算の形式モデルとしての通信プロセス，特に，MilnerのCCS(Calculus for Communicating Systems) について学ぶ．操作的意味を構造的操作的意味定義(Structural Operational Semantics)によって定義し，通信の可能性に基づく等価な振舞いとして，双模倣等価性(bisimularity)を定める．CCSにおける演算子が双模倣性を保存することによって，並行計算の代数が構成できることを示す． さらに，様相論理体系としてHennessy-Milner論理との関係を示す． |
|
|
授業の目的 【英語】
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 are defined in the form of
SOS(Structural Operational Semantics) and understood as
the bisimularity of communication capability. CCS is shown to hold
algebraic properties with respect to its operations. We further
discuss the relationship to the model logic of Hennessy-Milner logic. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | 並行計算を表現する通信プロセス計算の体系について修得する．
通信プロセス計算としてMilnerのCCSに対して双模倣性を学び，並行計算をプロセス代数として理解する．
振舞いを特徴づける時相論理の拡張について示し，基本的な検証手法について示す． |
|
|
到達目標 【英語】
Objectives of the Course | | We learn the formal calculus for communicating systems with concurrency.
This lecture discusses Milner's CCS and the bisimularity as the fundamental understanding
of concurrency and CCS forms an algebra of communication systems as 'Process Algebra'.
The modal logic of Hennesy-Milner fully characterizes the bisimularity to show a verification
method for concurrent systems.
|
|
|
授業の内容や構成
Course Content / Plan | | 並行計算をラベル付き遷移システムとしてモデル化する。
複数のラベル付き遷移システムがラベルの同期による相互作用を及ぼしながら計算が進行する。
並行計算を特徴づける概念として，双模倣性から導かれる等価関係について習得する。
双模倣性は余帰納的な概念，ゲーム意味論によって特徴づけられることを示す。
〔計画〕
1. イントロダクション
2. 強等価性
3. 弱等価性
4. プロセス計算の意味階層
5. 時相論理HMLによる特徴付け
6. 総合討論 | Concurrency is modeled in terms of labeled transition systems with
communication. We show process calculi as the formal systems for
analyzing concurrent systems and their logical characterization.
Also, we discuss the timed extension of processes.
1. Introduction
2. Strong bisimularity
3. Weak bisimularity
4. Process calculi
5. Hennessy/Milner Logic
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) | | | 各回において演習課題を出し，終了時にレポート課題を出題する。 | | Several exercises are given. |
|
|
授業開講形態等
Lecture format, etc. | | | 対面を基本とするが，必要に応じてリアルタイム配信のリモート講義を実施する。 |
|
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|