76 Search Results for "Meyer, Roland"

Volume

LIPIcs, Volume 85

28th International Conference on Concurrency Theory (CONCUR 2017)

CONCUR 2017, September 5-8, 2017, Berlin, Germany

Editors: Roland Meyer and Uwe Nestmann

Document
DOI: 10.4230/LIPIcs.LICS.2026.53
PVASS Reachability Is Decidable

Authors: Roland Guttenberg, Eren Keskin, and Roland Meyer

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.
Cite as

Roland Guttenberg, Eren Keskin, and Roland Meyer. PVASS Reachability Is Decidable. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 53:1-53:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{guttenberg_et_al:LIPIcs.LICS.2026.53,
  author =	{Guttenberg, Roland and Keskin, Eren and Meyer, Roland},
  title =	{{PVASS Reachability Is Decidable}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{53:1--53:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.53},
  URN =		{urn:nbn:de:0030-drops-268406},
  doi =		{10.4230/LIPIcs.LICS.2026.53},
  annote =	{Keywords: Pushdowns, Petri Nets, VASS, PVASS, Reachability, Decidability, Complexity}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.10
77 Shades of Grey

Authors: Quentin Bramas, Stéphane Devismes, Anaïs Durand, Pascal Lafourcade, and Anissa Lamani

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
Bruce Wayne contacted us to help him develop a new surveillance technology for dark environments such as caves, using a swarm of Unmanned Aerial Vehicles (UAVs), called Batdroids. A Batdroid has no chirality, limited visibility, and a perfect clock to synchronize with the others. A Batdroid can produce 77 shades of grey in dark mode and four colors in light mode. In this paper, we propose two algorithms using three Batdroids to perpetually explore a finite 3D grid modeling a cave. The first algorithm operates in darkness, uses 77 shades of grey, and requires visibility range one. The second operates in light, uses four colors and visibility range two. We also prove that three is the optimal number of Batdroids required to solve Bruce Wayne’s challenge.
Cite as

Quentin Bramas, Stéphane Devismes, Anaïs Durand, Pascal Lafourcade, and Anissa Lamani. 77 Shades of Grey. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bramas_et_al:LIPIcs.FUN.2026.10,
  author =	{Bramas, Quentin and Devismes, St\'{e}phane and Durand, Ana\"{i}s and Lafourcade, Pascal and Lamani, Anissa},
  title =	{{77 Shades of Grey}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.10},
  URN =		{urn:nbn:de:0030-drops-257294},
  doi =		{10.4230/LIPIcs.FUN.2026.10},
  annote =	{Keywords: Mobile robots, grid exploration, perpetual exploration}
}
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/DagMan.11.1.19
Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)

Authors: Christine Bauer, Li Chen, Nicola Ferro, Norbert Fuhr, Avishek Anand, Timo Breuer, Guglielmo Faggioli, Ophir Frieder, Hideo Joho, Jussi Karlgren, Johannes Kiesel, Bart P. Knijnenburg, Aldo Lipani, Lien Michiels, Andrea Papenmeier, Maria Soledad Pera, Mark Sanderson, Scott Sanner, Benno Stein, Johanne R. Trippas, Karin Verspoor, and Martijn C. Willemsen

Published in: Dagstuhl Manifestos, Volume 11, Issue 1 (2025)

Abstract
During the workshop, we deeply discussed what CONversational Information ACcess (CONIAC) is and its unique features, proposing a world model abstracting it, and defined the Conversational Agents Framework for Evaluation (CAFE) for the evaluation of CONIAC systems, consisting of six major components: 1) goals of the system’s stakeholders, 2) user tasks to be studied in the evaluation, 3) aspects of the users carrying out the tasks, 4) evaluation criteria to be considered, 5) evaluation methodology to be applied, and 6) measures for the quantitative criteria chosen.
Cite as

