权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Non-classical Logics on Labelled Structures with Data

带数据的标记结构的非经典逻辑

基本信息

批准号：
75507430
负责人：
Professor Dr. Thomas Schwentick
金额：
--
依托单位：
Informatik I - Lehrstuhl Logik in der Informatik
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2008
资助国家：
德国
起止时间：
2007-12-31 至 2013-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/75507430?language=en
关键词：
Non classical Logics Labelled Structures

项目摘要

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.

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