23 Search Results for "Thomas, Wolfgang"


Document
HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete

Authors: Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)


Abstract
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is Σ₁¹-complete and HyperCTL* satisfiability is Σ₁²-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove Σ₁²-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is Π₁¹-complete.

Cite as

Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 47:1-47:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{fortin_et_al:LIPIcs.MFCS.2021.47,
  author =	{Fortin, Marie and Kuijer, Louwe B. and Totzke, Patrick and Zimmermann, Martin},
  title =	{{HyperLTL Satisfiability Is \Sigma₁¹-Complete, HyperCTL* Satisfiability Is \Sigma₁²-Complete}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{47:1--47:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.47},
  URN =		{urn:nbn:de:0030-drops-144870},
  doi =		{10.4230/LIPIcs.MFCS.2021.47},
  annote =	{Keywords: HyperLTL, HyperCTL*, Satisfiability, Analytical Hierarchy}
}
Document
Invited Talk
Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk)

Authors: Wolfgang Thomas

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)


Abstract
Determinacy of infinite two-player games is a topic of descriptive set theory that has triggered intensive research in theoretical computer science since 1957 when A. Church formulated his "synthesis problem" (regarding the construction of circuits with infinite behavior from logical specifications). In the first part of the lecture we review the fascinating development of the algorithmic theory of infinite games that was started by Church's problem, that enriched automata theory and related fields, and that led to interesting applications in verification and program synthesis. In the second part we turn to the question how to lift this theory from the case of the Cantor space (where a play is a sequence of bits) to the case of the Baire space (where a play is a sequence of natural numbers). While this step does not involve difficulties in classical descriptive set theory, the algorithmic approach raises non-trivial questions since it requires to consider automata that work over infinite alphabets. We present recent results (joint work with B. Brütsch) that provide a solution of Church's synthesis problem in this context, and we point to numerous questions that are still open.

Cite as

Wolfgang Thomas. Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{thomas:LIPIcs.CSL.2017.6,
  author =	{Thomas, Wolfgang},
  title =	{{Determinacy of Infinite Games: Perspectives of the Algorithmic Approach}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{6:1--6:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.6},
  URN =		{urn:nbn:de:0030-drops-77083},
  doi =		{10.4230/LIPIcs.CSL.2017.6},
  annote =	{Keywords: Infinite games, descriptive set theory, automata theory, transducers, automatic synthesis}
}
Document
Immersive Analytics (Dagstuhl Seminar 16231)

Authors: Tim Dwyer, Nathalie Henry Riche, Karsten Klein, Wolfgang Stuerzlinger, and Bruce Thomas

Published in: Dagstuhl Reports, Volume 6, Issue 6 (2016)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16231 "Immersive Analytics". Close to 40 researchers and practitioners participated in this seminar to discuss and define the field of Immersive Analytics, to create a community around it, and to identify its research challenges. As the participants had a diverse background in a variety of disciplines, including Human-Computer-Interaction, Augmented and Virtual Reality, Information Visualization, and Visual Analytics, the seminar featured a couple of survey talks on the first days, followed by plenary and working group discussions that were meant to shape the field of Immerswive Analytics. As an outcome, a book publication is planned with book chapters provided by the participants.

Cite as

Tim Dwyer, Nathalie Henry Riche, Karsten Klein, Wolfgang Stuerzlinger, and Bruce Thomas. Immersive Analytics (Dagstuhl Seminar 16231). In Dagstuhl Reports, Volume 6, Issue 6, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{dwyer_et_al:DagRep.6.6.1,
  author =	{Dwyer, Tim and Henry Riche, Nathalie and Klein, Karsten and Stuerzlinger, Wolfgang and Thomas, Bruce},
  title =	{{Immersive Analytics (Dagstuhl Seminar 16231)}},
  pages =	{1--9},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{6},
  editor =	{Dwyer, Tim and Henry Riche, Nathalie and Klein, Karsten and Stuerzlinger, Wolfgang and Thomas, Bruce},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.6.1},
  URN =		{urn:nbn:de:0030-drops-67249},
  doi =		{10.4230/DagRep.6.6.1},
  annote =	{Keywords: Visual Analytics, Immersion, Human-Computer Interaction, Augmented Reality, Virtual Reality}
}
Document
Past, Present, and Infinite Future

