22 Search Results for "Groote, Jan Friso"

Document
DOI: 10.4230/LIPIcs.CSL.2026.44
Minimal DFAs Witnessing Language Inequivalence

Authors: Jan Martens

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

Abstract
We study small witnesses for the inequivalence of two regular languages. A natural witness is a distinguishing word, e.g. a word in exactly one of the two languages. We propose using more succinct witnesses in the form of witnessing DFAs. A witnessing DFA recognizes a subset of one of the languages and contains at least one distinguishing word. In this way the DFA expresses behaviour contained in the first language but not the second. We show witnessing DFAs can be used to present more concise witnesses for the inequivalence of two regular languages. We show that the decision problem for the existence of a witnessing DFA of certain size is NP-complete in general, and in P in the special case of unary DFAs. Besides these computational aspects, we study structural properties of witnessing DFAs. Not all languages can be a minimal witness. It turns out that minimal witnesses are exactly the languages that are not decomposable in the union of languages with smaller state-complexity, the so-called prime languages as studied earlier by Kupferman and Mosheiff.
Cite as

Jan Martens. Minimal DFAs Witnessing Language Inequivalence. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 44:1-44:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{martens:LIPIcs.CSL.2026.44,
  author =	{Martens, Jan},
  title =	{{Minimal DFAs Witnessing Language Inequivalence}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{44:1--44:16},
  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.44},
  URN =		{urn:nbn:de:0030-drops-254691},
  doi =		{10.4230/LIPIcs.CSL.2026.44},
  annote =	{Keywords: Deterministic Finite Automata, Language Inequivalence, DFA decomposition, Prime languages}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.56
Negated String Containment Is Decidable

Authors: Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál

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

Abstract
We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate ¬Contains(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.
Cite as

Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. Negated String Containment Is Decidable. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 56:1-56:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.MFCS.2025.56,
  author =	{Havlena, Vojt\v{e}ch and He\v{c}ko, Michal and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej},
  title =	{{Negated String Containment Is Decidable}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{56:1--56:20},
  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.56},
  URN =		{urn:nbn:de:0030-drops-241631},
  doi =		{10.4230/LIPIcs.MFCS.2025.56},
  annote =	{Keywords: not-contains, string constraints, word combinatorics, primitive word}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.31
Compositional Reasoning for Parametric Probabilistic Automata

Authors: Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen

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

Abstract
We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.
Cite as

Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen. Compositional Reasoning for Parametric Probabilistic Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mertens_et_al:LIPIcs.CONCUR.2025.31,
  author =	{Mertens, Hannah and Quatmann, Tim and Katoen, Joost-Pieter},
  title =	{{Compositional Reasoning for Parametric Probabilistic Automata}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{31:1--31: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.31},
  URN =		{urn:nbn:de:0030-drops-239810},
  doi =		{10.4230/LIPIcs.CONCUR.2025.31},
  annote =	{Keywords: Verification, Probabilistic systems, Assume-guarantee reasoning, Parametric Probabilistic Automata, Parameter synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.35
From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases

Authors: Rowin Versteeg, Valentina Castiglioni, and Bas Luttik

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

Abstract
We consider process algebras with inaction, action prefix, non-deterministic choice and interleaving parallel composition modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum, and study the existence of finite bases (i.e., finite sound and complete axiomatisations) for these algebras. We prove that if the alphabet of actions is infinite and the behavioural equivalence is either simulation equivalence or trace equivalence, then a finite basis exists and is obtained by extending the known ground-complete axiomatisations for these behavioural equivalences. We prove that if the alphabet of actions is finite, then a finite basis does not exist for these equivalences. We also prove for all behavioural equivalences between ready simulation and completed traces there cannot exist a finite basis irrespective of the cardinality of the alphabet of actions (provided that it is non-empty). Finally, we prove that these results are maintained if the process algebra is extended with a constant for successful termination.
Cite as

Rowin Versteeg, Valentina Castiglioni, and Bas Luttik. From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{versteeg_et_al:LIPIcs.CONCUR.2025.35,
  author =	{Versteeg, Rowin and Castiglioni, Valentina and Luttik, Bas},
  title =	{{From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{35:1--35:18},
  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.35},
  URN =		{urn:nbn:de:0030-drops-239854},
  doi =		{10.4230/LIPIcs.CONCUR.2025.35},
  annote =	{Keywords: Equational basis, Parallel composition, Preorders, Equivalences, Linear time - branching time spectrum}
}
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.CONCUR.2025.20
Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement

Authors: Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino

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

Abstract
Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. We characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We present a compositional learning algorithm implementing these ideas, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments show that in more than 630 subject systems, CoalA delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.
Cite as

Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino. Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henry_et_al:LIPIcs.CONCUR.2025.20,
  author =	{Henry, L\'{e}o and Mousavi, Mohammad Reza and Neele, Thomas and Sammartino, Matteo},
  title =	{{Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{20:1--20: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.20},
  URN =		{urn:nbn:de:0030-drops-239700},
  doi =		{10.4230/LIPIcs.CONCUR.2025.20},
  annote =	{Keywords: Active learning, Compositional methods, Concurrency theory, Labelled transition systems, Formal methods}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.17
Just Verification of Mutual Exclusion Algorithms

Authors: Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck

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

Abstract
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements.
Cite as

Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck. Just Verification of Mutual Exclusion Algorithms. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanglabbeek_et_al:LIPIcs.CONCUR.2025.17,
  author =	{van Glabbeek, Rob and Luttik, Bas and Spronck, Myrthe S. C.},
  title =	{{Just Verification of Mutual Exclusion Algorithms}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{17:1--17:25},
  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.17},
  URN =		{urn:nbn:de:0030-drops-239670},
  doi =		{10.4230/LIPIcs.CONCUR.2025.17},
  annote =	{Keywords: Mutual exclusion, safe registers, regular registers, overlapping reads and writes, atomicity, safety, liveness, starvation freedom, justness, model checking, mCRL2}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.18
A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity

Authors: Jan Friso Groote and David N. Jansen

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

Abstract
We present a new O(mlog n) algorithm to calculate branching bisimulation equivalence, which is the finest commonly used behavioural equivalence on labelled transition systems that takes the internal action τ into account. This algorithm combines the simpler data structure of an earlier algorithm for Kripke structures (without action labels) with the memory-efficiency of a later algorithm partitioning sets of labelled transitions. It employs a particularly elegant four-way split of blocks of states, which refines a block under two splitters and isolates all new bottom states, simultaneously. Benchmark results show that this new algorithm outperforms the best known algorithm for branching bisimulation both in time and space.
Cite as

Jan Friso Groote and David N. Jansen. A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{groote_et_al:LIPIcs.CONCUR.2025.18,
  author =	{Groote, Jan Friso and Jansen, David N.},
  title =	{{A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{18:1--18:16},
  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.18},
  URN =		{urn:nbn:de:0030-drops-239688},
  doi =		{10.4230/LIPIcs.CONCUR.2025.18},
  annote =	{Keywords: Algorithm, Branching bisimulation, Partition refinement of states}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.32
Efficient Certified Reasoning for Binarized Neural Networks

Authors: Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Neural networks have emerged as essential components in safety-critical applications - these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value; they are particularly well-suited for safety-critical tasks because they retain much of the computational capacities of full-scale (floating-point or quantized) deep neural networks, but remain compatible with satisfiability solvers for qualitative verification and with model counters for quantitative reasoning. However, existing methods for BNN analysis suffer from either limited scalability or susceptibility to soundness errors, which hinders their applicability in real-world scenarios. In this work, we present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs. Our approach introduces a native representation of BNN constraints in a custom-designed solver for qualitative reasoning, and in an approximate model counter for quantitative reasoning. We further develop specialized proof generation and checking pipelines with native support for BNN constraint reasoning, ensuring trustworthiness for all of our verification results. Empirical evaluations on a BNN robustness verification benchmark suite demonstrate that our certified solving approach achieves a 9× speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a 218× speedup over the existing CNF-based baseline. In terms of coverage, our pipeline produces fully certified results for 99% and 86% of the qualitative and quantitative reasoning queries on BNNs, respectively. This is in sharp contrast to the best existing baselines which can fully certify only 62% and 4% of the queries, respectively.
Cite as

Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Efficient Certified Reasoning for Binarized Neural Networks. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2025.32,
  author =	{Yang, Jiong and Tan, Yong Kiam and Soos, Mate and Myreen, Magnus O. and Meel, Kuldeep S.},
  title =	{{Efficient Certified Reasoning for Binarized Neural Networks}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.32},
  URN =		{urn:nbn:de:0030-drops-237665},
  doi =		{10.4230/LIPIcs.SAT.2025.32},
  annote =	{Keywords: Neural network verification, proof certification, SAT solving, approximate model counting}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.12
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors: Rémy Cerda, Giulio Manzonetto, and Alexis Saurin

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

Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
  author =	{Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
  title =	{{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{12:1--12:20},
  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.12},
  URN =		{urn:nbn:de:0030-drops-236277},
  doi =		{10.4230/LIPIcs.FSCD.2025.12},
  annote =	{Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.3
Unsolvable Terms in Filter Models (Invited Talk)

Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell

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

Abstract
Intersection type theories (itt’s) and filter models, i.e. λ-calculus models generated by itt’s, are reviewed in full generality. In this framework, which subsumes most λ-calculus models in the literature based on Scott-continuous functions, we discuss the interpretation of unsolvable terms. We give a necessary, but not sufficient, condition on an itt for the interpretation of some unsolvable term to be non-trivial in the filter model it generates. This result is obtained building on a type theoretic characterisation of the fine structure of unsolvables.
Cite as

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell. Unsolvable Terms in Filter Models (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dezaniciancaglini_et_al:LIPIcs.FSCD.2025.3,
  author =	{Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Honsell, Furio},
  title =	{{Unsolvable Terms in Filter Models}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{3:1--3:24},
  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.3},
  URN =		{urn:nbn:de:0030-drops-236181},
  doi =		{10.4230/LIPIcs.FSCD.2025.3},
  annote =	{Keywords: \lambda-calculus, Intersection Types, Unsolvable Terms, Filter Models}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.138
Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Authors: Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Markov decision processes (MDPs) are a canonical model to reason about decision making within a stochastic environment. We study a fundamental class of infinite MDPs: one-counter MDPs (OC-MDPs). They extend finite MDPs via an associated counter taking natural values, thus inducing an infinite MDP over the set of configurations (current state and counter value). We consider two characteristic objectives: reaching a target state (state-reachability), and reaching a target state with counter value zero (selective termination). The synthesis problem for the latter is not known to be decidable and connected to major open problems in number theory. Furthermore, even seemingly simple strategies (e.g., memoryless ones) in OC-MDPs might be impossible to build in practice (due to the underlying infinite configuration space): we need finite, and preferably small, representations. To overcome these obstacles, we introduce two natural classes of concisely represented strategies based on a (possibly infinite) partition of counter values in intervals. For both classes, and both objectives, we study the verification problem (does a given strategy ensure a high enough probability for the objective?), and two synthesis problems (does there exist such a strategy?): one where the interval partition is fixed as input, and one where it is only parameterized. We develop a generic approach based on a compression of the induced infinite MDP that yields decidability in all cases, with all complexities within PSPACE.
Cite as

Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour. Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 138:1-138:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.ICALP.2025.138,
  author =	{Ajdar\'{o}w, Michal and Main, James C. A. and Novotn\'{y}, Petr and Randour, Mickael},
  title =	{{Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{138:1--138:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.138},
  URN =		{urn:nbn:de:0030-drops-235157},
  doi =		{10.4230/LIPIcs.ICALP.2025.138},
  annote =	{Keywords: one-counter Markov decision processes, randomised strategies, termination, reachability}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.12
Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Cite as

Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
  author =	{Ghanbari, Ali},
  title =	{{Automatic Goal Clone Detection in Rocq}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.12},
  URN =		{urn:nbn:de:0030-drops-233055},
  doi =		{10.4230/LIPIcs.ECOOP.2025.12},
  annote =	{Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.26
The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum

Authors: Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir

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

Abstract
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek’s branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.
Cite as

Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir. The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2025.26,
  author =	{Aceto, Luca and Achilleos, Antonis and Chalki, Aggeliki and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{26:1--26:18},
  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.26},
  URN =		{urn:nbn:de:0030-drops-227836},
  doi =		{10.4230/LIPIcs.CSL.2025.26},
  annote =	{Keywords: Characteristic formulae, prime formulae, bisimulation, simulation relations, modal logics, complexity theory, satisfiability}
}
Document
Survey
DOI: 10.4230/TGDK.1.1.12
Structural Summarization of Semantic Graphs Using Quotients

Authors: Ansgar Scherp, David Richerby, Till Blume, Michael Cochez, and Jannik Rau

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Graph summarization is the process of computing a compact version of an input graph while preserving chosen features of its structure. We consider semantic graphs where the features include edge labels and label sets associated with a vertex. Graph summaries are typically much smaller than the original graph. Applications that depend on the preserved features can perform their tasks on the summary, but much faster or with less memory overhead, while producing the same outcome as if they were applied on the original graph. In this survey, we focus on structural summaries based on quotients that organize vertices in equivalence classes of shared features. Structural summaries are particularly popular for semantic graphs and have the advantage of defining a precise graph-based output. We consider approaches and algorithms for both static and temporal graphs. A common example of quotient-based structural summaries is bisimulation, and we discuss this in detail. While there exist other surveys on graph summarization, to the best of our knowledge, we are the first to bring in a focused discussion on quotients, bisimulation, and their relation. Furthermore, structural summarization naturally connects well with formal logic due to the discrete structures considered. We complete the survey with a brief description of approaches beyond structural summaries.
Cite as

Ansgar Scherp, David Richerby, Till Blume, Michael Cochez, and Jannik Rau. Structural Summarization of Semantic Graphs Using Quotients. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{scherp_et_al:TGDK.1.1.12,
  author =	{Scherp, Ansgar and Richerby, David and Blume, Till and Cochez, Michael and Rau, Jannik},
  title =	{{Structural Summarization of Semantic Graphs Using Quotients}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{12:1--12:25},
  ISSN =	{2942-7517},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.12},
  URN =		{urn:nbn:de:0030-drops-194862},
  doi =		{10.4230/TGDK.1.1.12},
  annote =	{Keywords: graph summarization, quotients, stratified bisimulation}
}
  • Refine by Type
  • 22 Document/PDF
  • 15 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 13 2025
  • 4 2023
  • 1 2021
  • 2 2020
  • Show More...

  • Refine by Author
  • 6 Groote, Jan Friso
  • 3 Martens, Jan
  • 2 Aceto, Luca
  • 2 Achilleos, Antonis
  • 2 Ingólfsdóttir, Anna
  • Show More...

  • Refine by Series/Journal
  • 19 LIPIcs
  • 1 OASIcs
  • 1 TGDK
  • 1 DagSemProc

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 4 Theory of computation → Modal and temporal logics
  • 3 Software and its engineering → Formal software verification
  • 2 Theory of computation → Design and analysis of algorithms
  • 2 Theory of computation → Probabilistic computation
  • Show More...

  • Refine by Keyword
  • 2 λ-calculus
  • 1 Active learning
  • 1 Algorithm
  • 1 Assume-guarantee reasoning
  • 1 Behavioural Equivalence
  • 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