Geometric Model Checking of Continuous Space

要約

トポロジカル空間モデル検査は、モーダル論理のトポロジカルな解釈のためにモデル検査技法を開発する最近のパラダイムである。クロージャ空間の空間論理（SLCS）は、モーダル論理に到達可能接続詞を拡張し、「～に近い」「～に囲まれている」といった興味深い空間特性を表現するために使用できるようにしたものである。SLCSは、グラフやデジタル画像などの離散空間を、準離散閉空間として解釈して推論するための強固な論理的枠組みの核を構成している。最近開発されたモーダル論理の幾何学的意味論に従って、我々は連続空間における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, DeepL