Scholarlink

<p>Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows one to state properties about geometrical entities whose attributes change over time. For the given extension, we prove the equivalence of its operational semantics with a denotational one. We then introduce a temporal extension of the tool <Emphasis FontCategory="NonProportional">VoxLogicA</Emphasis>, a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Spatio-temporal Model Checking with VoxLogicA

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年6月3日

查看全文
  • Laura Bussi,
  • Vincenzo Ciancia,
  • Fabio Gadducci,
  • Mieke Massink

摘要

Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows one to state properties about geometrical entities whose attributes change over time. For the given extension, we prove the equivalence of its operational semantics with a denotational one. We then introduce a temporal extension of the tool VoxLogicA, a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams.