91 Search Results for "S., Akshay"

Volume

LIPIcs, Volume 65

36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

FSTTCS 2016, December 13-15, 2016, Chennai, India

Editors: Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen

Document
DOI: 10.4230/LIPIcs.ESA.2025.106
On Estimating the Quantum 𝓁_α Distance

Authors: Yupan Liu and Qisheng Wang

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

Abstract
We study the computational complexity of estimating the quantum 𝓁_α distance T_α(ρ₀,ρ₁), defined via the Schatten α-norm ‖A‖_α := tr(|A|^α)^{1/α}, given poly(n)-size state-preparation circuits of n-qubit quantum states ρ₀ and ρ₁. This quantity serves as a lower bound on the trace distance for α > 1. For any constant α > 1, we develop an efficient rank-independent quantum estimator for T_α(ρ₀,ρ₁) with time complexity poly(n), achieving an exponential speedup over the prior best results of exp(n) due to Wang, Guan, Liu, Zhang, and Ying (IEEE Trans. Inf. Theory 2024). Our improvement leverages efficiently computable uniform polynomial approximations of signed positive power functions within quantum singular value transformation, thereby eliminating the dependence on the rank of the states. Our quantum algorithm reveals a dichotomy in the computational complexity of the Quantum State Distinguishability Problem with Schatten α-norm (QSD_α), which involves deciding whether T_α(ρ₀,ρ₁) is at least 2/5 or at most 1/5. This dichotomy arises between the cases of constant α > 1 and α = 1: - For any 1+Ω(1) ≤ α ≤ O(1), QSD_α is BQP-complete. - For any 1 ≤ α ≤ 1+1/n, QSD_α is QSZK-complete, implying that no efficient quantum estimator for T_α(ρ₀,ρ₁) exists unless BQP = QSZK. The hardness results follow from reductions based on new rank-dependent inequalities for the quantum 𝓁_α distance with 1 ≤ α ≤ ∞, which are of independent interest.
Cite as

Yupan Liu and Qisheng Wang. On Estimating the Quantum 𝓁_α Distance. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 106:1-106:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ESA.2025.106,
  author =	{Liu, Yupan and Wang, Qisheng},
  title =	{{On Estimating the Quantum 𝓁\underline\alpha Distance}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{106:1--106:19},
  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.106},
  URN =		{urn:nbn:de:0030-drops-245758},
  doi =		{10.4230/LIPIcs.ESA.2025.106},
  annote =	{Keywords: quantum algorithms, quantum state testing, trace distance, Schatten norm}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.42
On the Spectral Expansion of Monotone Subsets of the Hypercube

Authors: Yumou Fei and Renato Ferreira Pinto Jr.

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

Abstract
We study the spectral gap of subgraphs of the hypercube induced by monotone subsets of vertices. For a monotone subset A ⊆ {0,1}ⁿ of density μ(A), the previous best lower bound on the spectral gap, due to Cohen [Cohen, 2016], was γ ≳ μ(A)/n², improving upon the earlier bound γ ≳ μ(A)²/n² established by Ding and Mossel [Ding and Mossel, 2014]. In this paper, we prove the optimal lower bound γ ≳ μ(A)/n. As a corollary, we improve the mixing time upper bound of the random walk on constant-density monotone sets from O(n³), as shown by Ding and Mossel, to O(n²). Along the way, we develop two new inequalities that may be of independent interest: (1) a directed L²-Poincaré inequality on the hypercube, and (2) an "approximate" FKG inequality for monotone sets.
Cite as

Yumou Fei and Renato Ferreira Pinto Jr.. On the Spectral Expansion of Monotone Subsets of the Hypercube. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fei_et_al:LIPIcs.APPROX/RANDOM.2025.42,
  author =	{Fei, Yumou and Ferreira Pinto Jr., Renato},
  title =	{{On the Spectral Expansion of Monotone Subsets of the Hypercube}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{42:1--42:24},
  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.42},
  URN =		{urn:nbn:de:0030-drops-244081},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.42},
  annote =	{Keywords: Random walks, mixing time, FKG inequality, Poincar\'{e} inequality, directed isoperimetry}
}
Document
DOI: 10.4230/LIPIcs.ITC.2025.3
Leakage-Resilience of Shamir’s Secret Sharing: Identifying Secure Evaluation Places

