10 Search Results for "Graedel, Erich"

Document
DOI: 10.4230/LIPIcs.CSL.2024.19
Ehrenfeucht-Fraïssé Games in Semiring Semantics

Authors: Sophie Brinke, Erich Grädel, and Lovro Mrkonjić

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Ehrenfeucht-Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. We investigate the soundness and completeness of this method in the more general context of semiring semantics. Motivated originally by provenance analysis of database queries, semiring semantics evaluates logical statements not just by true or false, but by values in some commutative semiring; this can provide much more detailed information, for instance concerning the combinations of atomic facts that imply the truth of a statement, or practical information about evaluation costs, confidence scores, access levels or the number of successful evaluation strategies. There is a wide variety of different semirings that are relevant for provenance analysis, and the applicability of classical logical methods in semiring semantics may strongly depend on the algebraic properties of the underlying semiring. While Ehrenfeucht-Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, this is in general not the case for other semirings. We provide a detailed analysis of the soundness and completeness of model comparison games on specific semirings, not just for classical Ehrenfeucht-Fraïssé games but also for other variants based on bijections or counting. Finally we propose a new kind of games, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.
Cite as

Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{brinke_et_al:LIPIcs.CSL.2024.19,
  author =	{Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
  title =	{{Ehrenfeucht-Fra\"{i}ss\'{e} Games in Semiring Semantics}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.19},
  URN =		{urn:nbn:de:0030-drops-196623},
  doi =		{10.4230/LIPIcs.CSL.2024.19},
  annote =	{Keywords: Semiring semantics, elementary equivalence, Ehrenfeucht-Fra\"{i}ss\'{e} games}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.20
Locality Theorems in Semiring Semantics

Authors: Clotilde Bizière, Erich Grädel, and Matthias Naaf

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model-theoretic properties still apply, and how this depends on the algebraic properties of the semiring. In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf’s locality theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman’s classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.
Cite as

Clotilde Bizière, Erich Grädel, and Matthias Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{biziere_et_al:LIPIcs.MFCS.2023.20,
  author =	{Bizi\`{e}re, Clotilde and Gr\"{a}del, Erich and Naaf, Matthias},
  title =	{{Locality Theorems in Semiring Semantics}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{20:1--20:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.20},
  URN =		{urn:nbn:de:0030-drops-185546},
  doi =		{10.4230/LIPIcs.MFCS.2023.20},
  annote =	{Keywords: Semiring semantics, Locality, First-order logic}
}
Document
DOI: 10.4230/DagRep.12.2.1
Logic and Random Discrete Structures (Dagstuhl Seminar 22061)

Authors: Erich Grädel, Phokion G. Kolaitis, Marc Noy, and Matthias Naaf

Published in: Dagstuhl Reports, Volume 12, Issue 2 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22061 "Logic and Random Discrete Structures". The main topic of this seminar has been the analysis of large random discrete structures, such as trees, graphs, or permutations, from the perspective of mathematical logic. It has brought together both experts and junior researchers from a number of different areas where logic and random structures play a role, with the goal to establish new connections between such areas and to encourage interactions between foundational research and different application areas, including probabilistic databases.
Cite as

Erich Grädel, Phokion G. Kolaitis, Marc Noy, and Matthias Naaf. Logic and Random Discrete Structures (Dagstuhl Seminar 22061). In Dagstuhl Reports, Volume 12, Issue 2, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{gradel_et_al:DagRep.12.2.1,
  author =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Noy, Marc and Naaf, Matthias},
  title =	{{Logic and Random Discrete Structures (Dagstuhl Seminar 22061)}},
  pages =	{1--16},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{2},
  editor =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Noy, Marc and Naaf, Matthias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.2.1},
  URN =		{urn:nbn:de:0030-drops-169295},
  doi =		{10.4230/DagRep.12.2.1},
  annote =	{Keywords: combinatorics, complexity theory, logic, random structures, probabilistic databases}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.133
Elementary Equivalence Versus Isomorphism in Semiring Semantics

Authors: Erich Grädel and Lovro Mrkonjić

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We study the first-order axiomatisability of finite semiring interpretations or, equivalently, the question whether elementary equivalence and isomorphism coincide for valuations of atomic facts over a finite universe into a commutative semiring. Contrary to the classical case of Boolean semantics, where every finite structure is axiomatised up to isomorphism by a first-order sentence, the situation in semiring semantics is rather different, and depends on the underlying semiring. We prove that for a number of important semirings, including min-max semirings, and the semirings of positive Boolean expressions, there exist finite semiring interpretations that are elementarily equivalent but not isomorphic. The same is true for the polynomial semirings that are universal for the classes of absorptive, idempotent, and fully idempotent semirings, respectively. On the other side, we prove that for other, practically relevant, semirings such as the Viterby semiring 𝕍, the tropical semiring 𝕋, the natural semiring ℕ and the universal polynomial semiring ℕ[X], all finite semiring interpretations are first-order axiomatisable, and thus elementary equivalence implies isomorphism.
Cite as

Erich Grädel and Lovro Mrkonjić. Elementary Equivalence Versus Isomorphism in Semiring Semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 133:1-133:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.ICALP.2021.133,
  author =	{Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
  title =	{{Elementary Equivalence Versus Isomorphism in Semiring Semantics}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{133:1--133:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.133},
  URN =		{urn:nbn:de:0030-drops-142022},
  doi =		{10.4230/LIPIcs.ICALP.2021.133},
  annote =	{Keywords: Semiring semantics, elementary equivalence, axiomatisability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.17
Semiring Provenance for Fixed-Point Logic

Authors: Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.
Cite as

Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. Semiring Provenance for Fixed-Point Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dannert_et_al:LIPIcs.CSL.2021.17,
  author =	{Dannert, Katrin M. and Gr\"{a}del, Erich and Naaf, Matthias and Tannen, Val},
  title =	{{Semiring Provenance for Fixed-Point Logic}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{17:1--17:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.17},
  URN =		{urn:nbn:de:0030-drops-134518},
  doi =		{10.4230/LIPIcs.CSL.2021.17},
  annote =	{Keywords: Finite Model Theory, Semiring Provenance, Absorptive Semirings, Fixed-Point Logics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.22
Guarded Teams: The Horizontally Guarded Case

Authors: Erich Grädel and Martin Otto

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity. We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams. In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.
Cite as

Erich Grädel and Martin Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2020.22,
  author =	{Gr\"{a}del, Erich and Otto, Martin},
  title =	{{Guarded Teams: The Horizontally Guarded Case}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.22},
  URN =		{urn:nbn:de:0030-drops-116650},
  doi =		{10.4230/LIPIcs.CSL.2020.22},
  annote =	{Keywords: Team semantics, guarded logics, bisimulation, characterisation theorems}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.31
Choiceless Logarithmic Space

Authors: Erich Grädel and Svenja Schalthöfer

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

Abstract
One of the most important open problems in finite model theory is the question whether there is a logic characterising efficient computation. While this question usually concerns Ptime, it can also be applied to other complexity classes, and in particular to Logspace which can be seen as a formalisation of efficient computation for big data. One of the strongest candidates for a logic capturing Ptime is Choiceless Polynomial Time (CPT). It is based on the idea of choiceless algorithms, a general model of symmetric computation over abstract structures (rather than their encodings by finite strings). However, there is currently neither a comparably strong candidate for a logic for Logspace, nor a logic transferring the idea of choiceless computation to Logspace. We propose here a notion of Choiceless Logarithmic Space which overcomes some of the obstacles posed by Logspace as a less robust complexity class. The resulting logic is contained in both Logspace and CPT, and is strictly more expressive than all logics for Logspace that have been known so far. Further, we address the question whether this logic can define all Logspace-queries, and prove that this is not the case.
Cite as

Erich Grädel and Svenja Schalthöfer. Choiceless Logarithmic Space. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 31:1-31:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.MFCS.2019.31,
  author =	{Gr\"{a}del, Erich and Schalth\"{o}fer, Svenja},
  title =	{{Choiceless Logarithmic Space}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{31:1--31: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.31},
  URN =		{urn:nbn:de:0030-drops-109758},
  doi =		{10.4230/LIPIcs.MFCS.2019.31},
  annote =	{Keywords: Finite Model Theory, Logics for Logspace, Choiceless Computation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.112
Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Anuj Dawar, Erich Grädel, and Wied Pakusa

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parameterized by a number k and a set Q of primes. The intuition is that two equivalent graphs G equiv^IM_{k, Q} H cannot be distinguished by means of partitioning the set of k-tuples in both graphs with respect to any linear-algebraic operator acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences have first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define {LA^{k}}(Q), an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that equiv^IM_{k, Q} is the natural notion of elementary equivalence for this logic. The logic LA^{omega}(Q) = Cup_{k in omega} LA^{k}(Q) is then a natural upper bound on the expressive power of any extension of fixed-point logics by means of Q-linear-algebraic operators. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that equiv^IM_{k, Q} is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in LA^{omega}(Q), which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke’s Theorem, an important result from the representation theory of finite groups.
Cite as

Anuj Dawar, Erich Grädel, and Wied Pakusa. Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 112:1-112:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.ICALP.2019.112,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Pakusa, Wied},
  title =	{{Approximations of Isomorphism and Logics with Linear-Algebraic Operators}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{112:1--112:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.112},
  URN =		{urn:nbn:de:0030-drops-106887},
  doi =		{10.4230/LIPIcs.ICALP.2019.112},
  annote =	{Keywords: Finite Model Theory, Graph Isomorphism, Descriptive Complexity, Algebra}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1771
2008 Preface -- IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science

Authors: Ramesh Hariharan, Madhavan Mukund, and V Vinay

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
This volume contains the proceedings of the 28th international conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), organized under the auspices of the Indian Association for Research in Computing Science (IARCS). This year's conference attracted 117 submissions. Each submission was reviewed by at least three independent referees. The final selection of the papers making up the programme was done through an electronic discussion on EasyChair, spanning two weeks, without a physical meeting of the Programme Committee (PC). All PC members participated actively in the discussion. We have five invited speakers this year: Hubert Comon-Lundh, Uriel Feige, Erich Graedel, Simon Peyton Jones and Leslie Valiant. We thank them for having readily accepted our invitation to talk at the conference and for providing abstracts (and even full papers) for the proceedings. We thank all the reviewers and PC members, without whose dedicated effort the conference would not be possible. We thank the Organizing Committee for making the arrangements for the conference. This year, the conference is being held at the Indian Institute of Science, Bangalore, as part of its centenary year celebrations. It is a great honour and privilege for the conference to be recognized and associated with the institute on this occasion. Finally, this year we have taken a decisive step in democratizing the conference by moving away from commercial publishers. Instead, we will be hosting the proceedings online, electronically, via the Dagstuhl Research Online Publication Server (DROPS). A complete copy of the proceedings will also be hosted on the FSTTCS website (www.fsttcs.org). The copyrights to the papers will reside not with the publishers but with the respective authors. The copyright is now governed by the Creative Commons attribution NC-ND. We do hope this direction will be sustained in the future.
Cite as

Ramesh Hariharan, Madhavan Mukund, and V Vinay. 2008 Preface -- IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, p. -1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{hariharan_et_al:LIPIcs.FSTTCS.2008.1771,
  author =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  title =	{{2008 Preface -- IARCS Annual Conference on  Foundations of Software Technology and Theoretical Computer Science}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{-1---1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1771},
  URN =		{urn:nbn:de:0030-drops-17713},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1771},
  annote =	{Keywords: Preface}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1768
Banach-Mazur Games on Graphs

Authors: Erich Graedel

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
We survey determinacy, definability, and complexity issues of Banach-Mazur games on finite and infinite graphs. Infinite games where two players take turns to move a token through a directed graph, thus tracing out an infinite path, have numerous applications in different branches of mathematics and computer science. In the usual format, the possible moves of the players are given by the edges of the graph; in each move a player takes the token from its current position along an edge to a next position. In Banach-Mazur games the players instead select in each move a \emph{path} of arbitrary finite length rather than just an edge. In both cases the outcome of a play is an infinite path. A winning condition is thus given by a set of infinite paths which is often specified by a logical formula, for instance from S1S, LTL, or first-order logic. Banach-Mazur games have a long tradition in descriptive set theory and topology, and they have recently been shown to have interesting applications also in computer science, for instance for planning in nondeterministic domains, for the study of fairness in concurrent systems, and for the semantics of timed automata. It turns out that Banach-Mazur games behave quite differently than the usual graph games. Often they admit simpler winning strategies and more efficient algorithmic solutions. For instance, Banach-Mazur games with $\omega$-regular winning conditions always have positional winning strategies, and winning positions for finite Banach-Mazur games with Muller winning condition are computable in polynomial time.
Cite as

Erich Graedel. Banach-Mazur Games on Graphs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 364-382, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{graedel:LIPIcs.FSTTCS.2008.1768,
  author =	{Graedel, Erich},
  title =	{{Banach-Mazur Games on Graphs}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{364--382},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1768},
  URN =		{urn:nbn:de:0030-drops-17684},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1768},
  annote =	{Keywords: Games, strategies, determinacy, positional determinacy, definability, complexity}
}
  • Refine by Author
  • 8 Grädel, Erich
  • 3 Naaf, Matthias
  • 2 Mrkonjić, Lovro
  • 1 Bizière, Clotilde
  • 1 Brinke, Sophie
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Finite Model Theory
  • 1 Mathematics of computing → Combinatorics
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Logic

  • Refine by Keyword
  • 3 Finite Model Theory
  • 3 Semiring semantics
  • 2 elementary equivalence
  • 1 Absorptive Semirings
  • 1 Algebra
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 2 2008
  • 2 2019
  • 2 2021
  • 1 2020
  • 1 2022
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact