Non-classical Logics on Labelled Structures with Data

点击翻译按钮获取中文摘要

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.