13 Search Results for "Neider, Daniel"

Document
DOI: 10.4230/DagRep.15.2.1
Logic and Neural Networks (Dagstuhl Seminar 25061)

Authors: Vaishak Belle, Michael Benedikt, Dana Drachsler-Cohen, Daniel Neider, and Tom Yuviler

Published in: Dagstuhl Reports, Volume 15, Issue 2 (2025)

Abstract
Logic and learning are central to Computer Science, and in particular to AI-related research. Already Alan Turing envisioned in his 1950 "Computing Machinery and Intelligence" paper a combination of statistical (ab initio) machine learning and an "unemotional" symbolic language such as logic. The combination of logic and learning has received new impetus from the spectacular success of deep learning systems. This report documents the program and the outcomes of Dagstuhl Seminar 25061 "Logic and Neural Networks". The goal of this Dagstuhl Seminar was to bring together researchers from various communities related to utilizing logical constraints in deep learning and to create bridges between them via the exchange of ideas. The seminar focused on a set of interrelated topics: enforcement of constraints on neural networks, verifying logical constraints on neural networks, training using logic to supplement traditional supervision, and explanation and approximation via logic. This Dagstuhl Seminar aimed not at studying these areas as separate components, but in exploring common techniques among them as well as connections to other communities in machine learning that share the same broad goals. The seminar format consisted of long and short talks, as well as breakout sessions. We summarize the motivations and proceedings of the seminar, and report on the abstracts of the talks and the results of the breakout sessions.
Cite as

Vaishak Belle, Michael Benedikt, Dana Drachsler-Cohen, Daniel Neider, and Tom Yuviler. Logic and Neural Networks (Dagstuhl Seminar 25061). In Dagstuhl Reports, Volume 15, Issue 2, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{belle_et_al:DagRep.15.2.1,
  author =	{Belle, Vaishak and Benedikt, Michael and Drachsler-Cohen, Dana and Neider, Daniel and Yuviler, Tom},
  title =	{{Logic and Neural Networks (Dagstuhl Seminar 25061)}},
  pages =	{1--20},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{15},
  number =	{2},
  editor =	{Belle, Vaishak and Benedikt, Michael and Drachsler-Cohen, Dana and Neider, Daniel and Yuviler, Tom},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.2.1},
  URN =		{urn:nbn:de:0030-drops-230939},
  doi =		{10.4230/DagRep.15.2.1},
  annote =	{Keywords: machine learning, learning theory, logic, computational complexity, databases, verification, safety}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.77
Minimization of Deterministic Finite Automata Modulo the Edit Distance

Authors: Jakub Michaliszyn and Jan Otop

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We propose a novel approach to minimization of deterministic finite automata (DFA), in which the DFA is further minimized at the expense of relaxing equality of languages to merely a similarity. As the notion of similarity of languages, we consider the edit distance between languages ℒ, ℒ', i.e., the minimal number of edits necessary to transform any word from ℒ to some word from ℒ' and vice versa. In this paper we address two problems: minimization up to a predetermined edit distance given in the input, and minimization up to a bounded edit distance, in which there has to be an upper bound on the number of edits, but it is not specified. We show the first problem to be PSpace {}-complete and that the second problem is in Σ₂^p, and both NP-hard and coNP-hard. We show that if we limit how many strongly connected components can be visited by a single run (i.e., bounded SCC-depth), the problem becomes NP-complete. We also establish maximal subclasses of DFA over which minimization up to a bounded edit distance can be performed in polynomial time. Additionally, we provide a succinct overview of alternative metrics for assessing language similarity.
Cite as

Jakub Michaliszyn and Jan Otop. Minimization of Deterministic Finite Automata Modulo the Edit Distance. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 77:1-77:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.MFCS.2025.77,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Minimization of Deterministic Finite Automata Modulo the Edit Distance}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{77:1--77:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.77},
  URN =		{urn:nbn:de:0030-drops-241843},
  doi =		{10.4230/LIPIcs.MFCS.2025.77},
  annote =	{Keywords: automata theory, automata minimization, edit distance}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.66
Deciding Regular Games: a Playground for Exponential Time Algorithms