Christine Bauer, Li Chen, Nicola Ferro, Norbert Fuhr, Avishek Anand, Timo Breuer, Guglielmo Faggioli, Ophir Frieder, Hideo Joho, Jussi Karlgren, Johannes Kiesel, Bart P. Knijnenburg, Aldo Lipani, Lien Michiels, Andrea Papenmeier, Maria Soledad Pera, Mark Sanderson, Scott Sanner, Benno Stein, Johanne R. Trippas, Karin Verspoor, and Martijn C. Willemsen. Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352). In Dagstuhl Manifestos, Volume 11, Issue 1, pp. 19-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagMan.11.1.19,
  author =	{Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert and Anand, Avishek and Breuer, Timo and Faggioli, Guglielmo and Frieder, Ophir and Joho, Hideo and Karlgren, Jussi and Kiesel, Johannes and Knijnenburg, Bart P. and Lipani, Aldo and Michiels, Lien and Papenmeier, Andrea and Pera, Maria Soledad and Sanderson, Mark and Sanner, Scott and Stein, Benno and Trippas, Johanne R. and Verspoor, Karin and Willemsen, Martijn C.},
  title =	{{Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)}},
  pages =	{19--67},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2025},
  volume =	{11},
  number =	{1},
  editor =	{Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert and Anand, Avishek and Breuer, Timo and Faggioli, Guglielmo and Frieder, Ophir and Joho, Hideo and Karlgren, Jussi and Kiesel, Johannes and Knijnenburg, Bart P. and Lipani, Aldo and Michiels, Lien and Papenmeier, Andrea and Pera, Maria Soledad and Sanderson, Mark and Sanner, Scott and Stein, Benno and Trippas, Johanne R. and Verspoor, Karin and Willemsen, Martijn C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.11.1.19},
  URN =		{urn:nbn:de:0030-drops-252722},
  doi =		{10.4230/DagMan.11.1.19},
  annote =	{Keywords: Conversational Agents, Evaluation, Information Access}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2025.2
Unboundedness Problems for Formal Languages (Invited Talk)

Authors: Georg Zetzsche

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
Informally, unboundedness problems are decision problems that ask about the existence of infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came into focus in recent years because of their connections to downward closure computation and separability problems. Although unboundedness problems may seem difficult at first, it turns out that there are techniques that are at the same time conceptually very simple, but also apply to a surprisingly wide variety of language classes. The talk will survey recent results (and techniques) concerning unboundedness problems.
Cite as

Georg Zetzsche. Unboundedness Problems for Formal Languages (Invited Talk). In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zetzsche:LIPIcs.FSTTCS.2025.2,
  author =	{Zetzsche, Georg},
  title =	{{Unboundedness Problems for Formal Languages}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.2},
  URN =		{urn:nbn:de:0030-drops-250810},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.2},
  annote =	{Keywords: Decidability, formal languages, unifying frameworks, downward closure, separability}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.10
Amnesiac Flooding: Easy to Break, Hard to Escape

