20 Search Results for "Kuske, Dietrich"


Document
A Class of Rational Trace Relations Closed Under Composition

Authors: Dietrich Kuske

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)


Abstract
Rational relations on words form a well-studied and often applied notion. While the definition in trace monoids is immediate, they have not been studied in this more general context. A possible reason is that they do not share the main useful properties of rational relations on words. To overcome this unfortunate limitation, this paper proposes a restricted class of rational relations, investigates its properties, and applies the findings to systems equipped with a pushdown that does not hold a word but a trace.

Cite as

Dietrich Kuske. A Class of Rational Trace Relations Closed Under Composition. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 20:1-20:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{kuske:LIPIcs.FSTTCS.2023.20,
  author =	{Kuske, Dietrich},
  title =	{{A Class of Rational Trace Relations Closed Under Composition}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.20},
  URN =		{urn:nbn:de:0030-drops-193935},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.20},
  annote =	{Keywords: rational relations, Mazurkiewicz traces, preservation of rationality and recognizability}
}
Document
Separating Regular Languages over Infinite Words with Respect to the Wagner Hierarchy

Authors: Christopher Hugenroth

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)


Abstract
We investigate the separation problem for regular ω-languages with respect to the Wagner hierarchy where the input languages are given as deterministic Muller automata (DMA). We show that a minimal separating DMA can be computed in exponential time and that some languages require separators of exponential size. Further, we show that in this setting it can be decided in polynomial time whether a separator exists on a certain level of the Wagner hierarchy and that emptiness of the intersection of two languages given by DMAs can be decided in polynomial time. Finally, we show that separation can also be decided in polynomial time if the input languages are given as deterministic parity automata.

Cite as

Christopher Hugenroth. Separating Regular Languages over Infinite Words with Respect to the Wagner Hierarchy. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 46:1-46:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{hugenroth:LIPIcs.FSTTCS.2021.46,
  author =	{Hugenroth, Christopher},
  title =	{{Separating Regular Languages over Infinite Words with Respect to the Wagner Hierarchy}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{46:1--46:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.46},
  URN =		{urn:nbn:de:0030-drops-155574},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.46},
  annote =	{Keywords: Separation, Regular, Wagner Hierarchy, Muller Automata, Parity Automata, Product Automata, Membership}
}
Document
Complexity of Counting First-Order Logic for the Subword Order

Authors: Dietrich Kuske and Christian Schwarz

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)


Abstract
This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in two-fold exponential space provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalizes the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.

Cite as

Dietrich Kuske and Christian Schwarz. Complexity of Counting First-Order Logic for the Subword Order. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 61:1-61:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{kuske_et_al:LIPIcs.MFCS.2020.61,
  author =	{Kuske, Dietrich and Schwarz, Christian},
  title =	{{Complexity of Counting First-Order Logic for the Subword Order}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{61:1--61:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.61},
  URN =		{urn:nbn:de:0030-drops-127297},
  doi =		{10.4230/LIPIcs.MFCS.2020.61},
  annote =	{Keywords: Counting logic, piecewise testable languages}
}
Document
Verification of Flat FIFO Systems

Authors: Alain Finkel and M. Praveen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.

Cite as

Alain Finkel and M. Praveen. Verification of Flat FIFO Systems. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.CONCUR.2019.12,
  author =	{Finkel, Alain and Praveen, M.},
  title =	{{Verification of Flat FIFO Systems}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.12},
  URN =		{urn:nbn:de:0030-drops-109147},
  doi =		{10.4230/LIPIcs.CONCUR.2019.12},
  annote =	{Keywords: Infinite state systems, FIFO, counters, flat systems, reachability, termination, complexity}
}
Document
A Sound Algorithm for Asynchronous Session Subtyping

Authors: Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behavior but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm and we apply it to many examples that cannot be managed with the previous approaches.

Cite as

Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asynchronous Session Subtyping. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bravetti_et_al:LIPIcs.CONCUR.2019.38,
  author =	{Bravetti, Mario and Carbone, Marco and Lange, Julien and Yoshida, Nobuko and Zavattaro, Gianluigi},
  title =	{{A Sound Algorithm for Asynchronous Session Subtyping}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.38},
  URN =		{urn:nbn:de:0030-drops-109408},
  doi =		{10.4230/LIPIcs.CONCUR.2019.38},
  annote =	{Keywords: Session types, Concurrency, Subtyping, Algorithm}
}
Document
Constant Delay Enumeration with FPT-Preprocessing for Conjunctive Queries of Bounded Submodular Width

