| 研究課題/領域番号 |
19F19797
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
佐野 勝彦 北海道大学, 文学研究院, 准教授 (20456809)
|
|---|
| 研究分担者 |
VIRTEMA JONNI 北海道大学, 文学研究院, 外国人特別研究員
|
|---|
| 研究期間 (年度) |
2019-11-08 – 2022-03-31
|
| キーワード | Team Semantics / BSS Machines / Modal Logic / Hyperproperties |
|---|
| 研究実績の概要 |
本年度の研究において、研究分担者は、Probabilistic independence logic の記述的計算量を特定した。具体的には、S-BSS機械上でクラスNPを特徴づける。さらに、S-BSS機械上でクラスPを特徴づける可能性のある有力な候補を絞った。
命題論理と様相論理のチーム意味論の設定での確率論理のモデル理論に関しては、研究分担者は研究代表者と共に関連する論理の表現力の特徴づけを与える研究を進めた。具体的には、この設定での双模倣概念を特定し、有名な van Benthem による特徴づけ定理が確率論理の設定へとどのように一般化されるのかについておおよその見通しを得た。ここで、van Benthem による特徴づけ定理とは、様相論理のクリプキモデル上での表現力が、適切な一階述語論理の双模倣に関して不変な断片の表現力と一致することを示す定理である。
研究分担者は、実行トレースについてのhyperpropertyをモデルするのに役立つ、チーム意味論をもつ様相論理の研究についても着手した。ここで hyperproperty とはトレースの集合に関する性質であり、information flow securityにおいて重要な性質となる。分担者の最近の論文Team semantics for the specification and verification of hyperpropertiesではhyperpropetyのためのチーム意味論に基づく論理（Team LTL）を構築した。特に、既存のHyper LTLと呼ばれる hyperproperty のための論理との連関について明らかにした。例えば、bounded termination という性質は Hyper LTL では表現できないが、Team LTLでは容易く表現できることになる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究開始時に予定していた、チーム意味論によ確率命題論理、および、確率様相論理のモデル論的研究については表現力の特徴づけについてのおおよその見通しを得ることができた。また、チーム意味論による確率一階述語論理についての記述的計算量の特徴づけやBSS機械との関連についての結果が得られたことで、チーム意味論による確率命題論理、確率様相論理の研究の推進にも大きく役立つ基盤を構築することができた。
|
| 今後の研究の推進方策 |
これまでチーム意味論の設定での確率論理の研究は実り豊かであることが判明し、計算機科学分野での論理への興味を惹きつけてきた。様相チーム意味論の応用として、hyperproperty の研究は有望な研究トピックといえる。またこれと同時に、命題論理や命題様相論理といった単純な設定で、確率チーム意味論の基盤的性質を明らかにすることも重要である。この点から今後の研究計画としては次の三つを考えている。第一に、計算のBSSモデルを使って計算の複雑さのクラスを特徴づける研究を進める。第二に、第一の研究で得られた計算の複雑さのクラスの特徴づけが、命題論理や様相命題論理の設定でどの程度成立するのかを調べ、計算のBSSモデルとの関連を明らかにする。第三に、上記で説明したhyperpropertyの研究をさらに進める、確率チーム意味論に基づく様相論理ないし時間論理を考案することである。
|
