25 Search Results for "Jain, Sanjay"

Document
DOI: 10.4230/LIPIcs.CSL.2026.23
A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

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

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

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

Copy BibTex To Clipboard

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

Authors: Sushmita Gupta, Pallavi Jain, Sanjay Seetharaman, and Meirav Zehavi

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
We present an algorithm for a class of n-fold ILPs whose existing algorithms in literature are often either (1) based on the augmentation framework where one starts with an arbitrary solution and then iteratively moves towards an optimal solution by solving appropriate programs; or (2) require solving a linear relaxation of the program; or (3) are based on decomposition/proximity based arguments. Combinatorial n-fold ILPs is a class of n-fold ILPs introduced and studied by Knop et al. [MP2020] that captures several other problems in a variety of domains. We present a simple and direct algorithm that solves combinatorial n-fold ILPs with unbounded non-negative variables via an application of the Steinitz lemma. Depending on the structure of the input ILP, we also improve upon the existing algorithms in the literature in terms of the running time, thereby showing an improvement that mirrors the one shown by Rohwedder [ICALP2025] contemporaneously and independently.
Cite as

Sushmita Gupta, Pallavi Jain, Sanjay Seetharaman, and Meirav Zehavi. A Simple Algorithm for Combinatorial n-Fold ILPs Using the Steinitz Lemma. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gupta_et_al:LIPIcs.IPEC.2025.14,
  author =	{Gupta, Sushmita and Jain, Pallavi and Seetharaman, Sanjay and Zehavi, Meirav},
  title =	{{A Simple Algorithm for Combinatorial n-Fold ILPs Using the Steinitz Lemma}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.14},
  URN =		{urn:nbn:de:0030-drops-251467},
  doi =		{10.4230/LIPIcs.IPEC.2025.14},
  annote =	{Keywords: n-fold integer linear program, parameterized algorithms}
}
Document
Research
DOI: 10.4230/TGDK.3.3.4
Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web

Authors: Florian Ruosch, Cristina Sarasua, and Abraham Bernstein

Published in: TGDK, Volume 3, Issue 3 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 3

Abstract
In Argument Mining, predicting argumentative relations between texts (or spans) remains one of the most challenging aspects, even more so in the cross-document setting. This paper makes three key contributions to advance research in this domain. We first extend an existing dataset, the Sci-Arg corpus, by annotating it with explicit inter-document argumentative relations, thereby allowing arguments to be distributed over several documents forming an Argument Web; these new annotations are published using Semantic Web technologies (RDF, OWL). Second, we explore and evaluate three automated approaches for predicting these inter-document argumentative relations, establishing critical baselines on the new dataset. We find that a simple classifier based on discourse indicators with access to context outperforms neural methods. Third, we conduct a comparative analysis of these approaches for both intra- and inter-document settings, identifying statistically significant differences in results that indicate the necessity of distinguishing between these two scenarios. Our findings highlight significant challenges in this complex domain and open crucial avenues for future research on the Argument Web of Science, particularly for those interested in leveraging Semantic Web technologies and knowledge graphs to understand scholarly discourse. With this, we provide the first stepping stones in the form of a benchmark dataset, three baseline methods, and an initial analysis for a systematic exploration of this field relevant to the Web of Data and Science.
Cite as

Florian Ruosch, Cristina Sarasua, and Abraham Bernstein. Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 3, pp. 4:1-4:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{ruosch_et_al:TGDK.3.3.4,
  author =	{Ruosch, Florian and Sarasua, Cristina and Bernstein, Abraham},
  title =	{{Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:33},
  ISSN =	{2942-7517},
  year =	{2025},
  volume =	{3},
  number =	{3},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.3.4},
  URN =		{urn:nbn:de:0030-drops-252159},
  doi =		{10.4230/TGDK.3.3.4},
  annote =	{Keywords: Argument Mining, Large Language Models, Knowledge Graphs, Link Prediction}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.5
Distributed Games with a Central Decision Maker

Authors: Bharat Adsul and Nehul Jain

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

Abstract
We study distributed games played on non-deterministic asynchronous automata which feature a central decision maker process that participates in all key decision making tasks. In these partial-information games, processes use their causal past to respond to scheduling choices made by the scheduler and cooperatively strategize as a team to achieve the winning objective. We show that the problem of deciding the existence of a distributed winning strategy is efficiently solvable for global safety and local parity objectives. We provide algorithmic solutions that match their computational hardness. We formulate the notion of a finite-state distributed strategy which allows to quantify its distributed memory requirements. For the aforementioned objectives, we establish that finite-state distributed winning strategies always exist. In fact, we provide novel constructions of such winning strategies which are shown to have almost optimal amount of distributed memory. We also show that a natural extension of the model with two decision making processes is undecidable.
Cite as

Bharat Adsul and Nehul Jain. Distributed Games with a Central Decision Maker. 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. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.FSTTCS.2025.5,
  author =	{Adsul, Bharat and Jain, Nehul},
  title =	{{Distributed Games with a Central Decision Maker}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{5:1--5:18},
  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.5},
  URN =		{urn:nbn:de:0030-drops-250843},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.5},
  annote =	{Keywords: Mazurkiewicz traces, models of concurrency, distributed synthesis, game-theoretic models, asynchronous automata, distributed decision-making}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.23
Parallel Complexity of Depth-First-Search and Maximal Path in Restricted Graph Classes

Authors: Archit Chauhan, Samir Datta, and M. Praveen

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

Abstract
Constructing a Depth First Search (DFS) tree is a fundamental graph problem, whose parallel complexity is still not settled. Reif showed parallel intractability of lex-first DFS. In contrast, randomized parallel algorithms (and more recently, deterministic quasipolynomial parallel algorithms) are known for constructing a DFS tree in general (di)graphs. However a deterministic parallel algorithm for DFS in general graphs remains an elusive goal. Working towards this, a series of works gave deterministic NC algorithms for DFS in planar graphs and digraphs. We further extend these results to more general graph classes, by providing NC algorithms for (di)graphs of bounded genus, and for undirected H-minor-free graphs where H is a fixed graph with at most one crossing. For the case of (di)graphs of bounded treewidth, we further improve the complexity to a Logspace bound. Constructing a maximal path is a simpler problem (that reduces to DFS) for which no deterministic parallel bounds are known for general graphs. For planar graphs a bound of O(log n) parallel time on a CRCW PRAM (thus in NC²) is known. We improve this bound to Logspace.
Cite as

Archit Chauhan, Samir Datta, and M. Praveen. Parallel Complexity of Depth-First-Search and Maximal Path in Restricted Graph Classes. 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. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chauhan_et_al:LIPIcs.FSTTCS.2025.23,
  author =	{Chauhan, Archit and Datta, Samir and Praveen, M.},
  title =	{{Parallel Complexity of Depth-First-Search and Maximal Path in Restricted Graph Classes}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{23:1--23:21},
  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.23},
  URN =		{urn:nbn:de:0030-drops-251041},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.23},
  annote =	{Keywords: Parallel Complexity, Graph Algorithms, Depth First Search, Maximal Path, Planar Graphs, Minor-Free, Treewidth, Logspace}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2025.44
Brief Announcement: Incrementally Verifiable Distributed Computation

Authors: Eden Aldema Tshuva and Rotem Oshman

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

Abstract
Incrementally verifiable computation (IVC) is a cryptographic scheme that allows a prover to certify the correctness of a long or ongoing computation in an incremental manner, by repeatedly updating a proof certifying the computation so far. Updating the proof does not require access to the entire trace of the computation, which makes the IVC prover memory efficient. In this work we construct incrementally verifiable distributed computation, which allows a distributed algorithm to efficiently certify its own execution using low memory and communication overhead. Our primary motivation is massively-parallel computation (MPC), where memory efficiency is make-or-break: the machines participating in an MPC algorithm usually cannot store the entire trace of their computation. Thus, certifying MPC algorithms essentially requires distributed IVC. At the heart of this work is a new abstraction, updatable batch arguments for {NP} (UpBARGs), which we define and construct. Standard BARGs allow one to prove a batch of k {NP}-statements using a proof whose length barely grows with k; however, the statements and their witnesses must all be known in advance. In contrast, UpBARGs support adding statements and witnesses on the fly, making them a flexible tool for constructing IVC across different computational models. We use UpBARGs to construct IVC for streaming algorithms, for MPC algorithms, and for PRAM algorithms in the exclusive-read exclusive-write (EREW) model.
Cite as

Eden Aldema Tshuva and Rotem Oshman. Brief Announcement: Incrementally Verifiable Distributed Computation. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 44:1-44:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aldematshuva_et_al:LIPIcs.DISC.2025.44,
  author =	{Aldema Tshuva, Eden and Oshman, Rotem},
  title =	{{Brief Announcement: Incrementally Verifiable Distributed Computation}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{44:1--44:7},
  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.44},
  URN =		{urn:nbn:de:0030-drops-248829},
  doi =		{10.4230/LIPIcs.DISC.2025.44},
  annote =	{Keywords: Incrementally verifiable computation, massively parallel computation, streaming, parallel RAM, batch arguments, SNARG}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ESA.2025.2
Securing Dynamic Data: A Primer on Differentially Private Data Structures (Invited Talk)

Authors: Monika Henzinger and Roodabeh Safavi

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
We give an introduction into differential privacy in the dynamic setting, called the continual observation setting.
Cite as

Monika Henzinger and Roodabeh Safavi. Securing Dynamic Data: A Primer on Differentially Private Data Structures (Invited Talk). In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.ESA.2025.2,
  author =	{Henzinger, Monika and Safavi, Roodabeh},
  title =	{{Securing Dynamic Data: A Primer on Differentially Private Data Structures}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.2},
  URN =		{urn:nbn:de:0030-drops-244702},
  doi =		{10.4230/LIPIcs.ESA.2025.2},
  annote =	{Keywords: Differential privacy, continual observation}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.40
Sublinear Space Graph Algorithms in the Continual Release Model

Authors: Alessandro Epasto, Quanquan C. Liu, Tamalika Mukherjee, and Felix Zhou

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)

Abstract
The graph continual release model of differential privacy seeks to produce differentially private solutions to graph problems under a stream of edge updates where new private solutions are released after each update. Thus far, previously known edge-differentially private algorithms for most graph problems including densest subgraph and matchings in the continual release setting only output real-value estimates (not vertex subset solutions) and do not use sublinear space. Instead, they rely on computing exact graph statistics on the input [Hendrik Fichtenberger et al., 2021; Shuang Song et al., 2018]. In this paper, we leverage sparsification to address the above shortcomings for edge-insertion streams. Our edge-differentially private algorithms use sublinear space with respect to the number of edges in the graph while some also achieve sublinear space in the number of vertices in the graph. In addition, for the densest subgraph problem, we also output edge-differentially private vertex subset solutions; no previous graph algorithms in the continual release model output such subsets. We make novel use of assorted sparsification techniques from the non-private streaming and static graph algorithms literature to achieve new results in the sublinear space, continual release setting. This includes algorithms for densest subgraph, maximum matching, as well as the first continual release k-core decomposition algorithm. We also develop a novel sparse level data structure for k-core decomposition that may be of independent interest. To complement our insertion-only algorithms, we conclude with polynomial additive error lower bounds for edge-privacy in the fully dynamic setting, where only logarithmic lower bounds were previously known.
Cite as

Alessandro Epasto, Quanquan C. Liu, Tamalika Mukherjee, and Felix Zhou. Sublinear Space Graph Algorithms in the Continual Release Model. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 40:1-40:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{epasto_et_al:LIPIcs.APPROX/RANDOM.2025.40,
  author =	{Epasto, Alessandro and Liu, Quanquan C. and Mukherjee, Tamalika and Zhou, Felix},
  title =	{{Sublinear Space Graph Algorithms in the Continual Release Model}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{40:1--40:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.40},
  URN =		{urn:nbn:de:0030-drops-244064},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.40},
  annote =	{Keywords: Differential Privacy, Continual Release, Densest Subgraph, k-Core Decomposition, Maximum Matching}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.51
Word Structures and Their Automatic Presentations

Authors: Xiaoyang Gong, Bakh Khoussainov, and Yuyang Zhuge

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

Abstract
We study automatic presentations of the structures (ℕ; S), (ℕ; E_S), (ℕ; ≤), and their expansions by a unary predicate U. Here S is the successor function, E_S is the undirected version of S, and ≤ is the natural order. We call these structures word structures. Our goal is three-fold. First, we study the isomorphism problem for automatic word structures by focusing on the following three problems. The first problem asks to design an algorithm that, given an automatic structure A, decides if A is isomorphic to (ℕ; S). The second asks to design an algorithm that, given two automatic presentations of (ℕ; S, U₁) and (ℕ; S, U₂), where U₁ and U₂ are unary predicates, decides if these structures are isomorphic. The third problem investigates if there is an algorithm that, given two automatic presentations of (ℕ; ≤, U₁) and (ℕ; ≤, U₂), decides whether U₁ ∩ U₂ ≠ ∅. We show that these problems are undecidable. Next, we study intrinsic regularity of the function S in the structure Path_ω = (ℕ; E_S). We build an automatic presentation of Path_ω in which S is not regular. This implies that S is not intrinsically regular in Path_ω. For U ⊆ ℕ, let d_U be the function that computes the distances between the consecutive elements of U. We build automatic presentations of (ℕ; ≤, U) where d_U can realise logarithmic, radical, intermediate, and exponential functions.
Cite as

Xiaoyang Gong, Bakh Khoussainov, and Yuyang Zhuge. Word Structures and Their Automatic Presentations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 51:1-51:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gong_et_al:LIPIcs.MFCS.2025.51,
  author =	{Gong, Xiaoyang and Khoussainov, Bakh and Zhuge, Yuyang},
  title =	{{Word Structures and Their Automatic Presentations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{51:1--51: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.51},
  URN =		{urn:nbn:de:0030-drops-241581},
  doi =		{10.4230/LIPIcs.MFCS.2025.51},
  annote =	{Keywords: Automatic structures, the isomorphism problem, decidability, undecidability, regular relations}
}
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.12
The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives

Authors: Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard

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

Abstract
This paper studies the rational synthesis problem for multi-player games played on graphs when rational players are following subgame perfect equilibria. In these games, one player, the system, declares his strategy upfront, and the other players, composing the environment, then rationally respond by playing strategies forming a subgame perfect equilibrium. We study the complexity of the rational synthesis problem when the players have ω-regular objectives encoded as parity objectives. Our algorithm is based on an encoding into a three-player game with imperfect information, showing that the problem is in 2ExpTime. When the number of environment players is fixed, the problem is in ExpTime and is NP- and coNP-hard. Moreover, for a fixed number of players and reachability objectives, we get a polynomial algorithm.
Cite as

Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard. The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2025.12,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Reynouard, Alexis and Van Den Bogaard, Marie},
  title =	{{The Non-Cooperative Rational Synthesis Problem for SPEs and \omega-Regular Objectives}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{12:1--12: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.12},
  URN =		{urn:nbn:de:0030-drops-239622},
  doi =		{10.4230/LIPIcs.CONCUR.2025.12},
  annote =	{Keywords: non-zero-sum games, subgame perfect equilibria, rational synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.9
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games

Authors: Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou

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

Abstract
Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. This paper introduces a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction. Furthermore, we demonstrate that under binary encoding this reduction is polynomial, thereby directly corroborating the known NP ∩ coNP complexity of SPGs and providing new understanding in the relationship between parity and reachability objectives in turn-based stochastic games.
Cite as

Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou. A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berthon_et_al:LIPIcs.CONCUR.2025.9,
  author =	{Berthon, Rapha\"{e}l and Katoen, Joost-Pieter and Zhou, Zihan},
  title =	{{A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{9:1--9: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.9},
  URN =		{urn:nbn:de:0030-drops-239595},
  doi =		{10.4230/LIPIcs.CONCUR.2025.9},
  annote =	{Keywords: stochastic games, parity, reduction}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.14
Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Authors: Kazuki Watanabe

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure. Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.
Cite as

Kazuki Watanabe. Pareto Fronts for Compositionally Solving String Diagrams of Parity Games. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{watanabe:LIPIcs.CALCO.2025.14,
  author =	{Watanabe, Kazuki},
  title =	{{Pareto Fronts for Compositionally Solving String Diagrams of Parity Games}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.14},
  URN =		{urn:nbn:de:0030-drops-235734},
  doi =		{10.4230/LIPIcs.CALCO.2025.14},
  annote =	{Keywords: parity game, compositionality, string diagram}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2025.10
LoRaHART: Hardware-Aware Real-Time Scheduling for LoRa

Authors: Soumya Ranjan Sahoo, Amalinda Gamage, Niraj Kumar, and Arvind Easwaran

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
Time-sensitive data acquisition is critical for many Low-Power Wide-Area Network (LPWAN) applications, such as healthcare monitoring and industrial Internet of Things. Among the available LPWAN technologies, LoRa (Long Range) has emerged as a leading choice, offering kilometer-scale communication with minimal power consumption and enabling high-density deployments across large areas. However, the conventional ALOHA-based Medium Access Control (MAC) in LoRa is not designed to support real-time communication over large-scale networks. This paper introduces LoRaHART, a novel approach that overcomes two critical, under-explored limitations in Commercial Off The Shelf (COTS) LoRa gateways that impact real-time performance. LoRa gateways have limited capacity for demodulation of parallel transmissions and their antenna can either transmit or receive at any time instant. LoRaHART incorporates a hardware-aware super-frame structure, comprising both Time Division Multiple Access (TDMA) slots as well as opportunistic retransmissions using Carrier Sense Multiple Access (CSMA), designed to mitigate the above constraints. We use a partial packing and makespan minimization algorithm to schedule periodic real-time transmissions efficiently within the TDMA slots, and also develop a probabilistic node contention model for CSMA retransmissions, providing analytical guarantees for deadline satisfaction under ideal channel conditions. Our evaluation of LoRaHART on a 40-node LoRa testbed demonstrates significant improvements over existing solutions in practice, achieving an average Packet Reception Ratio of 98% and a 45% higher airtime utilization than the best performing baseline.
Cite as

Soumya Ranjan Sahoo, Amalinda Gamage, Niraj Kumar, and Arvind Easwaran. LoRaHART: Hardware-Aware Real-Time Scheduling for LoRa. In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 10:1-10:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sahoo_et_al:LIPIcs.ECRTS.2025.10,
  author =	{Sahoo, Soumya Ranjan and Gamage, Amalinda and Kumar, Niraj and Easwaran, Arvind},
  title =	{{LoRaHART: Hardware-Aware Real-Time Scheduling for LoRa}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{10:1--10:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.10},
  URN =		{urn:nbn:de:0030-drops-235880},
  doi =		{10.4230/LIPIcs.ECRTS.2025.10},
  annote =	{Keywords: LoRa, LPWAN, Real-time Scheduling, Hardware Constraints}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.160
Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages

Authors: Olivier Idir and Karoliina Lehtinen

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

Abstract
The parity index problem of tree automata asks, given a regular tree language L and a set of priorities J, is L J-feasible, that is, recognised by a nondeterministic parity automaton with priorities J? This is a long-standing open problem, of which only a few sub-cases and variations are known to be decidable. In a significant but technically difficult step, Colcombet and Löding reduced the problem to the uniform universality of distance-parity automata. In this article, we revisit the index problem using tools from the parity game literature. We add some counters to Lehtinen’s register game, originally used to solve parity games in quasipolynomial time, and use this novel game to characterise J-feasibility. This provides a alternative proof to Colcombet and Löding’s reduction. We then provide a second characterisation, based on the notion of attractor decompositions and the complexity of their structure, as measured by a parameterised version of their Strahler number, which we call n-Strahler number. Finally, we rephrase this result using the notion of universal tree extended to automata: a guidable automaton recognises a [1,2j]-feasible language if and only if it admits a universal tree with n-Strahler number j, for some n. In particular, a language recognised by a guidable automaton {A} is Büchi-feasible if and only if there is a uniform bound n ∈ ℕ such that all trees in the language admit an accepting run with an attractor decomposition of width bounded by n. Equivalently, the language is Büchi-feasible if and only if {A} admits a finite universal tree. While we do not solve the decidability of the index problem, our work makes the state-of-the-art more accessible and brings to light the deep relationships between the J-feasibility of a language and attractor decompositions, universal trees and Lehtinen’s register game.
Cite as

Olivier Idir and Karoliina Lehtinen. Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 160:1-160:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{idir_et_al:LIPIcs.ICALP.2025.160,
  author =	{Idir, Olivier and Lehtinen, Karoliina},
  title =	{{Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{160:1--160: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.160},
  URN =		{urn:nbn:de:0030-drops-235377},
  doi =		{10.4230/LIPIcs.ICALP.2025.160},
  annote =	{Keywords: Tree automata, parity automata, Mostowski index, Strahler number, attractor decomposition, universal trees}
}
  • Refine by Type
  • 25 Document/PDF
  • 18 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 16 2025
  • 2 2024
  • 2 2023
  • 2 2019
  • Show More...

  • Refine by Author
  • 6 Jain, Sanjay
  • 5 Stephan, Frank
  • 2 Gao, Ziyuan
  • 2 Hoi, Gordon
  • 2 Khoussainov, Bakh
  • Show More...

  • Refine by Series/Journal
  • 21 LIPIcs
  • 4 TGDK

  • Refine by Classification
  • 3 Theory of computation
  • 3 Theory of computation → Automata over infinite objects
  • 2 Information systems → Graph-based database models
  • 2 Theory of computation → Algorithmic game theory
  • 2 Theory of computation → Design and analysis of algorithms
  • Show More...

  • Refine by Keyword
  • 2 Knowledge Graphs
  • 2 Large Language Models
  • 2 recursion theory
  • 2 stochastic games
  • 1 Algorithmic and automatic learning
  • 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