Authors: Christoph Berkholz and Nicole Schweikardt

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
Marx (STOC 2010, J. ACM 2013) introduced the notion of submodular width of a conjunctive query (CQ) and showed that for any class Phi of Boolean CQs of bounded submodular width, the model-checking problem for Phi on the class of all finite structures is fixed-parameter tractable (FPT). Note that for non-Boolean queries, the size of the query result may be far too large to be computed entirely within FPT time. We investigate the free-connex variant of submodular width and generalise Marx’s result to non-Boolean queries as follows: For every class Phi of CQs of bounded free-connex submodular width, within FPT-preprocessing time we can build a data structure that allows to enumerate, without repetition and with constant delay, all tuples of the query result. Our proof builds upon Marx’s splitting routine to decompose the query result into a union of results; but we have to tackle the additional technical difficulty to ensure that these can be enumerated efficiently.

Cite as

Christoph Berkholz and Nicole Schweikardt. Constant Delay Enumeration with FPT-Preprocessing for Conjunctive Queries of Bounded Submodular Width. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 58:1-58:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2019.58,
  author =	{Berkholz, Christoph and Schweikardt, Nicole},
  title =	{{Constant Delay Enumeration with FPT-Preprocessing for Conjunctive Queries of Bounded Submodular Width}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{58:1--58:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.58},
  URN =		{urn:nbn:de:0030-drops-110021},
  doi =		{10.4230/LIPIcs.MFCS.2019.58},
  annote =	{Keywords: conjunctive queries, constant delay enumeration, hypertree decompositions, submodular width, fixed-parameter tractability}
}
Document
The Domino Problem is Undecidable on Surface Groups

Authors: Nathalie Aubrun, Sebastián Barbieri, and Etienne Moutot

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
We show that the domino problem is undecidable on orbit graphs of non-deterministic substitutions which satisfy a technical property. As an application, we prove that the domino problem is undecidable for the fundamental group of any closed orientable surface of genus at least 2.

Cite as

Nathalie Aubrun, Sebastián Barbieri, and Etienne Moutot. The Domino Problem is Undecidable on Surface Groups. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 46:1-46:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{aubrun_et_al:LIPIcs.MFCS.2019.46,
  author =	{Aubrun, Nathalie and Barbieri, Sebasti\'{a}n and Moutot, Etienne},
  title =	{{The Domino Problem is Undecidable on Surface Groups}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{46:1--46:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.46},
  URN =		{urn:nbn:de:0030-drops-109900},
  doi =		{10.4230/LIPIcs.MFCS.2019.46},
  annote =	{Keywords: tilings, substitutions, SFTs, decidability, domino problem}
}
Document
Climbing up the Elementary Complexity Classes with Theories of Automatic Structures

Authors: Faried Abu Zaid, Dietrich Kuske, and Peter Lindner

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)


Abstract
Automatic structures are structures that admit a finite presentation via automata. Their most prominent feature is that their theories are decidable. In the literature, one finds automatic structures with non-elementary theory (e.g., the complete binary tree with equal-level predicate) and automatic structures whose theories are at most 3-fold exponential (e.g., Presburger arithmetic or infinite automatic graphs of bounded degree). This observation led Durand-Gasselin to the question whether there are automatic structures of arbitrary high elementary complexity. We give a positive answer to this question. Namely, we show that for every h >=0 the forest of (infinitely many copies of) all finite trees of height at most h+2 is automatic and it's theory is complete for STA(*, exp_h(n, poly(n)), poly(n)), an alternating complexity class between h-fold exponential time and space. This exact determination of the complexity of the theory of these forests might be of independent interest.

Cite as

Faried Abu Zaid, Dietrich Kuske, and Peter Lindner. Climbing up the Elementary Complexity Classes with Theories of Automatic Structures. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 3:1-3:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{abuzaid_et_al:LIPIcs.CSL.2018.3,
  author =	{Abu Zaid, Faried and Kuske, Dietrich and Lindner, Peter},
  title =	{{Climbing up the Elementary Complexity Classes with Theories of Automatic Structures}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.3},
  URN =		{urn:nbn:de:0030-drops-96701},
  doi =		{10.4230/LIPIcs.CSL.2018.3},
  annote =	{Keywords: Automatic Structures, Complexity Theory, Model Theory}
}
Document
Gaifman Normal Forms for Counting Extensions of First-Order Logic

Authors: Dietrich Kuske and Nicole Schweikardt

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)


