リアクティブシステムの段階的充足可能性とSafety Propertyの関係

スポンサーリンク

概要

論文の詳細を見る
時相論理で記述されたリアクティブシステムの仕様から、その仕様を満たすリアクティブシステムが存在するかどうかを判定することができる。また、その実現可能性に関しては様々な性質が提案されている。ここで提案されている実現可能性は、実際のリアクティブシステムにとっては、強すぎる性質である。一方、段階的充足可能性は、実際のリアクティブシステムが満たすべき性質に最も近いものであると考えられる。Safety Propertyは、システムが満たすべき重要な性質であり、システムの安全性を保証するものである。本稿では、段階的充足可能性を満たす仕様からは、その仕様を満たし、かつ、Safety Propertyを満たすリアクティブシステムが存在することを示す。これにより、段階的充足可能性が実際のリアクティブシステムが満たすべき性質であることが言える。
社団法人電子情報通信学会の論文
2001-01-16

著者

関連論文

もっと見る

スポンサーリンク