Authors: Thomas Wilke

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
I was supposed to deliver one of the speeches at Wolfgang Thomas's retirement ceremony. Wolfgang had called me on the phone earlier and posed some questions about temporal logic, but I hadn't had good answers at the time. What I decided to do at the ceremony was to take up the conversation again and show how it could have evolved if only I had put more effort into answering his questions. Here is the imaginary conversation with Wolfgang. The contributions are (1) the first direct translation from counter-free omega-automata into future temporal formulas, (2) a definition of bimachines for omega-words, (3) a translation from arbitrary temporal formulas (including both, future and past operators) into counter-free omega-bimachines, and (4) an automata-based proof of separation: every arbitrary temporal formula is equivalent to a boolean combination of pure future, present, and pure past formulas when interpreted in omega-words.

Cite as

Thomas Wilke. Past, Present, and Infinite Future. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 95:1-95:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{wilke:LIPIcs.ICALP.2016.95,
  author =	{Wilke, Thomas},
  title =	{{Past, Present, and Infinite Future}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{95:1--95:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.95},
  URN =		{urn:nbn:de:0030-drops-62306},
  doi =		{10.4230/LIPIcs.ICALP.2016.95},
  annote =	{Keywords: linear-time temporal logic, separation, backward deterministic omega-automata, counter freeness}
}
Document
Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061)

Authors: Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas

Published in: Dagstuhl Reports, Volume 5, Issue 2 (2015)


Abstract
In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and - as a special focus - connections with control engineering (supervisory control).

Cite as

Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas. Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061). In Dagstuhl Reports, Volume 5, Issue 2, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{chatterjee_et_al:DagRep.5.2.1,
  author =	{Chatterjee, Krishnendu and Lafortune, St\'{e}phane and Markey, Nicolas and Thomas, Wolfgang},
  title =	{{Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061)}},
  pages =	{1--25},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{2},
  editor =	{Chatterjee, Krishnendu and Lafortune, St\'{e}phane and Markey, Nicolas and Thomas, Wolfgang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.2.1},
  URN =		{urn:nbn:de:0030-drops-50424},
  doi =		{10.4230/DagRep.5.2.1},
  annote =	{Keywords: non-zero-sum games, infinite games, multi-player games, partial-observation games, quantitative games, controller synthesis, supervisory control}
}
Document
Constant compression and random weights

Authors: Wolfgang Merkle and Jason Teutsch

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)


Abstract
Omega numbers, as considered in algorithmic randomness, are by definition real numbers that are equal to the halting probability of a universal prefix-free Turing machine. Omega numbers are obviously left-r.e., i.e., are effectively approximable from below. Furthermore, among all left-r.e. real numbers in the appropriate range between 0 and 1, the Omega numbers admit well-known characterizations as the ones that are Martin-Löf random, as well as the ones such that any of their effective approximation from below is slower than any other effective approximation from below to any other real, up to a constant factor. In what follows, we obtain a further characterization of Omega numbers in terms of Theta numbers. Tadaki considered for a given prefix-free Turing machine and some natural number a the set of all strings that are compressed by this machine by at least a bits relative to their length, and he introduced Theta numbers as the weight of sets of this form. He showed that in the case of a universal prefix-free Turing machine any Theta number is an Omega number and he asked whether this implication can be reversed. We answer his question in the affirmative and thus obtain a new characterization of Omega numbers. In addition to the one-sided case of the set of all strings compressible by at least a certain number a of bits, we consider sets that comprise all strings that are compressible by at least a but no more than b bits, and we call the weight of such a set a two-sided Theta number. We demonstrate that in the case of a universal prefix-free Turing machine, for given a and all sufficiently large b the corresponding two-sided Theta number is again an Omega number. Conversely, any Omega number can be realized as two-sided Theta number for any pair of natural numbers a and b>a.

Cite as

Wolfgang Merkle and Jason Teutsch. Constant compression and random weights. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 172-181, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{merkle_et_al:LIPIcs.STACS.2012.172,
  author =	{Merkle, Wolfgang and Teutsch, Jason},
  title =	{{Constant compression and random weights}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{172--181},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.172},
  URN =		{urn:nbn:de:0030-drops-34351},
  doi =		{10.4230/LIPIcs.STACS.2012.172},
  annote =	{Keywords: computational complexity, Kolmogorov complexity, algorithmic randomness, Omega number}
}
Document
10501 Abstracts Collection – Advances and Applications of Automata on Words and Trees