Abstract
We consider the extension of first-order logic FO by unary counting quantifiers and generalise the notion of Gaifman normal form from FO to this setting. For formulas that use only ultimately periodic counting quantifiers, we provide an algorithm that computes equivalent formulas in Gaifman normal form. We also show that this is not possible for formulas using at least one quantifier that is not ultimately periodic. Now let d be a degree bound. We show that for any formula phi with arbitrary counting quantifiers, there is a formula gamma in Gaifman normal form that is equivalent to phi on all finite structures of degree <= d. If the quantifiers of phi are decidable (decidable in elementary time, ultimately periodic), gamma can be constructed effectively (in elementary time, in worst-case optimal 3-fold exponential time). For the setting with unrestricted degree we show that by using our Gaifman normal form for formulas with only ultimately periodic counting quantifiers, a known fixed-parameter tractability result for FO on classes of structures of bounded local tree-width can be lifted to the extension of FO with ultimately periodic counting quantifiers (a logic equally expressive as FO+MOD, i.e., first-oder logic with modulo-counting quantifiers).

Cite as

Dietrich Kuske and Nicole Schweikardt. Gaifman Normal Forms for Counting Extensions of First-Order Logic. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 133:1-133:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{kuske_et_al:LIPIcs.ICALP.2018.133,
  author =	{Kuske, Dietrich and Schweikardt, Nicole},
  title =	{{Gaifman Normal Forms for Counting Extensions of First-Order Logic}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{133:1--133:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.133},
  URN =		{urn:nbn:de:0030-drops-91375},
  doi =		{10.4230/LIPIcs.ICALP.2018.133},
  annote =	{Keywords: Finite model theory, Gaifman locality, modulo-counting quantifiers, fixed parameter tractable model-checking}
}
Document
Infinite and Bi-infinite Words with Decidable Monadic Theories

Authors: Dietrich Kuske, Jiamou Liu, and Anastasia Moskvina

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


Abstract
We study word structures of the form (D,<=,P) where D is either N or Z, <= is a linear ordering on D and P in D is a predicate on D. In particular we show: (a) The set of recursive omega-words with decidable monadic second order theories is Sigma_3-complete. (b) We characterise those sets P subset of Z that yield bi-infinite words (Z,<=,P) with decidable monadic second order theories. (c) We show that such "tame" predicates P exist in every Turing degree. (d) We determine, for P subset of Z, the number of predicates Q subset of Z such that (Z,<=,P) and (Z,<=,Q) are indistinguishable. Through these results we demonstrate similarities and differences between logical properties of infinite and bi-infinite words.

Cite as

Dietrich Kuske, Jiamou Liu, and Anastasia Moskvina. Infinite and Bi-infinite Words with Decidable Monadic Theories. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 472-486, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{kuske_et_al:LIPIcs.CSL.2015.472,
  author =	{Kuske, Dietrich and Liu, Jiamou and Moskvina, Anastasia},
  title =	{{Infinite and Bi-infinite Words with Decidable Monadic Theories}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{472--486},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.472},
  URN =		{urn:nbn:de:0030-drops-54325},
  doi =		{10.4230/LIPIcs.CSL.2015.472},
  annote =	{Keywords: infinite words, bi-infinite words, monadic second order logic}
}
Document
Verification of Dynamic Register Automata

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)


Abstract
We consider the verification problem for Dynamic Register Automata (DRA). DRA extend classical register automata by process creation. In this setting, each process is equipped with a finite set of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a DRA reaches a configuration where at least one process is in an error state. We first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we introduce the model of degenerative DRA which allows non-deterministic reset of the registers. We prove that for every given DRA, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative DRA remains undecidable, we show that the problem becomes decidable with nonprimitive recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we consider the class of strongly safe DRA, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe DRA, the state reachability problem becomes decidable.

Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine. Verification of Dynamic Register Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 653-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2014.653,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Kara, Ahmet and Rezine, Othmane},
  title =	{{Verification of  Dynamic Register Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{653--665},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.653},
  URN =		{urn:nbn:de:0030-drops-48787},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.653},
  annote =	{Keywords: Verification, Reachability problem, Register automata}
}
Document
Isomorphisms of scattered automatic linear orders

Authors: Dietrich Kuske

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)


