50 Search Results for "Dam, Mads"

Volume

LIPIcs, Volume 82

26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

CSL 2017, August 20-24, 2017, Stockholm, Sweden

Editors: Valentin Goranko and Mads Dam

Document
DOI: 10.4230/LIPIcs.CSL.2026.15
Cyclic Proof Theory of Generalised Inductive Definitions

Authors: Gianluca Curzi and Lukas Melgaard

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We study cyclic proof systems for μPA, an extension of Peano arithmetic by generalised inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic Π^1_2-CA₀ by Möllerfeld. The main result of this paper is that cyclic and inductive μPA have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam’s systems for first-order μ-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within Π^1_2-CA₀, leveraging Möllerfeld’s conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem. As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for μPA prove the same theorems. This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson’s Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.
Cite as

Gianluca Curzi and Lukas Melgaard. Cyclic Proof Theory of Generalised Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{curzi_et_al:LIPIcs.CSL.2026.15,
  author =	{Curzi, Gianluca and Melgaard, Lukas},
  title =	{{Cyclic Proof Theory of Generalised Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.15},
  URN =		{urn:nbn:de:0030-drops-254399},
  doi =		{10.4230/LIPIcs.CSL.2026.15},
  annote =	{Keywords: cyclic proofs, positive inductive definitions, arithmetic, fixed points, proof theory, reset proof systems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.23
A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
Cite as

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
  author =	{Bandukara, Mohamed H. and Tzevelekos, Nikos},
  title =	{{A Logic for Fresh Labelled Transition Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.23},
  URN =		{urn:nbn:de:0030-drops-254478},
  doi =		{10.4230/LIPIcs.CSL.2026.23},
  annote =	{Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.29
Linear Logic Using Negative Connectives

Authors: Dale Miller

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
In linear logic, the invertibility of a connective’s right-introduction rule is equivalent to the non-invertibility of its left-introduction rule. This duality motivates the concept of polarity: a connective is termed negative if its right-introduction rule is invertible, and positive otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes of goal-reduction and backchaining, respectively. These phases are formalized here using the framework of multifocused proofs. We analyze linear logic by dissecting it into three sublogics: L₀ (first-order intuitionistic logic with conjunction, implication, and universal quantification); L₁ (an extension of L₀ incorporating linear implication which preserves its intuitionistic nature); and L₂ (which includes multiplicative falsity ⊥ and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of L₀ and L₁. While multifocused proofs of L₂ sequents can accommodate parallel applications of left-introduction rules, proofs of L₀ and L₁ sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic.
Cite as

Dale Miller. Linear Logic Using Negative Connectives. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{miller:LIPIcs.FSCD.2025.29,
  author =	{Miller, Dale},
  title =	{{Linear Logic Using Negative Connectives}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.29},
  URN =		{urn:nbn:de:0030-drops-236442},
  doi =		{10.4230/LIPIcs.FSCD.2025.29},
  annote =	{Keywords: Linear logic, multifocused proofs, sequent calculus}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.21
An Expressive Trace Logic for Recursive Programs

Authors: Dilian Gurov and Reiner Hähnle

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.
Cite as

Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gurov_et_al:LIPIcs.FSCD.2025.21,
  author =	{Gurov, Dilian and H\"{a}hnle, Reiner},
  title =	{{An Expressive Trace Logic for Recursive Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.21},
  URN =		{urn:nbn:de:0030-drops-236360},
  doi =		{10.4230/LIPIcs.FSCD.2025.21},
  annote =	{Keywords: Denotational semantics, compositional semantics, program specification, compositional verification, fixed point logic, trace logic}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2017
LIPIcs, Volume 82, CSL'17, Complete Volume

Authors: Valentin Goranko and Mads Dam

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

Abstract
LIPIcs, Volume 82, CSL'17, Complete Volume
Cite as

26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{goranko_et_al:LIPIcs.CSL.2017,
  title =	{{LIPIcs, Volume 82, CSL'17, Complete Volume}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017},
  URN =		{urn:nbn:de:0030-drops-78103},
  doi =		{10.4230/LIPIcs.CSL.2017},
  annote =	{Keywords: Conference Proceedings, Software/Program Verification, Formal Definitions and Theory, Language Constructs and Features, Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2017.0
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers

Authors: Valentin Goranko and Mads Dam

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
Cite as

26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{goranko_et_al:LIPIcs.CSL.2017.0,
  author =	{Goranko, Valentin and Dam, Mads},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{0:i--0:xviii},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.0},
  URN =		{urn:nbn:de:0030-drops-76671},
  doi =		{10.4230/LIPIcs.CSL.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.1
The Ackermann Award 2017

Authors: Anuj Dawar and Daniel Leivant

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

Abstract
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2017 edition of the award.
Cite as

Anuj Dawar and Daniel Leivant. The Ackermann Award 2017. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2017.1,
  author =	{Dawar, Anuj and Leivant, Daniel},
  title =	{{The Ackermann Award 2017}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{1:1--1:4},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.1},
  URN =		{urn:nbn:de:0030-drops-76938},
  doi =		{10.4230/LIPIcs.CSL.2017.1},
  annote =	{Keywords: Ackermann Award, jury report, citation}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.2
Schema Mappings: Structural Properties and Limits (Invited Talk)

Authors: Phokion G. Kolaitis

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

Abstract
A schema mapping is a high-level specification of the relationship between two database schemas. For the past fifteen years, schema mappings have played an essential role in the modeling and analysis of important data inter-operability tasks, such as data exchange and data integration. Syntactically, schema mappings are expressed in some schema-mapping language, which, typically, is a fragment of first-order logic or second-order logic. In the first part of the talk, we will introduce the main schema-mapping languages, will discuss the fundamental structural properties of these languages, and will then use these structural properties to obtain characterizations of various schema-mapping languages in the spirit of abstract model theory. In the second part of the talk, we will examine schema mappings from a dynamic viewpoint by considering sequences of schema mappings and studying the convergence properties of such sequences. To this effect, we will introduce a metric space that is based on a natural notion of distance between sets of database instances and will investigate pointwise limits and uniform limits of sequences of schema mappings. Among other findings, it will turn out that the completion of this metric space can be described in terms of graph limits arising from converging sequences of homomorphism densities.
Cite as

Phokion G. Kolaitis. Schema Mappings: Structural Properties and Limits (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kolaitis:LIPIcs.CSL.2017.2,
  author =	{Kolaitis, Phokion G.},
  title =	{{Schema Mappings: Structural Properties and Limits}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{2:1--2: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.2},
  URN =		{urn:nbn:de:0030-drops-76707},
  doi =		{10.4230/LIPIcs.CSL.2017.2},
  annote =	{Keywords: logic and databases, schema mappings, data exchange, metric spaces}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.3
First-Order Interpolation and Grey Areas of Proofs (Invited Talk)

Authors: Laura Kovács

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

Abstract
Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. In this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the “grey area” of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants. While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this talk we therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems - any such proof system should deal with formulas of arbitrary quantifier complexity.
Cite as

Laura Kovács. First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.CSL.2017.3,
  author =	{Kov\'{a}cs, Laura},
  title =	{{First-Order Interpolation and Grey Areas of Proofs}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{3:1--3: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.3},
  URN =		{urn:nbn:de:0030-drops-76912},
  doi =		{10.4230/LIPIcs.CSL.2017.3},
  annote =	{Keywords: theorem proving, interpolation, proof transformations, constraint solving, program analysis}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.4
Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)

Authors: Stephan Kreutzer

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

Abstract
The model-checking problem for a logic LLL is the problem of decidig for a given formula phi in LLL and structure AA whether the formula is true in the structure, i.e. whether AA models phi. Model-checking for logics such as First-Order Logic (FO) or Monadic Second-Order Logic (MSO) has been studied intensively in the literature, especially in the context of algorithmic meta-theorems within the framework of parameterized complexity. However, in the past the focus of this line of research was model-checking on classes of sparse graphs, e.g. planar graphs, graph classes excluding a minor or classes which are nowhere dense. By now, the complexity of first-order model-checking on sparse classes of graphs is completely understood. Hence, current research now focusses mainly on classes of dense graphs. In this talk we will briefly review the known results on sparse classes of graphs and explain the complete classification of classes of sparse graphs on which first-order model-checking is tractable. In the second part we will then focus on recent and ongoing research analysing the complexity of first-order model-checking on classes of dense graphs.
Cite as

Stephan Kreutzer. Current Trends and New Perspectives for First-Order Model Checking (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kreutzer:LIPIcs.CSL.2017.4,
  author =	{Kreutzer, Stephan},
  title =	{{Current Trends and New Perspectives for First-Order Model Checking}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{4:1--4:5},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.4},
  URN =		{urn:nbn:de:0030-drops-77095},
  doi =		{10.4230/LIPIcs.CSL.2017.4},
  annote =	{Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, Model-Checking, Logical Approaches in Graph Theory}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.5
Arithmetic Circuits: An Overview (Invited Talk)

Authors: Meena Mahajan

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

Abstract
This talk reviews recent developments in algebraic complexity theory. It outlines some major results concerning structure, completeness, closure, and lower bounds. It describes some techniques that have been central to obtaining these results, including extreme depth reduction, partial derivatives, and padding.
Cite as

Meena Mahajan. Arithmetic Circuits: An Overview (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{mahajan:LIPIcs.CSL.2017.5,
  author =	{Mahajan, Meena},
  title =	{{Arithmetic Circuits: An Overview}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{5:1--5: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.5},
  URN =		{urn:nbn:de:0030-drops-76858},
  doi =		{10.4230/LIPIcs.CSL.2017.5},
  annote =	{Keywords: algebraic complexity, circuits, formulas, branching programs, determinant, permanent}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.6
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.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
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.7
Symbolic Automata Theory with Applications (Invited Talk)

Authors: Margus Veanes

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

Abstract
Symbolic automata extend classic finite state automata by allowing transitions to carry predicates over rich alphabet theories. The key algorithmic difference to classic automata is the ability to efficiently operate over very large or infinite alphabets. In this talk we give an overview of what is currently known about symbolic automata, what their main applications are, and what challenges arise when reasoning about them. We also discuss some of the open problems and research directions in symbolic automata theory.
Cite as

Margus Veanes. Symbolic Automata Theory with Applications (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 7:1-7:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{veanes:LIPIcs.CSL.2017.7,
  author =	{Veanes, Margus},
  title =	{{Symbolic Automata Theory with Applications}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{7:1--7:3},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.7},
  URN =		{urn:nbn:de:0030-drops-76872},
  doi =		{10.4230/LIPIcs.CSL.2017.7},
  annote =	{Keywords: automaton, transducer, symbolic}
}
  • Refine by Type
  • 49 Document/PDF
  • 5 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 2 2026
  • 3 2025
  • 45 2017

  • Refine by Author
  • 2 Boudou, Joseph
  • 2 Dam, Mads
  • 2 Ghica, Dan R.
  • 2 Goranko, Valentin
  • 2 Grädel, Erich
  • Show More...

  • Refine by Series/Journal
  • 49 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Proof theory
  • 1 Theory of computation → Denotational semantics
  • Show More...

  • Refine by Keyword
  • 2 Linear logic
  • 2 first-order logic
  • 2 fixed points
  • 2 proof theory
  • 2 trees
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact