| 研究課題/領域番号 |
18K11154
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| キーワード | 定理証明支援系 / 形式化 / ベクトル加算系 |
|---|
| 研究実績の概要 |
本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
今年度オンラインで開催された国際会議LICS/ICALPでのJerome Leroux氏による招待講演において、一般のベクトル加算系の到達可能性問題が、有界なベクトル加算系の到達可能性問題に対数領域還元可能であるという内容が発表された。後者の有界な場合に限った決定可能性や判定アルゴリズムは、一般の場合と比較して格段に易しい。この還元は前年度に同氏らがLICSで発表した論文中の定理の応用となっており、今年度はこの内容について調査を行った。有界なベクトル加算系への還元によって決定可能性を示すという方法は、本研究課題の開始時点では知られていなかった新しい手法である。還元先である有界なベクトル加算系の到達可能性問題の決定可能性については、それと等価である有界なペトリネットに関しては本研究課題の初年度で形式化を行っているため、その成果を利用できるのではないかと考えている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
今年度はコロナ禍で授業形態が大きく変更されたことに伴う対応に時間を割かざるを得なかったため。
|
| 今後の研究の推進方策 |
コロナ禍による授業形態の変更への対応は今年度である程度ノウハウが蓄積されたため、次年度以降は本研究課題の遂行に時間をかけることができるように思われる。
|
| 次年度使用額が生じた理由 |
今年度はコロナ禍で出張が不可能であったため、未使用額が生じた。
次年度以降、状況が改善し次第、旅費として使用する計画である。
今後の進捗状況によっては期間延長も考慮に入れる。
|