Authors: Jihun Hwang, Hemanta K. Maji, Hai H. Nguyen, and Xiuyu Ye

Published in: LIPIcs, Volume 343, 6th Conference on Information-Theoretic Cryptography (ITC 2025)

Abstract
Can Shamir’s secret-sharing protect its secret even when all shares are partially compromised? For instance, repairing Reed-Solomon codewords, when possible, recovers the entire secret in the corresponding Shamir’s secret sharing. Yet, Shamir’s secret sharing mitigates various side-channel threats, depending on where its "secret-sharing polynomial" is evaluated. Although most evaluation places yield secure schemes, none are known explicitly; even techniques to identify them are unknown. Our work initiates research into such classifier constructions and derandomization objectives. In this work, we focus on Shamir’s scheme over prime fields, where every share is required to reconstruct the secret. We investigate the security of these schemes against single-bit probes into shares stored in their native binary representation. Technical analysis is particularly challenging when dealing with Reed-Solomon codewords over prime fields, as observed recently in the code repair literature. Furthermore, ensuring the statistical independence of the leakage from the secret necessitates the elimination of any subtle correlations between them. In this context, we present: 1) An efficient algorithm to classify evaluation places as secure or vulnerable against the least-significant-bit leakage. 2) Modulus choices where the classifier above extends to any single-bit probe per share. 3) Explicit modulus choices and secure evaluation places for them. On the way, we discover new bit-probing attacks on Shamir’s scheme, revealing surprising correlations between the leakage and the secret, leading to vulnerabilities when choosing evaluation places naïvely. Our results rely on new techniques to analyze the security of secret-sharing schemes against side-channel threats. We connect their leakage resilience to the orthogonality of square wave functions, which, in turn, depends on the 2-adic valuation of rational approximations. These techniques, novel to the security analysis of secret sharings, can potentially be of broader interest.
Cite as