Authors: Henry Austin, Maximilien Gadouleau, George B. Mertzios, and Amitabh Trehan

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
Broadcast is a central problem in distributed computing. Recently, Hussak and Trehan [PODC'19/ STACS'20/DC'23] proposed a stateless broadcasting protocol (Amnesiac Flooding), which was surprisingly proven to terminate in asymptotically optimal time (linear in the diameter of the network). However, it remains unclear: (i) Are there other stateless terminating broadcast algorithms with the desirable properties of Amnesiac Flooding, (ii) How robust is Amnesiac Flooding with respect to faults? In this paper we make progress on both of these fronts. Under a reasonable restriction (obliviousness to message content) additional to the fault-free synchronous model, we prove that Amnesiac Flooding is the only strictly stateless deterministic protocol that can achieve terminating broadcast. We achieve this by identifying four natural properties of a terminating broadcast protocol that Amnesiac Flooding uniquely satisfies. In contrast, we prove that even minor relaxations of any of these four criteria allow the construction of other terminating broadcast protocols. On the other hand, we prove that Amnesiac Flooding can become non-terminating or non-broadcasting, even if we allow just one node to drop a single message on a single edge in a single round. As a tool for proving this, we focus on the set of all configurations of transmissions between nodes in the network, and obtain a dichotomy characterizing the configurations, starting from which, Amnesiac Flooding terminates. Additionally, we characterise the structure of sets of Byzantine agents capable of forcing non-termination or non-broadcast of the protocol on arbitrary networks.
Cite as

Henry Austin, Maximilien Gadouleau, George B. Mertzios, and Amitabh Trehan. Amnesiac Flooding: Easy to Break, Hard to Escape. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{austin_et_al:LIPIcs.DISC.2025.10,
  author =	{Austin, Henry and Gadouleau, Maximilien and Mertzios, George B. and Trehan, Amitabh},
  title =	{{Amnesiac Flooding: Easy to Break, Hard to Escape}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.10},
  URN =		{urn:nbn:de:0030-drops-248273},
  doi =		{10.4230/LIPIcs.DISC.2025.10},
  annote =	{Keywords: Amnesiac flooding, Terminating protocol, Algorithm state, Stateless protocol, Flooding algorithm, Network algorithms, Graph theory, Termination, Communication, Broadcast}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.36
Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.53
Wait-Only Broadcast Protocols Are Easier to Verify

Authors: Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder

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

Abstract
We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there is an execution which puts all processes on a given state; and the repeated coverability problem which asks if there is an infinite execution where a given transition is taken infinitely often. Since both problems are undecidable in the general case, we investigate those problems when the protocol is Wait-Only, i.e., it has no state from which a process can both broadcast and receive messages. We establish that the synchronization problem becomes Ackermann-complete, and the repeated coverability problem is in ExpSpace and PSpace-hard.
Cite as

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Wait-Only Broadcast Protocols Are Easier to Verify. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 53:1-53:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{guillou_et_al:LIPIcs.MFCS.2025.53,
  author =	{Guillou, Lucie and Sangnier, Arnaud and Sznajder, Nathalie},
  title =	{{Wait-Only Broadcast Protocols Are Easier to Verify}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{53:1--53: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.53},
  URN =		{urn:nbn:de:0030-drops-241609},
  doi =		{10.4230/LIPIcs.MFCS.2025.53},
  annote =	{Keywords: Parameterised verification, Reachability, Broadcast}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.38
The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors: Elias Rojas Collins, Chris Köcher, and Georg Zetzsche

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

Abstract
In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Cite as

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{collins_et_al:LIPIcs.MFCS.2025.38,
  author =	{Collins, Elias Rojas and K\"{o}cher, Chris and Zetzsche, Georg},
  title =	{{The Complexity of Separability for Semilinear Sets and Parikh Automata}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{38:1--38:21},
  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.38},
  URN =		{urn:nbn:de:0030-drops-241457},
  doi =		{10.4230/LIPIcs.MFCS.2025.38},
  annote =	{Keywords: Vector Addition System, Separability, Regular Language}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.13
Languages of Boundedly-Ambiguous Vector Addition Systems with States

Authors: Wojciech Czerwiński and Łukasz Orlikowski

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

Abstract
The aim of this paper is to deliver broad understanding of a class of languages of boundedly-ambiguous VASSs, that is k-ambiguous VASSs for some natural k. These are languages of Vector Addition Systems with States with the acceptance condition defined by the set of accepting states such that each accepted word has at most k accepting runs. We develop tools for proving that a given language is not accepted by any k-ambiguous VASS. Using them we show a few negative results: lack of some closure properties of languages of k-ambiguous VASSs and undecidability of the k-ambiguity problem, namely the question whether a given VASS language is a language of some k-ambiguous VASS. In fact we show an even more general undecidability result stating that for any class containing all regular languages and only k-ambiguous VASS languages for some k ∈ ℕ it is undecidable whether a language of a given 1-dimensional VASS belongs to this class. Finally, we show that the regularity problem is decidable for k-ambiguous VASSs.
Cite as

Wojciech Czerwiński and Łukasz Orlikowski. Languages of Boundedly-Ambiguous Vector Addition Systems with States. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2025.13,
  author =	{Czerwi\'{n}ski, Wojciech and Orlikowski, {\L}ukasz},
  title =	{{Languages of Boundedly-Ambiguous Vector Addition Systems with States}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{13:1--13:23},
  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.13},
  URN =		{urn:nbn:de:0030-drops-239635},
  doi =		{10.4230/LIPIcs.CONCUR.2025.13},
  annote =	{Keywords: vector addition systems, Petri nets, unambiguity, bounded-ambiguity, languages}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.30
Open Bisimilarity for the π-Calculus with Mismatch

Authors: Tiange Liu, Alwen Tiu, and Ross Horne

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

Abstract
Open bisimilarity is an equivalence relation for the π-calculus that is also congruence, making it suitable to use in compositional reasoning for mobile processes and communication protocols. The original definition of open bisimilarity, due to Sangiorgi, does not account for the mismatch operator, that is crucial in modelling real-world protocols. When mismatch is present, the congruence property no longer holds for open bisimilarity. In a LICS 2018 paper, Horne et al. proposed an extension of open bisimilarity, using a history-indexed class of relations, to address this problem. That definition, however, turns out to be non-compositional as we shall demonstrate in this paper. This paper presents a new definition of open bisimilarity in the π-calculus that incorporates mismatch. This is achieved by augmenting the transition semantics of the π-calculus with an explicit assumption about name distinctions, and by requiring that open bisimulation to be closed under an arbitary extension of the name distinctions assumption. We then prove that the resulting open bisimilarity is both an equivalence relation and a congruence.
Cite as

Tiange Liu, Alwen Tiu, and Ross Horne. Open Bisimilarity for the π-Calculus with Mismatch. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.CONCUR.2025.30,
  author =	{Liu, Tiange and Tiu, Alwen and Horne, Ross},
  title =	{{Open Bisimilarity for the \pi-Calculus with Mismatch}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-239805},
  doi =		{10.4230/LIPIcs.CONCUR.2025.30},
  annote =	{Keywords: mismatch, open bisimilarity, pi calculus}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2025.37
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)

Authors: Tomáš Dacík and Tomáš Vojnar

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

Abstract
We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.
Cite as

Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dacik_et_al:LIPIcs.ECOOP.2025.37,
  author =	{Dac{\'\i}k, Tom\'{a}\v{s} and Vojnar, Tom\'{a}\v{s}},
  title =	{{RacerF: Lightweight Static Data Race Detection for C Code}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{37:1--37: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.37},
  URN =		{urn:nbn:de:0030-drops-233298},
  doi =		{10.4230/LIPIcs.ECOOP.2025.37},
  annote =	{Keywords: concurrency, data race detection, static analysis}
}
Document
DOI: 10.4230/LIPIcs.SAND.2025.1
The Expressive Power of Uniform Population Protocols with Logarithmic Space

Authors: Philipp Czerner, Vincent Fischer, and Roland Guttenberg

Published in: LIPIcs, Volume 330, 4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025)

Abstract
Population protocols are a model of computation in which indistinguishable mobile agents interact in pairs to decide a property of their initial configuration. Originally introduced by Angluin et. al. in 2004 with a constant number of states, research nowadays focuses on protocols where the space usage depends on the number of agents. The expressive power of population protocols has so far however only been determined for protocols using o(log n) states, which compute only semilinear predicates, and for Ω(n) states. This leaves a significant gap, particularly concerning protocols with Θ(log n) or Θ(polylog n) states, which are the most common constructions in the literature. In this paper we close the gap and prove that for any ε > 0 and f ∈ Ω(log n)∩𝒪(n^{1-ε}), both uniform and non-uniform population protocols with Θ(f(n)) states can decide exactly those predicates, whose unary encoding lies in NSPACE(f(n) log n).
Cite as

Philipp Czerner, Vincent Fischer, and Roland Guttenberg. The Expressive Power of Uniform Population Protocols with Logarithmic Space. In 4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 330, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.SAND.2025.1,
  author =	{Czerner, Philipp and Fischer, Vincent and Guttenberg, Roland},
  title =	{{The Expressive Power of Uniform Population Protocols with Logarithmic Space}},
  booktitle =	{4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025)},
  pages =	{1:1--1:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-368-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{330},
  editor =	{Meeks, Kitty and Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2025.1},
  URN =		{urn:nbn:de:0030-drops-230540},
  doi =		{10.4230/LIPIcs.SAND.2025.1},
  annote =	{Keywords: Population Protocols, Uniform, Expressive Power}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2024.3
Verifying Concurrent Search Structures (Invited Talk)

Authors: Thomas Wies

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Search structures support the fundamental data storage primitives on key-value pairs: insert a pair, delete by key, search by key, and update the value associated with a key. Concurrent search structures are parallel algorithms to speed access to search structures on multicore and distributed servers. For these data structures to be efficient, the underlying parallel algorithms need to perform fine-grained synchronization between threads. This makes them notoriously difficult to design and implement correctly. Indeed, bugs are routinely found both in actual implementations and in the designs proposed by experts in peer-reviewed publications. Often, these bugs elude testing-based quality control due to complex thread interactions that only manifest after deployment, and under conditions that are difficult to replicate. Given the critical role that concurrent search structures play in today’s software infrastructure, it is therefore highly desirable to verify their correctness using formal methods, preferably in an automated fashion. In this talk, I will present a framework for obtaining linearizability proofs for concurrent search structures that are modular, reusable, and amenable to automation. The framework takes advantage of recent advances in local reasoning techniques based on concurrent separation logic. I will provide an overview of these techniques and discuss there use for verifying both lock-based and lock-free concurrent search structures such as concurrent (skip)lists, hash structures, binary search trees, B trees, and log-structured merge trees.
Cite as

Thomas Wies. Verifying Concurrent Search Structures (Invited Talk). In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wies:LIPIcs.CONCUR.2024.3,
  author =	{Wies, Thomas},
  title =	{{Verifying Concurrent Search Structures}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.3},
  URN =		{urn:nbn:de:0030-drops-207754},
  doi =		{10.4230/LIPIcs.CONCUR.2024.3},
  annote =	{Keywords: Concurrent search structures}
}
  • Refine by Type
  • 75 Document/PDF
  • 13 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 3 2026
  • 10 2025
  • 4 2024
  • 3 2023
  • 2 2020
  • Show More...

  • Refine by Author
  • 18 Meyer, Roland
  • 6 Muskalla, Sebastian
  • 6 Zetzsche, Georg
  • 4 Saivasan, Prakash
  • 3 Atig, Mohamed Faouzi
  • Show More...

  • Refine by Series/Journal
  • 72 LIPIcs
  • 2 TGDK
  • 1 DagMan

  • Refine by Classification
  • 6 Theory of computation → Formal languages and automata theory
  • 4 Theory of computation → Models of computation
  • 3 Theory of computation → Automata over infinite objects
  • 3 Theory of computation → Parallel computing models
  • 3 Theory of computation → Regular languages
  • Show More...

  • Refine by Keyword
  • 6 Petri nets
  • 4 Concurrency
  • 3 Decidability
  • 3 Parity Games
  • 3 Reachability
  • 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