学部・大学院区分情報・博前
時間割コード2550060
科目区分
主専攻科目
科目名　【日本語】並行分散計算特論2
科目名　【英語】
コースナンバリングコードGSI156052J
担当教員　【日本語】結縁　祥治 ○
担当教員　【英語】YUEN Shoji ○
単位数1
開講期・開講時間帯秋２期 火曜日 ２時限
Fall2 Tue 2
対象学年１年
1
授業形態
開講系（学部）・開講専攻（大学院）
情報システム学専攻
必修・選択


授業の目的　【日本語】
授業の目的　【英語】
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 timed property of concurrent systems to extend process
calculi to timed behavior, and apply the verification of timed systems
such as embedded systems.
到達目標　【日本語】
並行計算を表現する通信プロセス計算の体系について習得する。
通信プロセス計算として代表的なMilnerのCCS(CalculusforCommunicatingSystems)に対して双模倣性に基づく代数的意味論を示す。
さらに振舞いを特徴づける時相論理の拡張について示し，基本的な検証手法について示す。
最後に，並行システムの時間的な性質の特徴づけについて述べ，組み込みシステムなど時間に依存したシステムのモデル化と検証手法の基礎を習得する。
到達目標　【英語】
Concurrency is ubiquitous these days with the development of computer hardware
and network. This lecture discusses the fundamentals for theory and practice of
concurrency to characterise and analyse the behaviour of concurrent computation.
授業の内容や構成
並行計算をラベル付き遷移システムとしてモデル化する。
複数のラベル付き遷移システムがラベルの同期による相互作用を及ぼしながら計算が進行する。
並行計算を特徴づける概念として，双模倣性から導かれる等価関係について習得する。
双模倣性は余帰納的な概念，ゲーム意味論によって特徴づけられることを示す。

〔計画〕
1. イントロダクション
2. 強等価性
3. 弱等価性
4. プロセス計算の意味階層
5. 時相論理HMLによる特徴付け
6. 時間概念によるプロセス計算の拡張
7. 総合討論
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
5. Hennessy/Milner Logic
6. Timed extension
7. Discussions
履修条件・関連する科目
成績評価の方法と基準
各回の演習課題を５０％と最終レポート課題を５０％，合計１００点満点で６０点以上を合格とする。
Exercises.
教科書・参考書
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
課外学習等（授業時間外学習の指示）
各回において演習課題を出し，終了時にレポート課題を出題する。
Several exercises are given.
授業開講形態等
遠隔授業（オンデマンド型）で行う場合の追加措置