Authors: Zihui Liang, Bakh Khoussainov, and Mingyu Xiao

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Regular games form a well-established class of games for analysis and synthesis of reactive systems. They include colored Muller games, McNaughton games, Muller games, Rabin games, and Streett games. These games are played on directed graphs G where Player 0 and Player 1 play by generating an infinite path ρ through the graph. The winner is determined by specifications put on the set X of vertices in ρ that occur infinitely often. These games are determined, enabling the partitioning of G into two sets Win₀ and Win₁ of winning positions for Player 0 and Player 1, respectively. Numerous algorithms exist that decide instances of regular games, e.g., Muller games, by computing Win₀ and Win₁. In this paper we aim to find general principles for designing uniform algorithms that decide all regular games. For this we utilize various recursive and dynamic programming algorithms that leverage standard notions such as subgames and traps. Importantly, we show that our techniques improve or match the performances of existing algorithms for many instances of regular games.
Cite as

Zihui Liang, Bakh Khoussainov, and Mingyu Xiao. Deciding Regular Games: a Playground for Exponential Time Algorithms. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 66:1-66:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liang_et_al:LIPIcs.MFCS.2025.66,
  author =	{Liang, Zihui and Khoussainov, Bakh and Xiao, Mingyu},
  title =	{{Deciding Regular Games: a Playground for Exponential Time Algorithms}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{66:1--66:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.66},
  URN =		{urn:nbn:de:0030-drops-241732},
  doi =		{10.4230/LIPIcs.MFCS.2025.66},
  annote =	{Keywords: Regular games, colored Muller games, Rabin games, McNaughton games, Muller games, deciding games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.19
Time for Timed Monitorability

Authors: Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann

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

Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
  author =	{Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
  title =	{{Time for Timed Monitorability}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{19:1--19:20},
  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.19},
  URN =		{urn:nbn:de:0030-drops-239690},
  doi =		{10.4230/LIPIcs.CONCUR.2025.19},
  annote =	{Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.34
New Fault Domains for Conformance Testing of Finite State Machines

Authors: Frits Vaandrager and Ivo Melse

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

Abstract
A fault domain reflects a tester’s assumptions about faults that may occur in an implementation and that need to be detected during testing. A fault domain that has been widely studied in the literature on black-box conformance testing is the class of finite state machines (FSMs) with at most m states. Numerous strategies for generating test suites have been proposed that guarantee fault coverage for this class. These so-called m-complete test suites grow exponentially in m-n, where n is the number of states of the specification, so one can only run them for small values of m-n. But the assumption that m-n is small is not realistic in practice. In his seminal paper from 1964, Hennie raised the challenge to design checking experiments in which the number of states may increase appreciably. In order to solve this long-standing open problem, we propose (much larger) fault domains that capture the assumption that all states in an implementation can be reached by first performing a sequence from some set A (typically a state cover for the specification), followed by k arbitrary inputs, for some small k. The number of states of FSMs in these fault domains grows exponentially in k. We present a sufficient condition for k-A-completeness of test suites with respect to these fault domains. Our condition implies k-A-completeness of two prominent m-complete test suite generation strategies, the Wp and HSI methods. Thus these strategies are complete for much larger fault domains than those for which they were originally designed, and thereby solve Hennie’s challenge. We show that three other prominent m-complete methods (H, SPY and SPYH) do not always generate k-A-complete test suites.
Cite as

Frits Vaandrager and Ivo Melse. New Fault Domains for Conformance Testing of Finite State Machines. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vaandrager_et_al:LIPIcs.CONCUR.2025.34,
  author =	{Vaandrager, Frits and Melse, Ivo},
  title =	{{New Fault Domains for Conformance Testing of Finite State Machines}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{34:1--34:22},
  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.34},
  URN =		{urn:nbn:de:0030-drops-239843},
  doi =		{10.4230/LIPIcs.CONCUR.2025.34},
  annote =	{Keywords: conformance testing, finite state machines, Mealy machines, apartness, observation tree, fault domains, k-A-complete test suites}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.24
Learning Tree Pattern Transformations

Authors: Daniel Neider, Leif Sabellek, Johannes Schmidt, Fabian Vehlken, and Thomas Zeume

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
Explaining why and how a tree t structurally differs from another tree t^⋆ is a question that is encountered throughout computer science, including in understanding tree-structured data such as XML or JSON data. In this article, we explore how to learn explanations for structural differences between pairs of trees from sample data: suppose we are given a set {(t₁, t₁^⋆),… , (t_n, t_n^⋆)} of pairs of labelled, ordered trees; is there a small set of rules that explains the structural differences between all pairs (t_i, t_i^⋆)? This raises two research questions: (i) what is a good notion of "rule" in this context?; and (ii) how can sets of rules explaining a data set be learned algorithmically? We explore these questions from the perspective of database theory by (1) introducing a pattern-based specification language for tree transformations; (2) exploring the computational complexity of variants of the above algorithmic problem, e.g. showing NP-hardness for very restricted variants; and (3) discussing how to solve the problem for data from CS education research using SAT solvers.
Cite as

Daniel Neider, Leif Sabellek, Johannes Schmidt, Fabian Vehlken, and Thomas Zeume. Learning Tree Pattern Transformations. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{neider_et_al:LIPIcs.ICDT.2025.24,
  author =	{Neider, Daniel and Sabellek, Leif and Schmidt, Johannes and Vehlken, Fabian and Zeume, Thomas},
  title =	{{Learning Tree Pattern Transformations}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.24},
  URN =		{urn:nbn:de:0030-drops-229652},
  doi =		{10.4230/LIPIcs.ICDT.2025.24},
  annote =	{Keywords: Tree pattern transformations, learning from positive examples, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.4
Learning Aggregate Queries Defined by First-Order Logic with Counting

Authors: Steffen van Bergerem and Nicole Schweikardt

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
In the logical framework introduced by Grohe and Turán (TOCS 2004) for Boolean classification problems, the instances to classify are tuples from a logical structure, and Boolean classifiers are described by parametric models based on logical formulas. This is a specific scenario for supervised passive learning, where classifiers should be learned based on labelled examples. Existing results in this scenario focus on Boolean classification. This paper presents learnability results beyond Boolean classification. We focus on multiclass classification problems where the task is to assign input tuples to arbitrary integers. To represent such integer-valued classifiers, we use aggregate queries specified by an extension of first-order logic with counting terms called FOC₁. Our main result shows the following: given a database of polylogarithmic degree, within quasi-linear time, we can build an index structure that makes it possible to learn FOC₁-definable integer-valued classifiers in time polylogarithmic in the size of the database and polynomial in the number of training examples.
Cite as

Steffen van Bergerem and Nicole Schweikardt. Learning Aggregate Queries Defined by First-Order Logic with Counting. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.ICDT.2025.4,
  author =	{van Bergerem, Steffen and Schweikardt, Nicole},
  title =	{{Learning Aggregate Queries Defined by First-Order Logic with Counting}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.4},
  URN =		{urn:nbn:de:0030-drops-229457},
  doi =		{10.4230/LIPIcs.ICDT.2025.4},
  annote =	{Keywords: Supervised learning, multiclass classification problems, counting logic}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.19
The Complexity of Learning LTL, CTL and ATL Formulas

Authors: Benjamin Bordais, Daniel Neider, and Rajarshi Roy

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We consider the problem of learning temporal logic formulas from examples of system behavior. Learning temporal properties has crystallized as an effective means to explain complex temporal behaviors. Several efficient algorithms have been designed for learning temporal formulas. However, the theoretical understanding of the complexity of the learning decision problems remains largely unexplored. To address this, we study the complexity of the passive learning problems of three prominent temporal logics, Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL) and several of their fragments. We show that learning formulas with unbounded occurrences of binary operators is NP-complete for all of these logics. On the other hand, when investigating the complexity of learning formulas with bounded occurrences of binary operators, we exhibit discrepancies between the complexity of learning LTL, CTL and ATL formulas (with a varying number of agents).
Cite as

Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The Complexity of Learning LTL, CTL and ATL Formulas. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.STACS.2025.19,
  author =	{Bordais, Benjamin and Neider, Daniel and Roy, Rajarshi},
  title =	{{The Complexity of Learning LTL, CTL and ATL Formulas}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.19},
  URN =		{urn:nbn:de:0030-drops-228441},
  doi =		{10.4230/LIPIcs.STACS.2025.19},
  annote =	{Keywords: Temporal logic, passive learning, complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.8
The Parameterized Complexity of Learning Monadic Second-Order Logic

Authors: Steffen van Bergerem, Martin Grohe, and Nina Runde

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Within the model-theoretic framework for supervised learning introduced by Grohe and Turán (TOCS 2004), we study the parameterized complexity of learning concepts definable in monadic second-order logic (MSO). We show that the problem of learning an MSO-definable concept from a training sequence of labeled examples is fixed-parameter tractable on graphs of bounded clique-width, and that it is hard for the parameterized complexity class para-NP on general graphs. It turns out that an important distinction to be made is between 1-dimensional and higher-dimensional concepts, where the instances of a k-dimensional concept are k-tuples of vertices of a graph. For the higher-dimensional case, we give a learning algorithm that is fixed-parameter tractable in the size of the graph, but not in the size of the training sequence, and we give a hardness result showing that this is optimal. By comparison, in the 1-dimensional case, we obtain an algorithm that is fixed-parameter tractable in both.
Cite as

Steffen van Bergerem, Martin Grohe, and Nina Runde. The Parameterized Complexity of Learning Monadic Second-Order Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.CSL.2025.8,
  author =	{van Bergerem, Steffen and Grohe, Martin and Runde, Nina},
  title =	{{The Parameterized Complexity of Learning Monadic Second-Order Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.8},
  URN =		{urn:nbn:de:0030-drops-227651},
  doi =		{10.4230/LIPIcs.CSL.2025.8},
  annote =	{Keywords: monadic second-order definable concept learning, agnostic probably approximately correct learning, parameterized complexity, clique-width, fixed-parameter tractable, Boolean classification, supervised learning, monadic second-order logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.74
Optimally Resilient Strategies in Pushdown Safety Games

Authors: Daniel Neider, Patrick Totzke, and Martin Zimmermann

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

Abstract
Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that computing optimally resilient strategies only incurs a polynomial overhead over solving classical games. This paper studies safety games with disturbances played on infinite arenas induced by pushdown systems. We show how to compute optimally resilient strategies in triply-exponential time. For the subclass of safety games played on one-counter configuration graphs, we show that determining the degree of resilience of the initial configuration is PSPACE-complete and that optimally resilient strategies can be computed in doubly-exponential time.
Cite as

Daniel Neider, Patrick Totzke, and Martin Zimmermann. Optimally Resilient Strategies in Pushdown Safety Games. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{neider_et_al:LIPIcs.MFCS.2020.74,
  author =	{Neider, Daniel and Totzke, Patrick and Zimmermann, Martin},
  title =	{{Optimally Resilient Strategies in Pushdown Safety Games}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{74:1--74:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.74},
  URN =		{urn:nbn:de:0030-drops-127432},
  doi =		{10.4230/LIPIcs.MFCS.2020.74},
  annote =	{Keywords: Controller Synthesis, Infinite Games, Resilient Strategies, Pushdown Games}
}
Document
DOI: 10.4230/DagRep.9.9.1
Logic and Learning (Dagstuhl Seminar 19361)

Authors: Michael Benedikt, Kristian Kersting, Phokion G. Kolaitis, and Daniel Neider

Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)

Abstract
The goal of building truly intelligent systems has forever been a central problem in computer science. While logic-based approaches of yore have had their successes and failures, the era of machine learning, specifically deep learning is also coming upon significant challenges. There is a growing consensus that the inductive reasoning and complex, high-dimensional pattern recognition capabilities of deep learning models need to be combined with symbolic (even programmatic), deductive capabilities traditionally developed in the logic and automated reasoning communities in order to achieve the next step towards building intelligent systems, including making progress at the frontier of hard problems such as explainable AI. However, these communities tend to be quite separate and interact only minimally, often at odds with each other upon the subject of the ``correct approach'' to AI. This report documents the efforts of Dagstuhl Seminar 19361 on ``Logic and Learning'' to bring these communities together in order to: (i) bridge the research efforts between them and foster an exchange of ideas in order to create unified formalisms and approaches that bear the advantages of both research methodologies; (ii) review and analyse the progress made across both communities; (iii) understand the subtleties and difficulties involved in solving hard problems using both perspectives; (iv) make attempts towards a consensus on what the hard problems are and what the elements of good solutions to these problems would be. The three focal points of the seminar were the strands of ``Logic for Machine Learning'', ``Machine Learning for Logic'', and ``Logic vs. Machine Learning''. The seminar format consisted of long and short talks, as well as breakout sessions. We summarise the motivations and proceedings of the seminar, and report on the abstracts of the talks and the results of the breakout sessions.
Cite as

Michael Benedikt, Kristian Kersting, Phokion G. Kolaitis, and Daniel Neider. Logic and Learning (Dagstuhl Seminar 19361). In Dagstuhl Reports, Volume 9, Issue 9, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{benedikt_et_al:DagRep.9.9.1,
  author =	{Benedikt, Michael and Kersting, Kristian and Kolaitis, Phokion G. and Neider, Daniel},
  title =	{{Logic and Learning (Dagstuhl Seminar 19361)}},
  pages =	{1--22},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Benedikt, Michael and Kersting, Kristian and Kolaitis, Phokion G. and Neider, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.9.1},
  URN =		{urn:nbn:de:0030-drops-118425},
  doi =		{10.4230/DagRep.9.9.1},
  annote =	{Keywords: Artificial Intelligence, Automated reasoning, Databases, Deep Learning, Inductive Logic Programming, Logic, Logic and Learning, Logic for Machine Learning, Logic vs. Machine Learning, Machine Learning, Machine Learning for Logic, Neurosymbolic methods}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.34
Synthesizing Optimally Resilient Controllers

Authors: Daniel Neider, Alexander Weinert, and Martin Zimmermann

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

Abstract
Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermittent disturbances. In this extended framework, one is interested in computing optimally resilient strategies, i.e., strategies that are resilient against as many disturbances as possible. Dallal, Neider, and Tabuada showed how to compute such strategies for safety specifications. In this work, we compute optimally resilient strategies for a much wider range of winning conditions and show that they do not require more memory than winning strategies in the classical model. Our algorithms only have a polynomial overhead in comparison to the ones computing winning strategies. In particular, for parity conditions optimally resilient strategies are positional and can be computed in quasipolynomial time.
Cite as

Daniel Neider, Alexander Weinert, and Martin Zimmermann. Synthesizing Optimally Resilient Controllers. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{neider_et_al:LIPIcs.CSL.2018.34,
  author =	{Neider, Daniel and Weinert, Alexander and Zimmermann, Martin},
  title =	{{Synthesizing Optimally Resilient Controllers}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.34},
  URN =		{urn:nbn:de:0030-drops-97010},
  doi =		{10.4230/LIPIcs.CSL.2018.34},
  annote =	{Keywords: Controller Synthesis, Infinite Games, Resilient Strategies, Disturbances}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.10
Robust Linear Temporal Logic

Authors: Paulo Tabuada and Daniel Neider

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
Although it is widely accepted that every system should be robust, in the sense that "small" violations of environment assumptions should lead to "small" violations of system guarantees, it is less clear how to make this intuitive notion of robustness mathematically precise. In this paper, we address the problem of how to specify robustness in temporal logic. Our solution consists of a robust version of the Linear Temporal Logic (LTL) fragment that only contains the always and eventually temporal operators.
Cite as

Paulo Tabuada and Daniel Neider. Robust Linear Temporal Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{tabuada_et_al:LIPIcs.CSL.2016.10,
  author =	{Tabuada, Paulo and Neider, Daniel},
  title =	{{Robust Linear Temporal Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.10},
  URN =		{urn:nbn:de:0030-drops-65508},
  doi =		{10.4230/LIPIcs.CSL.2016.10},
  annote =	{Keywords: Linear Temporal Logic, Robustness}
}
  • Refine by Type
  • 13 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 9 2025
  • 2 2020
  • 1 2018
  • 1 2016

  • Refine by Author
  • 7 Neider, Daniel
  • 3 Zimmermann, Martin
  • 2 Benedikt, Michael
  • 2 van Bergerem, Steffen
  • 1 Belle, Vaishak
  • Show More...

  • Refine by Series/Journal
  • 11 LIPIcs
  • 2 DagRep

  • Refine by Classification
  • 3 Computing methodologies → Logical and relational learning
  • 3 Computing methodologies → Supervised learning
  • 2 Theory of computation
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Complexity theory and logic
  • Show More...

  • Refine by Keyword
  • 2 Controller Synthesis
  • 2 Infinite Games
  • 2 Resilient Strategies
  • 2 computational complexity
  • 1 Artificial Intelligence
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact