論文の概要: Geometric Model Checking of Continuous Space
- arxiv url: http://arxiv.org/abs/2105.06194v1
- Date: Thu, 13 May 2021 11:25:25 GMT
- ステータス: 処理完了
- システム内更新日: 2021-05-14 14:03:24.176993
- Title: Geometric Model Checking of Continuous Space
- Title（参考訳）: 連続空間の幾何学的モデル検査
- Authors: Nick Bezhanishvili and Vincenzo Ciancia and David Gabelaia and
Gianluca Grilletti and Diego Latella and Mieke Massink
- Abstract要約: 閉空間空間の空間論理(SLCS)は、離散空間を推論するための固体論理フレームワークの核を構成する。
連続空間におけるSLCSの解釈を、ポリヘドラに基づくモデルに頼って、モデル検査の手続きを認めることが可能であることを示す。
SLCS式をポリヘドラ上で効率よく検証することを目的とした,新しいツールPolyLogicAによるアプローチの実現可能性を示す。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Topological Spatial Model Checking is a recent paradigm that combines Model
Checking with 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. In particular,
the spatial model checker VoxLogicA, that uses an extended version of SLCS, has
been used successfully in the domain of medical imaging. However, SLCS is not
restricted to discrete space. Following a recently developed geometric
semantics of Modal Logic, we show that it is possible to assign an
interpretation to SLCS in continuous space, admitting a model checking
procedure, by resorting to models based on polyhedra. In medical imaging such
representations of space are increasingly relevant, due to recent developments
of 3D scanning and visualisation techniques that exploit mesh processing. We
demonstrate feasibility of our approach via a new tool, PolyLogicA, aimed at
efficient verification of SLCS formulas on polyhedra, while inheriting some
well-established optimization techniques already adopted in VoxLogicA. Finally,
we cater for a geometric definition of bisimilarity, proving that it
characterises logical equivalence.
- Abstract（参考訳）: トポロジカル空間モデルチェックは、モデルチェックとモーダル論理のトポロジカル解釈を組み合わせた最近のパラダイムである。
閉包空間の空間論理(SLCS)は、モーダル論理を到達可能性接続で拡張し、「近く」や「囲まれている」といった興味深い空間特性を表現するのに使用できる。
SLCS は、グラフやデジタル画像などの離散空間を準離散閉包空間として解釈するソリッド論理フレームワークの核を構成する。
特に、SLCSの拡張版を用いた空間モデルチェッカーVoxLogicAは、医用画像の領域でうまく使われている。
しかし、SLCS は離散空間に制限されない。
最近開発されたモーダル論理の幾何学的意味論に従えば、ポリヘドラに基づくモデルに頼ってモデル検査手順を認めることで、連続空間におけるSLCSに解釈を割り当てることが可能であることを示す。
医用画像におけるこのような空間の表現は、メッシュ処理を利用する3Dスキャンと可視化技術の発展により、ますます重要になっている。
我々は、VoxLogicAですでに採用されている最適化手法を継承しつつ、ポリヘドラ上でのSLCS公式の効率的な検証を目的とした新しいツールPolyLogicAによるアプローチの実現可能性を示す。
最後に、双相同性の幾何学的定義を求め、論理同値性を特徴付ける。
関連論文リスト
- PRAGA: Prototype-aware Graph Adaptive Aggregation for Spatial Multi-modal Omics Analysis [1.1619559582563954]
空間多モードオミクス解析(PRAGA)のための空間多モードオミクス解決フレームワークPRototype-Aware Graph Adaptative Aggregationを提案する。
PRAGAは動的グラフを構築し、潜在意味関係を捉え、空間情報と特徴意味論を包括的に統合する。
学習可能なグラフ構造は、クロスモーダルな知識を学習することで摂動を損なうこともできる。
論文 参考訳（メタデータ） (2024-09-19T12:53:29Z) - S$^2$Mamba: A Spatial-spectral State Space Model for Hyperspectral Image Classification [44.99672241508994]
ハイパースペクトル画像(HSI)を用いた土地被覆解析は、空間分解能の低さと複雑なスペクトル情報のため、未解決の課題である。
ハイパースペクトル画像分類のための空間スペクトル状態空間モデルであるS$2$Mambaを提案する。
論文 参考訳（メタデータ） (2024-04-28T15:12:56Z) - Geometric Neural Diffusion Processes [55.891428654434634]
拡散モデルの枠組みを拡張して、無限次元モデリングに一連の幾何学的先行を組み込む。
これらの条件で、生成関数モデルが同じ対称性を持つことを示す。
論文 参考訳（メタデータ） (2023-07-11T16:51:38Z) - Active Nearest Neighbor Regression Through Delaunay Refinement [79.93030583257597]
近接回帰に基づく能動関数近似アルゴリズムを提案する。
我々のActive Nearest Neighbor Regressor (ANNR) は計算幾何学の Voronoi-Delaunay フレームワークに頼り、空間を一定の関数値のセルに分割する。
論文 参考訳（メタデータ） (2022-06-16T10:24:03Z) - Inverting brain grey matter models with likelihood-free inference: a
tool for trustable cytoarchitecture measurements [62.997667081978825]
脳の灰白質細胞構造の特徴は、体密度と体積に定量的に敏感であり、dMRIでは未解決の課題である。
我々は新しいフォワードモデル、特に新しい方程式系を提案し、比較的スパースなb殻を必要とする。
次に,提案手法を逆転させるため,確率自由推論 (LFI) として知られるベイズ解析から最新のツールを適用した。
論文 参考訳（メタデータ） (2021-11-15T09:08:27Z) - A spatial model checker in GPU (extended version) [0.9023847175654602]
我々は、新しいGPUベースのvoxlogicaを紹介し、その実装、スケーラビリティ、アプリケーションについて議論する。
単純な論理的仕様による脳腫瘍のセグメント化のための既存のベンチマークの解析は、最先端の精度に達した。
論文 参考訳（メタデータ） (2020-10-14T17:58:28Z) - Closed-Form Factorization of Latent Semantics in GANs [65.42778970898534]
画像合成のために訓練されたGAN(Generative Adversarial Networks)の潜在空間に、解釈可能な次元の豊富なセットが出現することが示されている。
本研究では,GANが学習した内部表現について検討し,その基礎となる変動要因を教師なしで明らかにする。
本稿では,事前学習した重みを直接分解することで,潜在意味発見のためのクローズドフォーム因数分解アルゴリズムを提案する。
論文 参考訳（メタデータ） (2020-07-13T18:05:36Z) - Disentangling and Unifying Graph Convolutions for Skeleton-Based Action
Recognition [79.33539539956186]
本稿では,マルチスケールグラフ畳み込みと,G3Dという空間時間グラフ畳み込み演算子を結合する簡単な方法を提案する。
これらの提案を結合することにより,MS-G3Dという強力な特徴抽出器を開発し,そのモデルが3つの大規模データセット上で従来の最先端手法より優れていることを示す。
論文 参考訳（メタデータ） (2020-03-31T11:28:25Z) - Spatial Pyramid Based Graph Reasoning for Semantic Segmentation [67.47159595239798]
セマンティックセグメンテーションタスクにグラフ畳み込みを適用し、改良されたラプラシアンを提案する。
グラフ推論は、空間ピラミッドとして構成された元の特徴空間で直接実行される。
計算とメモリのオーバーヘッドの利点で同等のパフォーマンスを実現しています。
論文 参考訳（メタデータ） (2020-03-23T12:28:07Z) - A spatio-temporalisation of ALC(D) and its translation into alternating
automata augmented with spatial constraints [0.0]
本稿では、記述論理(DL)のよく知られたALC(D)ファミリーを具体的なドメインで時間化することを検討する。
文献で遭遇するほとんどのモーダル時間論理を捉えるために、MTALC(Dx)の弱い周期的時間的ボックス(TBox)を導入する。
我々は, MTALC(Dx) の概念を弱巡回的 TBox に対して満足できる重要な結果が, 拡張空間制約を持つBuchi弱オートマトンの問題に還元可能であることを示す。
論文 参考訳（メタデータ） (2020-02-22T17:20:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。