Expressivity Meets Decidability in Spatiotemporal Logics
開催期間
12:00 ~ 13:00
場所
講演者
概要
避難訓練のため中止
The search for a complete logic for topological dynamics, posed as an open problem by Kremer and Mints in the mid-2000s, has been a central challenge in the field. Using the Cantor derivative interpretation within the topological semantics of modal logic, we establish a complete logical framework for dynamical systems. However, when incorporating global temporal modalities, this logic becomes undecidable. To balance expressivity with decidability, we introduce a topological fixed-point operator, achieving a logic that remains both expressive and decidable. These advancements pave the way for efficient formal reasoning and verification techniques for dynamical systems, which are essential for the development of multi-agent systems and artificial intelligence.