| 研究課題/領域番号 |
18K11154
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| キーワード | 定理証明支援系 / 形式化 / ベクトル加算系 |
|---|
| 研究実績の概要 |
本研究の目的は、ベクトル加算系における到達可能性問題の決定可能性を、定理証明支援系を用いて形式化することである。本問題が決定可能であることは1981年に証明され、その後も1990年初頭にかけてその証明が改良されていたが、それらは複雑な分解操作を伴うものであった。しかし、2011年になってその複雑な分解操作を用いない形の新しい証明がなされ、その後さらにその証明の簡略化がなされている。また、旧来の証明に現れる複雑な分解操作も、理論的には「イデアル分解」と呼ばれる美しい特徴付けがあることがやはり最近の研究で判明している。
今年度も昨年度に引き続き、一般のベクトル加算系の到達可能性問題を、有界なベクトル加算系の到達可能性問題に還元する方法について調査した。この還元によって決定可能性を示すという方法は、本研究課題の開始時点では知られていなかった新しい手法である。還元先である有界なベクトル加算系の到達可能性問題の決定可能性や判定アルゴリズムは、一般の場合と比較して格段に易しく、それと等価である有界なペトリネットに関する到達可能性と判定アルゴリズムは、本研究課題の初年度で形式化を行っているため、その成果を利用できることが見込まれる。また、この還元は到達可能性の決定可能性だけでなく、到達可能性の計算量の上界を示す際にも用いられるため、この還元の形式化により、将来的には到達可能性の計算量の形式化にも寄与することが期待される。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
昨年度コロナ禍で授業形態が大きく変更されたことに伴う対応に時間を割き進捗が遅れたが、その影響を十分に取り戻せていない状況である。
|
| 今後の研究の推進方策 |
次年度が本研究課題の最終年度であるが、現在までの進捗状況に鑑み、期間を延長する予定である。また、昨年度・今年度は配属されていなかった大学院生が次年度は配属されるため、当初の計画通り、大学院生と共同で分担して課題を進めていく。
|
| 次年度使用額が生じた理由 |
今年度もコロナ禍で出張が不可能であったことと、当初予定していたパソコンの更新を行わなかったため、未使用額が生じた。旅費については状況が改善し次第、使用する計画であり、パソコンの更新は次年度に行う。また、課題の期間を延長する予定である。
|
