Coalgebra-based generic decision procedures and complexity bounds for modal and hybrid logics

基于代数的通用决策程序以及模态和混合逻辑的复杂性界限

• 批准号: 59369218
• 负责人: Professor Dr. Lutz Schröder
• 金额: --
• 依托单位: Informatik 8 - Theoretische Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2007
• 资助国家: 德国
• 起止时间: 2006-12-31 至 2020-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/59369218?language=en
• 关键词: Coalgebra; based; generic; decision; procedures

Modal logics and various extensions of the basic modal language, e.g. hybrid languages that provide expressive means for reasoning about individuals and fixed point languages that capture different forms of temporal development, traditionally play a central role in computer science, in particular in the analysis of reactive systems and in knowledge representation. In both areas, there has been a notable tendency to move beyond the classical Kripke-style relational interpretation of modalities towards more elaborate system types, such as game-based, probabilistic, or preferential systems, giving rise, e.g., to alternating-time temporal logic, probabilistic description logics, and non-monotonic conditional logics, which obey rather different laws than relational modal logics. Coalgebraic logic provides a framework in which a wide variety of such logics can be treated in a semantically uniform manner, and indeed even allows for the development of generic algorithms and an ensuing generic complexity analysis. The current project is aimed at further extending and deepening the algorithmic foundations of coalgebraic modal logic, in particular towards iterative logics, fixed point logics, decidable fragments of coalgebraic first-order logics, and many-dimensional coalgebraic logics. The generic algorithms will be combined with a range of generic heuristic optimization strategies to obtain an efficient reasoner for coalgebraic temporal and description logics.

模态逻辑和基本模态语言的各种扩展，例如为个体推理提供表达手段的混合语言和捕捉不同形式的时间发展的固定点语言，传统上在计算机科学中起着核心作用，特别是在分析反应系统和知识表示方面。在这两个领域，都有一个明显的趋势，即超越经典的克里普克风格的模态关系解释，转向更复杂的系统类型，如基于游戏的、概率的或优先的系统，从而产生了交替时间时间逻辑、概率描述逻辑和非单调条件逻辑，它们遵循的规律与关系模态逻辑截然不同。共代数逻辑提供了一个框架，在这个框架中，可以以语义统一的方式处理各种各样的逻辑，实际上甚至允许开发通用算法和随后的通用复杂性分析。目前的项目旨在进一步扩展和深化共代数模态逻辑的算法基础，特别是迭代逻辑、不动点逻辑、共代数一阶逻辑的可决片段和多维共代数逻辑。通用算法将与一系列通用启发式优化策略相结合，以获得一个有效的共代数时间逻辑和描述逻辑推理器。

项目成果

Automatic verification of application-tailored OSEK kernels

自动验证应用程序定制的 OSEK 内核

• DOI: 10.23919/fmcad.2017.8102260
• 发表时间: 2017
• 期刊: 2017 Formal Methods in Computer Aided Design (FMCAD)
• 作者: Hans-Peter Deifel;Merlin Göttlinger;Stefan Milius;Lutz Schröder;Christian Dietrich;Daniel Lohmann
• 通讯作者: Daniel Lohmann

Completeness of Flat Coalgebraic Fixpoint Logics

• DOI: 10.1145/3157055
• 发表时间: 2018-01
• 期刊: ACM Transactions on Computational Logic (TOCL)
• 作者: Lutz Schröder;Y. Venema

Uniform Interpolation in Coalgebraic Modal Logic

代数模态逻辑中的一致插值

• DOI: 10.4230/lipics.calco.2017.21
• 发表时间: 2017
• 期刊: ArXiv
• 作者: Fatemeh Seifan;Lutz Schröder;Dirk Pattinson
• 通讯作者: Dirk Pattinson