Jihun Hwang, Hemanta K. Maji, Hai H. Nguyen, and Xiuyu Ye. Leakage-Resilience of Shamir’s Secret Sharing: Identifying Secure Evaluation Places. In 6th Conference on Information-Theoretic Cryptography (ITC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 343, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hwang_et_al:LIPIcs.ITC.2025.3,
  author =	{Hwang, Jihun and Maji, Hemanta K. and Nguyen, Hai H. and Ye, Xiuyu},
  title =	{{Leakage-Resilience of Shamir’s Secret Sharing: Identifying Secure Evaluation Places}},
  booktitle =	{6th Conference on Information-Theoretic Cryptography (ITC 2025)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-385-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{343},
  editor =	{Gilboa, Niv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITC.2025.3},
  URN =		{urn:nbn:de:0030-drops-243531},
  doi =		{10.4230/LIPIcs.ITC.2025.3},
  annote =	{Keywords: Shamir’s secret sharing, leakage resilience, physical bit probing, secure evaluation places, secure modulus choice, square wave families, LLL algorithm, Fourier analysis}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.79
Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space

Authors: Eike Neumann

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

Abstract
We study the problem of deciding whether a point escapes a closed subset of ℝ^d under the iteration of a continuous map f : ℝ^d → ℝ^d in the bit-model of real computation. We give a sound partial decision method for this problem which is complete in the sense that its halting set contains the halting set of all sound partial decision methods for the problem. Equivalently, our decision method terminates on all problem instances whose answer is robust under all sufficiently small perturbations of the function. We further show that the halting set of our algorithm is dense in the set of all problem instances. While our algorithm applies to general continuous functions, we demonstrate that it also yields complete decision methods for much more rigid function families: affine linear systems and quadratic complex polynomials. In the latter case, completeness is subject to the density of hyperbolicity conjecture in complex dynamics. This in particular yields an alternative proof of Hertling’s (2004) conditional answer to a question raised by Penrose (1989) regarding the computability of the Mandelbrot set.
Cite as

Eike Neumann. Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 79:1-79:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{neumann:LIPIcs.MFCS.2025.79,
  author =	{Neumann, Eike},
  title =	{{Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{79:1--79: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.79},
  URN =		{urn:nbn:de:0030-drops-241866},
  doi =		{10.4230/LIPIcs.MFCS.2025.79},
  annote =	{Keywords: Dynamical Systems, Computability in Analysis, Non-Linear Functions}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.71
On Large Zeros of Linear Recurrence Sequences

Authors: Florian Luca, Joël Ouaknine, and James Worrell

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

Abstract
The Skolem Problem asks to determine whether a given integer linear recurrence sequence (LRS) has a zero term. This problem, whose decidability has been open for many decades, arises across a wide range of topics in computer science, including loop termination, formal languages, automata theory, and probabilistic model checking, amongst many others. In the present paper, we introduce a notion of "large" zeros of (non-degenerate) linear recurrence sequences, i.e., zeros occurring at an index larger than a sixth-fold exponential of the size of the data defining the given LRS . We establish two main results. First, we show that large zeros are very sparse: the set of positive integers that can possibly arise as large zeros of some LRS has null density. This in turn immediately yields a Universal Skolem Set of density one, answering a question left open in the literature. Second, we define an infinite set of prime numbers, termed "good", having density one amongst all prime numbers, with the following property: for any large zero of a given LRS, there is an interval around the large zero together with an upper bound on the number of good primes possibly present in that interval. The bound in question is much lower than one would expect if good primes were distributed similarly as ordinary prime numbers, as per the Cramér model in number theory. We therefore conjecture that large zeros do not exist, which would entail decidability of the Skolem Problem.
Cite as

Florian Luca, Joël Ouaknine, and James Worrell. On Large Zeros of Linear Recurrence Sequences. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 71:1-71:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{luca_et_al:LIPIcs.MFCS.2025.71,
  author =	{Luca, Florian and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{On Large Zeros of Linear Recurrence Sequences}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{71:1--71:11},
  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.71},
  URN =		{urn:nbn:de:0030-drops-241781},
  doi =		{10.4230/LIPIcs.MFCS.2025.71},
  annote =	{Keywords: Skolem Problem, linear recurrence sequences, decidability, Cram\'{e}r conjecture}
}
Document
DOI: 10.4230/LIPIcs.DNA.31.4
Differentiable Programming of Indexed Chemical Reaction Networks and Reaction-Diffusion Systems

Authors: Inhoo Lee, Salvador Buse, and Erik Winfree

Published in: LIPIcs, Volume 347, 31st International Conference on DNA Computing and Molecular Programming (DNA 31) (2025)

Abstract
Many molecular systems are best understood in terms of prototypical species and reactions. The central dogma and related biochemistry are rife with examples: gene i is transcribed into RNA i, which is translated into protein i; kinase n phosphorylates substrate m; protein p dimerizes with protein q. Engineered nucleic acid systems also often have this form: oligonucleotide i hybridizes to complementary oligonucleotide j; signal strand n displaces the output of seesaw gate m; hairpin p triggers the opening of target q. When there are many variants of a small number of prototypes, it can be conceptually cleaner and computationally more efficient to represent the full system in terms of indexed species (e.g. for dimerization, M_p, D_pq) and indexed reactions (M_p + M_q → D_pq). Here, we formalize the Indexed Chemical Reaction Network (ICRN) model and describe a Python software package designed to simulate such systems in the well-mixed and reaction-diffusion settings, using a differentiable programming framework originally developed for large-scale neural network models, taking advantage of GPU acceleration when available. Notably, this framework makes it straightforward to train the models’ initial conditions and rate constants to optimize a target behavior, such as matching experimental data, performing a computation, or exhibiting spatial pattern formation. The natural map of indexed chemical reaction networks onto neural network formalisms provides a tangible yet general perspective for translating concepts and techniques from the theory and practice of neural computation into the design of biomolecular systems.
Cite as

Inhoo Lee, Salvador Buse, and Erik Winfree. Differentiable Programming of Indexed Chemical Reaction Networks and Reaction-Diffusion Systems. In 31st International Conference on DNA Computing and Molecular Programming (DNA 31). Leibniz International Proceedings in Informatics (LIPIcs), Volume 347, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.DNA.31.4,
  author =	{Lee, Inhoo and Buse, Salvador and Winfree, Erik},
  title =	{{Differentiable Programming of Indexed Chemical Reaction Networks and Reaction-Diffusion Systems}},
  booktitle =	{31st International Conference on DNA Computing and Molecular Programming (DNA 31)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-399-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{347},
  editor =	{Schaeffer, Josie and Zhang, Fei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.31.4},
  URN =		{urn:nbn:de:0030-drops-238534},
  doi =		{10.4230/LIPIcs.DNA.31.4},
  annote =	{Keywords: Differentiable Programming, Chemical Reaction Networks, Reaction-Diffusion Systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.6
Omega-Regular Verification and Control for Distributional Specifications in MDPs

Authors: S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić

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

Abstract
A classical approach to studying Markov decision processes (MDPs) is to view them as state transformers. However, MDPs can also be viewed as distribution transformers, where an MDP under a strategy generates a sequence of probability distributions over MDP states. This view arises in several applications, even as the probabilistic model checking problem becomes much harder compared to the classical state transformer counterpart. It is known that even distributional reachability and safety problems become computationally intractable (Skolem- and positivity-hard). To address this challenge, recent works focused on sound but possibly incomplete methods for verification and control of MDPs under the distributional view. However, existing automated methods are applicable only to distributional reachability, safety and reach-avoidance specifications. In this work, we present the first automated method for verification and control of MDPs with respect to distributional omega-regular specifications. To achieve this, we propose a novel notion of distributional certificates, which are sound and complete proof rules for proving that an MDP under a distributionally memoryless strategy satisfies some distributional omega-regular specification. We then use our distributional certificates to design the first fully automated algorithms for verification and control of MDPs with respect to distributional omega-regular specifications. Our algorithms follow a template-based synthesis approach and provide soundness and relative completeness guarantees, while running in PSPACE. Our prototype implementation demonstrates practical applicability of our algorithms to challenging examples collected from the literature.
Cite as

S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić. Omega-Regular Verification and Control for Distributional Specifications in MDPs. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2025.6,
  author =	{Akshay, S. and Neysari, Ouldouz and \v{Z}ikeli\'{c}, Ðor{\d}e},
  title =	{{Omega-Regular Verification and Control for Distributional Specifications in MDPs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{6:1--6:19},
  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.6},
  URN =		{urn:nbn:de:0030-drops-239562},
  doi =		{10.4230/LIPIcs.CONCUR.2025.6},
  annote =	{Keywords: MDPs, Distributional objectives, \omega-regularity, Certificates}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.33
Chance and Mass Interpretations of Probabilities in Markov Decision Processes

Authors: Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay, and Ichiro Hasuo

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

Abstract
Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.
Cite as

Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay, and Ichiro Hasuo. Chance and Mass Interpretations of Probabilities in Markov Decision Processes. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tsai_et_al:LIPIcs.CONCUR.2025.33,
  author =	{Tsai, Yun Chen and Phalakarn, Kittiphon and Akshay, S. and Hasuo, Ichiro},
  title =	{{Chance and Mass Interpretations of Probabilities in Markov Decision Processes}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{33:1--33:19},
  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.33},
  URN =		{urn:nbn:de:0030-drops-239838},
  doi =		{10.4230/LIPIcs.CONCUR.2025.33},
  annote =	{Keywords: MDP, distribution transformer, antichain, template-based synthesis}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.163
Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers

Authors: Toghrul Karimov

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

Abstract
A discrete-time linear dynamical system (LDS) is given by an update matrix M ∈ ℝ^{d× d}, and has the trajectories ⟨s, Ms, M²s, …⟩ for s ∈ ℝ^d. Reachability-type decision problems of linear dynamical systems, most notably the Skolem Problem, lie at the forefront of decidability: typically, sound and complete algorithms are known only in low dimensions, and these rely on sophisticated tools from number theory and Diophantine approximation. Recently, however, o-minimality has emerged as a counterpoint to these number-theoretic tools that allows us to decide certain modifications of the classical problems of LDS without any dimension restrictions. In this paper, we first introduce the Decomposition Method, a framework that captures all applications of o-minimality to decision problems of LDS that are currently known to us. We then use the Decomposition Method to show decidability of the Robust Safety Problem (restricted to bounded initial sets) in arbitrary dimension: given a matrix M, a bounded semialgebraic set S of initial points, and a semialgebraic set T of unsafe points, it is decidable whether there exists ε > 0 such that all orbits that begin in the ε-ball around S avoid T.
Cite as

Toghrul Karimov. Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 163:1-163:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{karimov:LIPIcs.ICALP.2025.163,
  author =	{Karimov, Toghrul},
  title =	{{Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{163:1--163:17},
  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.163},
  URN =		{urn:nbn:de:0030-drops-235401},
  doi =		{10.4230/LIPIcs.ICALP.2025.163},
  annote =	{Keywords: Linear dynamical systems, reachability problems, o-minimality}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.13
Quantum Speedup for Sampling Random Spanning Trees

Authors: Simon Apers, Minbo Gao, Zhengfeng Ji, and Chenghua Liu

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

Abstract
We present a quantum algorithm for sampling random spanning trees from a weighted graph in Õ(√{mn}) time, where n and m denote the number of vertices and edges, respectively. Our algorithm has sublinear runtime for dense graphs and achieves a quantum speedup over the best-known classical algorithm, which runs in Õ(m) time. The approach carefully combines, on one hand, a classical method based on "large-step" random walks for reduced mixing time and, on the other hand, quantum algorithmic techniques, including quantum graph sparsification and a sampling-without-replacement variant of Hamoudi’s multiple-state preparation. We also establish a matching lower bound, proving the optimality of our algorithm up to polylogarithmic factors. These results highlight the potential of quantum computing in accelerating fundamental graph sampling problems.
Cite as

Simon Apers, Minbo Gao, Zhengfeng Ji, and Chenghua Liu. Quantum Speedup for Sampling Random Spanning Trees. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{apers_et_al:LIPIcs.ICALP.2025.13,
  author =	{Apers, Simon and Gao, Minbo and Ji, Zhengfeng and Liu, Chenghua},
  title =	{{Quantum Speedup for Sampling Random Spanning Trees}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{13:1--13:21},
  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.13},
  URN =		{urn:nbn:de:0030-drops-233907},
  doi =		{10.4230/LIPIcs.ICALP.2025.13},
  annote =	{Keywords: Quantum Computing, Quantum Algorithms, Random Spanning Trees}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.128
3.415-Approximation for Coflow Scheduling via Iterated Rounding

Authors: Lars Rohwedder and Leander Schnaars

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

Abstract
We provide an algorithm giving a 140/41 (< 3.415)-approximation for Coflow Scheduling and a 4.36-approximation for Coflow Scheduling with release dates. This improves upon the best known 4- and respectively 5-approximations and addresses an open question posed by Agarwal, Rajakrishnan, Narayan, Agarwal, Shmoys, and Vahdat [Agarwal et al., 2018], Fukunaga [Fukunaga, 2022], and others. We additionally show that in an asymptotic setting, the algorithm achieves a (2+ε)-approximation, which is essentially optimal under ℙ ≠ NP. The improvements are achieved using a novel edge allocation scheme using iterated LP rounding together with a framework which enables establishing strong bounds for combinations of several edge allocation algorithms.
Cite as

Lars Rohwedder and Leander Schnaars. 3.415-Approximation for Coflow Scheduling via Iterated Rounding. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 128:1-128:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rohwedder_et_al:LIPIcs.ICALP.2025.128,
  author =	{Rohwedder, Lars and Schnaars, Leander},
  title =	{{3.415-Approximation for Coflow Scheduling via Iterated Rounding}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{128:1--128: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.128},
  URN =		{urn:nbn:de:0030-drops-235050},
  doi =		{10.4230/LIPIcs.ICALP.2025.128},
  annote =	{Keywords: Coflow Scheduling, Approximation Algorithms, Iterated Rounding}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2025.53
Differential Privacy on Trust Graphs

Authors: Badih Ghazi, Ravi Kumar, Pasin Manurangsi, and Serena Wang

Published in: LIPIcs, Volume 325, 16th Innovations in Theoretical Computer Science Conference (ITCS 2025)

Abstract
We study differential privacy (DP) in a multi-party setting where each party only trusts a (known) subset of the other parties with its data. Specifically, given a trust graph where vertices correspond to parties and neighbors are mutually trusting, we give a DP algorithm for aggregation with a much better privacy-utility trade-off than in the well-studied local model of DP (where each party trusts no other party). We further study a robust variant where each party trusts all but an unknown subset of at most t of its neighbors (where t is a given parameter), and give an algorithm for this setting. We complement our algorithms with lower bounds, and discuss implications of our work to other tasks in private learning and analytics.
Cite as

Badih Ghazi, Ravi Kumar, Pasin Manurangsi, and Serena Wang. Differential Privacy on Trust Graphs. In 16th Innovations in Theoretical Computer Science Conference (ITCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 325, pp. 53:1-53:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghazi_et_al:LIPIcs.ITCS.2025.53,
  author =	{Ghazi, Badih and Kumar, Ravi and Manurangsi, Pasin and Wang, Serena},
  title =	{{Differential Privacy on Trust Graphs}},
  booktitle =	{16th Innovations in Theoretical Computer Science Conference (ITCS 2025)},
  pages =	{53:1--53:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-361-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{325},
  editor =	{Meka, Raghu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2025.53},
  URN =		{urn:nbn:de:0030-drops-226816},
  doi =		{10.4230/LIPIcs.ITCS.2025.53},
  annote =	{Keywords: Differential privacy, trust graphs, minimum dominating set, packing number}
}
Document
DOI: 10.4230/DagRep.14.4.85
Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171)

Authors: S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, Ruzica Piskac, and Arijit Shaw

Published in: Dagstuhl Reports, Volume 14, Issue 4 (2024)

Abstract
This report summarizes the program of Dagstuhl Seminar 24171 on "Automated Synthesis: Functional, Reactive and Beyond". The seminar brought together researchers working on different aspects of functional synthesis and investigated its relationship with reactive synthesis. Through multiple expository tutorials, diverse technical talks, and multiple open discussion sessions, the seminar crystallized the current challenges for theory and tools in this area and opened fresh directions towards new applications.
Cite as

S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, Ruzica Piskac, and Arijit Shaw. Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171). In Dagstuhl Reports, Volume 14, Issue 4, pp. 85-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{akshay_et_al:DagRep.14.4.85,
  author =	{Akshay, S. and Finkbeiner, Bernd and Meel, Kuldeep S. and Piskac, Ruzica and Shaw, Arijit},
  title =	{{Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171)}},
  pages =	{85--107},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{4},
  editor =	{Akshay, S. and Finkbeiner, Bernd and Meel, Kuldeep S. and Piskac, Ruzica and Shaw, Arijit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.4.85},
  URN =		{urn:nbn:de:0030-drops-213515},
  doi =		{10.4230/DagRep.14.4.85},
  annote =	{Keywords: automated synthesis, boolean functions, knowledge representations, reactive synthesis, SAT/SMT solvers}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.5
MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

Authors: S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan

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

Abstract
The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This "de-alternation" step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. An attractive feature of GTAs is the presence of future clocks which act like timers that guess a time to an event and stay alive until a timeout. Future clocks seem to provide another natural way to implement the guess-and-check: start the future clock with a guessed time to an event and check its occurrence using a timeout. Indeed, using this feature, we provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Büchi non-emptiness in GTAs, which circumvents this fundamental challenge.
Cite as

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.5,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{5:1--5:19},
  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.5},
  URN =		{urn:nbn:de:0030-drops-207774},
  doi =		{10.4230/LIPIcs.CONCUR.2024.5},
  annote =	{Keywords: MITL model checking, timed automata, zones, liveness}
}
  • Refine by Type
  • 90 Document/PDF
  • 12 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 12 2025
  • 4 2024
  • 2 2023
  • 3 2022
  • 4 2021
  • Show More...

  • Refine by Author
  • 20 Akshay, S.
  • 6 Gastin, Paul
  • 5 Genest, Blaise
  • 5 Krishna, Shankara Narayanan
  • 3 Srivathsan, B.
  • Show More...

  • Refine by Series/Journal
  • 87 LIPIcs
  • 1 OASIcs
  • 1 TGDK
  • 1 DagRep

  • Refine by Classification
  • 6 Theory of computation → Logic and verification
  • 4 Theory of computation → Timed and hybrid models
  • 2 Theory of computation
  • 2 Theory of computation → Design and analysis of algorithms
  • 2 Theory of computation → Quantitative automata
  • Show More...

  • Refine by Keyword
  • 4 Skolem problem
  • 4 Timed automata
  • 3 Model Checking
  • 2 Algorithms
  • 2 Approximation Algorithms
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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