Authors: Christian Glasser, Jean-Eric Pin, Nicole Schweikardt, Victor Selivanov, and Wolfgang Thomas

Published in: Dagstuhl Seminar Proceedings, Volume 10501, Advances and Applications of Automata on Words and Trees (2011)


Abstract
From 12.12.2010 to 17.12.2010, the Dagstuhl Seminar 10501 ``Advances and Applications of Automata on Words and Trees'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. 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

Christian Glasser, Jean-Eric Pin, Nicole Schweikardt, Victor Selivanov, and Wolfgang Thomas. 10501 Abstracts Collection – Advances and Applications of Automata on Words and Trees. In Advances and Applications of Automata on Words and Trees. Dagstuhl Seminar Proceedings, Volume 10501, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{glasser_et_al:DagSemProc.10501.1,
  author =	{Glasser, Christian and Pin, Jean-Eric and Schweikardt, Nicole and Selivanov, Victor and Thomas, Wolfgang},
  title =	{{10501 Abstracts Collection – Advances and Applications of Automata on Words and Trees}},
  booktitle =	{Advances and Applications of Automata on Words and Trees},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10501},
  editor =	{Christian Glasser and Jean-Eric Pin and Nicole Schweikardt and Victor Selivanov and Wolfgang Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10501.1},
  URN =		{urn:nbn:de:0030-drops-31486},
  doi =		{10.4230/DagSemProc.10501.1},
  annote =	{Keywords: Automata theory, logic, verification, data structures, algorithms, complexity, games, infinite games with perfect information, reactive systems, specification and verification, combinatorics, hierarchies and reducibilities}
}
Document
10501 Executive Summary – Advances and Applications of Automata on Words and Trees

Authors: Christian Glasser, Jean-Eric Pin, Nicole Schweikardt, Victor Selivanov, and Wolfgang Thomas

Published in: Dagstuhl Seminar Proceedings, Volume 10501, Advances and Applications of Automata on Words and Trees (2011)


Abstract
The aim of the seminar was to discuss and systematize the recent fast progress in automata theory and to identify important directions for future research. For this, the seminar brought together more than 40 researchers from automata theory and related fields of applications. We had 19 talks of 30 minutes and 5 one-hour lectures leaving ample room for discussions. In the following we describe the topics in more detail.

Cite as

Christian Glasser, Jean-Eric Pin, Nicole Schweikardt, Victor Selivanov, and Wolfgang Thomas. 10501 Executive Summary – Advances and Applications of Automata on Words and Trees. In Advances and Applications of Automata on Words and Trees. Dagstuhl Seminar Proceedings, Volume 10501, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{glasser_et_al:DagSemProc.10501.2,
  author =	{Glasser, Christian and Pin, Jean-Eric and Schweikardt, Nicole and Selivanov, Victor and Thomas, Wolfgang},
  title =	{{10501 Executive Summary – Advances and Applications of Automata on Words and Trees}},
  booktitle =	{Advances and Applications of Automata on Words and Trees},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10501},
  editor =	{Christian Glasser and Jean-Eric Pin and Nicole Schweikardt and Victor Selivanov and Wolfgang Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10501.2},
  URN =		{urn:nbn:de:0030-drops-31474},
  doi =		{10.4230/DagSemProc.10501.2},
  annote =	{Keywords: Infinite games with perfect information, reactive systems, specification and verification, combinatorics, hierarchies and reducibilities}
}
Document
Parsing Unary Boolean Grammars Using Online Convolution

Authors: Alexander Okhotin and Christian Reitwießner

Published in: Dagstuhl Seminar Proceedings, Volume 10501, Advances and Applications of Automata on Words and Trees (2011)


Abstract
In contrast to context-free grammars, the extension of these grammars by explicit conjunction, the so-called conjunctive grammars can generate (quite complicated) non-regular languages over a single-letter alphabet (DLT 2007). Given these expressibility results, we study the parsability of Boolean grammars, an extension of context-free grammars by conjunction and negation, over a unary alphabet and show that they can be parsed in time O(|G| log^2(n) M(n)) where M(n) is the time to multiply two n-bit integers. This multiplication algorithm is transformed into a convolution algorithm which in turn is converted to an online convolution algorithm which is used for the parsing.

Cite as

Alexander Okhotin and Christian Reitwießner. Parsing Unary Boolean Grammars Using Online Convolution. In Advances and Applications of Automata on Words and Trees. Dagstuhl Seminar Proceedings, Volume 10501, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{okhotin_et_al:DagSemProc.10501.3,
  author =	{Okhotin, Alexander and Reitwie{\ss}ner, Christian},
  title =	{{Parsing Unary Boolean Grammars Using Online Convolution}},
  booktitle =	{Advances and Applications of Automata on Words and Trees},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10501},
  editor =	{Christian Glasser and Jean-Eric Pin and Nicole Schweikardt and Victor Selivanov and Wolfgang Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10501.3},
  URN =		{urn:nbn:de:0030-drops-31465},
  doi =		{10.4230/DagSemProc.10501.3},
  annote =	{Keywords: }
}
Document
Solovay functions and K-triviality

Authors: Laurent Bienvenu, Wolfgang Merkle, and Andre Nies

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)


Abstract
As part of his groundbreaking work on algorithmic randomness, Solovay demonstrated in the 1970s the remarkable fact that there are computable upper bounds of prefix-free Kolmogorov complexity $K$ that are tight on infinitely many values (up to an additive constant). Such computable upper bounds are called Solovay functions. Recent work of Bienvenu and Downey~[STACS 2009, LIPIcs 3, pp 147-158] indicates that Solovay functions are deeply connected with central concepts of algorithmic randomness such as $Omega$ numbers, K-triviality, and Martin-Loef randomness. In what follows, among other results we answer two open problems posed by Bienvenu and Downey about the definition of $K$-triviality and about the Gacs-Miller-Yu characterization of Martin-Loef randomness. The former defines a sequence A to be K-trivial if K(A|n) <=^+ K(n), the latter asserts that a sequence A is Martin-Loef random iff C(A|n) >=^+ n-K(n). So both involve the noncomputable function K. As our main results we show that in both cases K(n) can be equivalently replaced by any Solovay function, and, what is more, that among all computable functions such a replacement is possible exactly for the Solovay functions. Moreover, similar statements hold for the larger class of all right-c.e. in place of the computable functions. These full characterizations, besides having significant theoretical interest on their own, will be useful as tools when working with K-trivial and Martin-Loef random sequences.

Cite as

Laurent Bienvenu, Wolfgang Merkle, and Andre Nies. Solovay functions and K-triviality. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 452-463, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{bienvenu_et_al:LIPIcs.STACS.2011.452,
  author =	{Bienvenu, Laurent and Merkle, Wolfgang and Nies, Andre},
  title =	{{Solovay functions and K-triviality}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{452--463},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.452},
  URN =		{urn:nbn:de:0030-drops-30345},
  doi =		{10.4230/LIPIcs.STACS.2011.452},
  annote =	{Keywords: Algorithmic randomness, Kolmogorov complexity, K-triviality}
}
Document
08271 Abstracts Collection – Topological and Game-Theoretic Aspects of Infinite Computations

Authors: Peter Hertling, Victor Selivanov, Wolfgang Thomas, William W. Wadge, and Klaus Wagner

Published in: Dagstuhl Seminar Proceedings, Volume 8271, Topological and Game-Theoretic Aspects of Infinite Computations (2008)


Abstract
From June 29, 2008, to July 4, 2008, the Dagstuhl Seminar 08271 ``Topological and Game-Theoretic Aspects of Infinite Computations'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, many 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

Peter Hertling, Victor Selivanov, Wolfgang Thomas, William W. Wadge, and Klaus Wagner. 08271 Abstracts Collection – Topological and Game-Theoretic Aspects of Infinite Computations. In Topological and Game-Theoretic Aspects of Infinite Computations. Dagstuhl Seminar Proceedings, Volume 8271, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{hertling_et_al:DagSemProc.08271.1,
  author =	{Hertling, Peter and Selivanov, Victor and Thomas, Wolfgang and Wadge, William W. and Wagner, Klaus},
  title =	{{08271 Abstracts Collection – Topological and Game-Theoretic Aspects of Infinite Computations}},
  booktitle =	{Topological and Game-Theoretic Aspects of Infinite Computations},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8271},
  editor =	{Peter Hertling and Victor Selivanov and Wolfgang Thomas and William W. Wadge and Klaus Wagner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08271.1},
  URN =		{urn:nbn:de:0030-drops-16555},
  doi =		{10.4230/DagSemProc.08271.1},
  annote =	{Keywords: Automata theory, computability in analysis, dataflow computation, hierarchies, infinite computations, infinite games, reactive systems, specification and verification, topological complexity, Wadge reducibility}
}
Document
08271 Executive Summary – Topological and Game-Theoretic Aspects of Infinite Computations

Authors: Peter Hertling, Victor Selivanov, Wolfgang Thomas, William W. Wadge, and Klaus Wagner

Published in: Dagstuhl Seminar Proceedings, Volume 8271, Topological and Game-Theoretic Aspects of Infinite Computations (2008)


Abstract
The theory of the infinite behaviour of continuously operating computing devices is of primary importance for several branches of theoretical and practical computer science. In particular, it is fundamental for the verification and synthesis of reactive systems like microprocessors or operating systems, for the understanding of dataflow computation, and for the development of adequate mathematical foundations for exact real computation. The seminar brought together researchers from many different disciplines who are working on theoretical or practical aspects of infinite computations. In this summary we describe the topics, the goals, and the contributions of the seminar.

Cite as

Peter Hertling, Victor Selivanov, Wolfgang Thomas, William W. Wadge, and Klaus Wagner. 08271 Executive Summary – Topological and Game-Theoretic Aspects of Infinite Computations. In Topological and Game-Theoretic Aspects of Infinite Computations. Dagstuhl Seminar Proceedings, Volume 8271, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{hertling_et_al:DagSemProc.08271.2,
  author =	{Hertling, Peter and Selivanov, Victor and Thomas, Wolfgang and Wadge, William W. and Wagner, Klaus},
  title =	{{08271 Executive Summary – Topological and Game-Theoretic Aspects of Infinite Computations}},
  booktitle =	{Topological and Game-Theoretic Aspects of Infinite Computations},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8271},
  editor =	{Peter Hertling and Victor Selivanov and Wolfgang Thomas and William W. Wadge and Klaus Wagner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08271.2},
  URN =		{urn:nbn:de:0030-drops-16499},
  doi =		{10.4230/DagSemProc.08271.2},
  annote =	{Keywords: Automata theory, computability in analysis, dataflow computation, hierarchies, infinite computations, infinite games, reactive systems, specification}
}
Document
Cartesian Programming: The TransLucid Programming Language

Authors: John Plaice and Blanca Mancilla

Published in: Dagstuhl Seminar Proceedings, Volume 8271, Topological and Game-Theoretic Aspects of Infinite Computations (2008)


Abstract
The TransLucid programming language is a low-level intensional language, designed to be sufficiently rich for it to be the target language for translating the common programming paradigms into it, while still being fully declarative. The objects manipulated by TransLucid, called hyperdatons, are arbitrary-dimensional infinite arrays, indexed by multidimensional tuples of arbitrary types. We present the syntax, denotational and operational semantics for a simple TransLucid system, consisting of 1) a header detailing how expressions should be parsed, 2) a set of libraries of types, and operations thereon, defined in a host language, 3) a set of TransLucid equations, and 4) a TransLucid demand to be evaluated. The evaluation of a demand for an (identifier, context) pair is undertaken using eduction, where previously computed pairs are stored in a cache called a warehouse. The execution ensures that only those dimensions actually encountered during the execution of an expression are taken into account when caching intermediate results.

Cite as

John Plaice and Blanca Mancilla. Cartesian Programming: The TransLucid Programming Language. In Topological and Game-Theoretic Aspects of Infinite Computations. Dagstuhl Seminar Proceedings, Volume 8271, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{plaice_et_al:DagSemProc.08271.3,
  author =	{Plaice, John and Mancilla, Blanca},
  title =	{{Cartesian Programming: The TransLucid Programming Language}},
  booktitle =	{Topological and Game-Theoretic Aspects of Infinite Computations},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8271},
  editor =	{Peter Hertling and Victor Selivanov and Wolfgang Thomas and William W. Wadge and Klaus Wagner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08271.3},
  URN =		{urn:nbn:de:0030-drops-16546},
  doi =		{10.4230/DagSemProc.08271.3},
  annote =	{Keywords: Cartesian programming, Lucid language, declarative programming, multidimensional programming, context-aware programming, semantics.}
}
Document
Declarative Synchronous Multithreaded Programming

