License: 
Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2008.1325
URN: urn:nbn:de:0030-drops-13253
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1325/
Schwentick, Thomas
A Little Bit Infinite? On Adding Data to Finitely Labelled Structures (Abstract)
Abstract
Finite or infinite strings or trees with labels from a finite alphabet play an important role
in computer science. They can be used to model many interesting objects including system
runs in Automated Verification and XML documents in Database Theory. They allow the
application of formal tools like logical formulas to specify properties and automata for their
implementation. In this framework, many reasoning tasks that are undecidable for general
computational models can be solved algorithmically, sometimes even efficiently.
Nevertheless, the use of finitely labelled structures usually requires an early abstraction
from the real data. For example, theoretical research on XML processing very often con-
centrates on the document structure (including labels) but ignores attribute or text values.
While this abstraction has led to many interesting results, some aspects like key or other
integrity constraints can not be adequately handled.
In Automated Verification of software systems or communication protocols, infinite
domains occur even more naturally, e.g., induced by program data, recursion, time, com-
munication or by unbounded numbers of concurrent processes. Usually one approximates
infinite domains by finite ones in a very early abstraction step.
An alternative approach that has been investigated in recent years is to extend strings
and trees by (a limited amount of) data and to use logical languages with a restricted ex-
pressive power concerning this data. As an example, in the most simple setting, formulas
can only test equality of data values. The driving goal is to identify logical languages and
corresponding automata models which are strong enough to describe interesting proper-
ties of data-enhanced structures while keeping decidability or even feasibility of automatic
reasoning.
The talk gives a basic introduction into data-enhanced finitely labelled structures,
presents examples of their use, and highlights recent decidability and complexity results.
BibTeX - Entry
@InProceedings{schwentick:LIPIcs:2008:1325,
author = {Thomas Schwentick},
title = {{A Little Bit Infinitel On Adding Data to Finitely Labelled Structures (Abstract)}},
booktitle = {25th International Symposium on Theoretical Aspects of Computer Science},
pages = {17--18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-06-4},
ISSN = {1868-8969},
year = {2008},
volume = {1},
editor = {Susanne Albers and Pascal Weil},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1325},
URN = {urn:nbn:de:0030-drops-13253},
doi = {10.4230/LIPIcs.STACS.2008.1325},
annote = {Keywords: }
}
|
Collection: |
|
25th International Symposium on Theoretical Aspects of Computer Science |
|
Issue Date: |
|
2008 |
|
Date of publication: |
|
06.02.2008 |