Abstract
We prove the undecidability of the existence of an isomorphism between scattered tree-automatic linear orders as well as the existence of automorphisms of scattered word automatic linear orders. For the existence of automatic automorphisms of word automatic linear orders, we determine the exact level of undecidability in the arithmetical hierarchy.

Cite as

Dietrich Kuske. Isomorphisms of scattered automatic linear orders. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 455-469, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{kuske:LIPIcs.CSL.2012.455,
  author =	{Kuske, Dietrich},
  title =	{{Isomorphisms of scattered automatic linear orders}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{455--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.455},
  URN =		{urn:nbn:de:0030-drops-36906},
  doi =		{10.4230/LIPIcs.CSL.2012.455},
  annote =	{Keywords: Automatic structures, isomorphism, automorphism}
}
Document
Is Ramsey's Theorem omega-automatic?

Authors: Dietrich Kuske

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)


Abstract
We study the existence of infinite cliques in $\omega$-automatic (hyper-)graphs. It turns out that the situation is much nicer than in general uncountable graphs, but not as nice as for automatic graphs. More specifically, we show that every uncountable $\omega$-automatic graph contains an uncountable co-context-free clique or anticlique, but not necessarily a context-free (let alone regular) clique or anticlique. We also show that uncountable $\omega$-automatic ternary hypergraphs need not have uncountable cliques or anticliques at all.

Cite as

Dietrich Kuske. Is Ramsey's Theorem omega-automatic?. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 537-548, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{kuske:LIPIcs.STACS.2010.2483,
  author =	{Kuske, Dietrich},
  title =	{{Is Ramsey's Theorem omega-automatic?}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{537--548},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2483},
  URN =		{urn:nbn:de:0030-drops-24838},
  doi =		{10.4230/LIPIcs.STACS.2010.2483},
  annote =	{Keywords: Logic in computer science, automata, Ramsey theory}
}
Document
07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures

Authors: Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Proceedings, Volume 7441, Algorithmic-Logical Theory of Infinite Structures (2008)


Abstract
From 28.10. to 02.11.2007, the Dagstuhl Seminar 07441 ``Algorithmic-Logical Theory of Infinite Structures'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi. 07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{downey_et_al:DagSemProc.07441.1,
  author =	{Downey, Rod and Khoussainov, Bakhadyr and Kuske, Dietrich and Lohrey, Markus and Vardi, Moshe Y.},
  title =	{{07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.1},
  URN =		{urn:nbn:de:0030-drops-14122},
  doi =		{10.4230/DagSemProc.07441.1},
  annote =	{Keywords: Theories of infinite structures , computable model theory and automatic structures , model checking infinite systems}
}
Document
07441 Summary – Algorithmic-Logical Theory of Infinite Structures

Authors: Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Proceedings, Volume 7441, Algorithmic-Logical Theory of Infinite Structures (2008)


Abstract
One of the important research fields of theoretical and applied computer science and mathematics is the study of algorithmic, logical and model theoretic properties of structures and their interactions. By a structure we mean typical objects that arise in computer science and mathematics such as data structures, programs, transition systems, graphs, large databases, XML documents, algebraic systems including groups, integers, fields, Boolean algebras and so on.

Cite as

Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi. 07441 Summary – Algorithmic-Logical Theory of Infinite Structures. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{downey_et_al:DagSemProc.07441.2,
  author =	{Downey, Rod and Khoussainov, Bakhadyr and Kuske, Dietrich and Lohrey, Markus and Vardi, Moshe Y.},
  title =	{{07441 Summary – Algorithmic-Logical Theory of Infinite Structures}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.2},
  URN =		{urn:nbn:de:0030-drops-14111},
  doi =		{10.4230/DagSemProc.07441.2},
  annote =	{Keywords: Theories of infinite structures , computable model theory and automatic structures , model checking infinite systems}
}
  • Refine by Author
  • 11 Kuske, Dietrich
  • 4 Lohrey, Markus
  • 2 Downey, Rod
  • 2 Khoussainov, Bakhadyr
  • 2 Schweikardt, Nicole
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Complexity theory and logic
  • 2 Theory of computation → Regular languages
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Database query processing and optimization (theory)
  • Show More...

  • Refine by Keyword
  • 3 Logic in computer science
  • 2 Rabin's tree theorem
  • 2 Theories of infinite structures
  • 2 complexity
  • 2 computable model theory and automatic structures
  • Show More...

  • Refine by Type
  • 20 document

  • Refine by Publication Year
  • 7 2008
  • 4 2019
  • 2 2018
  • 1 2010
  • 1 2012
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail