Geometric Model Checking of Continuous Space

要約

トポロジ空間モデル チェックは、モーダル ロジックのトポロジ解釈のためにモデル チェック技術が開発された最近のパラダイムです。
クロージャー スペースの空間ロジック (SLCS) は、モーダル ロジックを到達可能性結合子で拡張します。これは、「近くにいる」または「囲まれている」などの興味深い空間プロパティを表現するために使用できます。
SLCS は、準離散閉包空間として解釈される、グラフやデジタル画像などの離散空間について推論するための堅固な論理フレームワークの核を構成します。
最近開発された Modal Logic の幾何学的セマンティクスに従って、多面体に基づくモデルに頼ることにより、幾何学的空間モデルのチェック手順を認めて、連続空間での SLCS の解釈を提案します。
このような空間の表現は、メッシュ処理を利用する 3D スキャンおよび視覚化技術の最近の開発により、多くのアプリケーション ドメインでますます関連性が高まっています。
多面体のSLCS式の幾何学的空間モデルチェッカーであるPolyLogicAを紹介し、現実的なサイズの2つの3D多面体モデルでのアプローチの実現可能性を示します。
最後に、二相似性の幾何学的定義を導入し、それが論理的等価性を特徴付けることを証明します。

要約(オリジナル)

Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as ‘being near to’ or ‘being surrounded by’. SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google