Authors: Blanca Mancilla and John Plaice

Published in: Dagstuhl Seminar Proceedings, Volume 8271, Topological and Game-Theoretic Aspects of Infinite Computations (2008)


Abstract
We demonstrate how TransLucid can be used as a reactive system. At each instant, there is a set of active ports, where sets of equations, demands and threads are all registered. Each thread defines a sequence of (state, demand) pairs, and threads may interact through the overall set of equations. The entire system remains fully declarative.

Cite as

Blanca Mancilla and John Plaice. Declarative Synchronous Multithreaded Programming. In Topological and Game-Theoretic Aspects of Infinite Computations. Dagstuhl Seminar Proceedings, Volume 8271, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{mancilla_et_al:DagSemProc.08271.4,
  author =	{Mancilla, Blanca and Plaice, John},
  title =	{{Declarative Synchronous Multithreaded Programming}},
  booktitle =	{Topological and Game-Theoretic Aspects of Infinite Computations},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8271},
  editor =	{Peter Hertling and Victor Selivanov and Wolfgang Thomas and William W. Wadge and Klaus Wagner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08271.4},
  URN =		{urn:nbn:de:0030-drops-16536},
  doi =		{10.4230/DagSemProc.08271.4},
  annote =	{Keywords: Synchronous programming, distributed computing, declarative programming, Cartesian programming, multidimensional programming.}
}
Document
General Logic Programs as Infinite Games

Authors: Chrysida Galanaki, Panos Rondogiannis, and William W. Wadge

Published in: Dagstuhl Seminar Proceedings, Volume 8271, Topological and Game-Theoretic Aspects of Infinite Computations (2008)


Abstract
In [vE86] M.H. van Emden introduced a simple game semantics for definite logic programs. Recently [RW05,GRW05], the authors extended this game to apply to logic programs with negation. Moreover, under the assumption that the programs have a finite number of rules, it was demonstrated in [RW05,GRW05] that the game is equivalent to the well-founded semantics of negation. In this paper we present work-in-progress towards demonstrating that the game of [RW05,GRW05] is equivalent to the well-founded semantics even in the case of programs that have a countably infinite number of rules. We argue however that in this case the proof of correctness has to be more involved. More specifically, in order to demonstrate that the game is correct one has to define a refined game in which each of the two players in his first move makes a bet in the form of a countable ordinal. Each ordinal can be considered as a kind of clock that imposes a "time limit" to the moves of the corresponding player. We argue that this refined game can be used to give the proof of correctness for the countably infinite case.

Cite as

Chrysida Galanaki, Panos Rondogiannis, and William W. Wadge. General Logic Programs as Infinite Games. In Topological and Game-Theoretic Aspects of Infinite Computations. Dagstuhl Seminar Proceedings, Volume 8271, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{galanaki_et_al:DagSemProc.08271.5,
  author =	{Galanaki, Chrysida and Rondogiannis, Panos and Wadge, William W.},
  title =	{{General Logic Programs as Infinite Games}},
  booktitle =	{Topological and Game-Theoretic Aspects of Infinite Computations},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8271},
  editor =	{Peter Hertling and Victor Selivanov and Wolfgang Thomas and William W. Wadge and Klaus Wagner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08271.5},
  URN =		{urn:nbn:de:0030-drops-16519},
  doi =		{10.4230/DagSemProc.08271.5},
  annote =	{Keywords: Infinite Games, Negation in Logic Programming, Well-Founded Semantics}
}
  • Refine by Author
  • 10 Thomas, Wolfgang
  • 4 Selivanov, Victor
  • 3 Pin, Jean-Eric
  • 3 Wadge, William W.
  • 2 Glasser, Christian
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 4 reactive systems
  • 3 Automata theory
  • 3 infinite games
  • 3 specification and verification
  • 2 Cartesian programming
  • Show More...

  • Refine by Type
  • 23 document

  • Refine by Publication Year
  • 7 2008
  • 4 2011
  • 2 2006
  • 2 2016
  • 1 1992
  • 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