Non-classical Logics on Labelled Structures with Data

有限标记结构如字符串或节点标记树在计算机科学中无处不在。在这种结构的帮助下，许多类型的对象都可以很容易地建模，例如，在自动验证或XML文档的上下文中运行的系统。形式化工具由逻辑（用于规范）和自动机（用于实现）提供。这个项目是关于从一个可能无限的领域通过数据值来扩展有限标记的结构，以及开发相应的工具，如逻辑、自动机和算法。在逻辑方面，重点是模态逻辑、时间逻辑和混合逻辑——在项目名称中被归入“非经典逻辑”。在自动验证的上下文中，数据值可用于表示进程id、变量值或时间点。在半结构化数据上下文中，它们可以表示属性值或文本值。在项目的后续工作中，我们将开发具有动态流程创建的分布式系统模型，以及具有线性或分支时间的数据感知时态逻辑，并在表达性和算法属性之间进行良好的权衡。这些模型将作为经典的基于状态的模型和消息序列图的扩展而获得。为了产生具有可确定（甚至有效）模型检查的场景，将考虑逻辑的限制以及模型的可能运行或计算树的结构的限制。

Finitely labelled structures as strings or node-labelled trees are ubiquitous in Computer Science. Many kinds of objects can be easily modelled with the help of such structures, e.g., system runs in the context of automated verification or XML documents. Formal tools are provided by logics (for specification) and automata (for implementation). This project is about the extension of finitely labelled structures by data values from a possibly infinite domain and the development of respective tools as logics, automata and algorithms. On the side of logics, the focus is on modal, temporal and hybrid logics - subsumed under the term "non-classical logics" in the name of the project.In the context of automated verification, the data values can be used to represent process ids, values of variables or time points. In the context of semistructured data, they can represent attribute or textual values.In the continuation of the project, we will develop models for distributed systems with dynamic process creation and data-aware temporal logics with linear or branching time with a good trade-off between expressiveness and algorithmic properties. These models will be obtained as extensions of classical state-based models and Message Sequence Charts. To yield scenarios with decidable (or even efficient) Model Checking, restrictions of logics will be considered as well as restrictions of the structure of possible runs or computation trees of the models.