格子状の様相を持つ時相論理による抽象化のための充足可能性判定

• 山本 光晴

  千葉大学理学部

• 萩谷 昌己

  東京大学大学院情報理工学系研究科

書誌事項

タイトル別名

• Satisfiability checking for abstraction by temporal logic with lattice-style modalities

抄録

我々は従来研究において、時相論理による抽象化を用いて1次元セル・オートマトンの解析を行う方法を提案した。抽象化においては、逆様相を持つ時相論理である2方向計算木論理と、その充足可能性判定が重要な役割を果たしている。本発表では、この手法を2次元以上のセル・オートマトンの解析に拡張するため、格子状の様相を持つ時相論理による抽象化を導入し、その充足可能性判定について述べる。本手法で導入する充足可能性判定においては、格子状の様相が持つ合流的性質と、実際の問題に典型的に現れるセルの属性の繰り返し構造を表現するために、Presburger式を利用する。

収録刊行物

• 日本ソフトウェア科学会大会講演論文集

  日本ソフトウェア科学会大会講演論文集 21 (0), 60-60, 2004

  日本ソフトウェア科学会

キーワード

• 形式的手法
• 抽象モデル検査
• 時相論理

詳細情報

• CRID: 1390282680500398592
• NII論文ID: 130005006623
• DOI: 10.11309/jssstconference.21.0.60.0
• ISSN: 13493515
• データソース種別:
  • JaLC
  • CiNii Articles
• 抄録ライセンスフラグ: 使用不可