@article{12164, abstract = {A shared-memory counter is a widely-used and well-studied concurrent object. It supports two operations: An Inc operation that increases its value by 1 and a Read operation that returns its current value. In Jayanti et al (SIAM J Comput, 30(2), 2000), Jayanti, Tan and Toueg proved a linear lower bound on the worst-case step complexity of obstruction-free implementations, from read-write registers, of a large class of shared objects that includes counters. The lower bound leaves open the question of finding counter implementations with sub-linear amortized step complexity. In this work, we address this gap. We show that n-process, wait-free and linearizable counters can be implemented from read-write registers with O(log2n) amortized step complexity. This is the first counter algorithm from read-write registers that provides sub-linear amortized step complexity in executions of arbitrary length. Since a logarithmic lower bound on the amortized step complexity of obstruction-free counter implementations exists, our upper bound is within a logarithmic factor of the optimal. The worst-case step complexity of the construction remains linear, which is optimal. This is obtained thanks to a new max register construction with O(logn) amortized step complexity in executions of arbitrary length in which the value stored in the register does not grow too quickly. We then leverage an existing counter algorithm by Aspnes, Attiya and Censor-Hillel [1] in which we “plug” our max register implementation to show that it remains linearizable while achieving O(log2n) amortized step complexity.}, author = {Baig, Mirza Ahad and Hendler, Danny and Milani, Alessia and Travers, Corentin}, issn = {1432-0452}, journal = {Distributed Computing}, keywords = {Computational Theory and Mathematics, Computer Networks and Communications, Hardware and Architecture, Theoretical Computer Science}, pages = {29--43}, publisher = {Springer Nature}, title = {{Long-lived counters with polylogarithmic amortized step complexity}}, doi = {10.1007/s00446-022-00439-5}, volume = {36}, year = {2023}, } @article{12287, abstract = {We present criteria for establishing a triangulation of a manifold. Given a manifold M, a simplicial complex A, and a map H from the underlying space of A to M, our criteria are presented in local coordinate charts for M, and ensure that H is a homeomorphism. These criteria do not require a differentiable structure, or even an explicit metric on M. No Delaunay property of A is assumed. The result provides a triangulation guarantee for algorithms that construct a simplicial complex by working in local coordinate patches. Because the criteria are easily verified in such a setting, they are expected to be of general use.}, author = {Boissonnat, Jean-Daniel and Dyer, Ramsay and Ghosh, Arijit and Wintraecken, Mathijs}, issn = {1432-0444}, journal = {Discrete & Computational Geometry}, keywords = {Computational Theory and Mathematics, Discrete Mathematics and Combinatorics, Geometry and Topology, Theoretical Computer Science}, pages = {156--191}, publisher = {Springer Nature}, title = {{Local criteria for triangulating general manifolds}}, doi = {10.1007/s00454-022-00431-7}, volume = {69}, year = {2023}, } @article{12563, abstract = {he approximate graph coloring problem, whose complexity is unresolved in most cases, concerns finding a c-coloring of a graph that is promised to be k-colorable, where c≥k. This problem naturally generalizes to promise graph homomorphism problems and further to promise constraint satisfaction problems. The complexity of these problems has recently been studied through an algebraic approach. In this paper, we introduce two new techniques to analyze the complexity of promise CSPs: one is based on topology and the other on adjunction. We apply these techniques, together with the previously introduced algebraic approach, to obtain new unconditional NP-hardness results for a significant class of approximate graph coloring and promise graph homomorphism problems.}, author = {Krokhin, Andrei and Opršal, Jakub and Wrochna, Marcin and Živný, Stanislav}, issn = {1095-7111}, journal = {SIAM Journal on Computing}, keywords = {General Mathematics, General Computer Science}, number = {1}, pages = {38--79}, publisher = {Society for Industrial & Applied Mathematics}, title = {{Topology and adjunction in promise constraint satisfaction}}, doi = {10.1137/20m1378223}, volume = {52}, year = {2023}, } @article{13988, abstract = {Most permissionless blockchains inherently suffer from throughput limitations. Layer-2 systems, such as side-chains or Rollups, have been proposed as a possible strategy to overcome this limitation. Layer-2 systems interact with the main-chain in two ways. First, users can move funds from/to the main-chain to/from the layer-2. Second, layer-2 systems periodically synchronize with the main-chain to keep some form of log of their activity on the main-chain - this log is key for security. Due to this interaction with the main-chain, which is necessary and recurrent, layer-2 systems impose some load on the main-chain. The impact of such load on the main-chain has been, so far, poorly understood. In addition to that, layer-2 approaches typically sacrifice decentralization and security in favor of higher throughput. This paper presents an experimental study that analyzes the current state of Ethereum layer-2 projects. Our goal is to assess the load they impose on Ethereum and to understand their scalability potential in the long-run. Our analysis shows that the impact of any given layer-2 on the main-chain is the result of both technical aspects (how state is logged on the main-chain) and user behavior (how often users decide to transfer funds between the layer-2 and the main-chain). Based on our observations, we infer that without efficient mechanisms that allow users to transfer funds in a secure and fast manner directly from one layer-2 project to another, current layer-2 systems will not be able to scale Ethereum effectively, regardless of their technical solutions. Furthermore, from our results, we conclude that the layer-2 systems that offer similar security guarantees as Ethereum have limited scalability potential, while approaches that offer better performance, sacrifice security and lead to an increase in centralization which runs against the end-goals of permissionless blockchains.}, author = {Neiheiser, Ray and Inacio, Gustavo and Rech, Luciana and Montez, Carlos and Matos, Miguel and Rodrigues, Luis}, issn = {2169-3536}, journal = {IEEE Access}, keywords = {General Engineering, General Materials Science, General Computer Science, Electrical and Electronic Engineering}, pages = {8651--8662}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Practical limitations of Ethereum’s layer-2}}, doi = {10.1109/access.2023.3237897}, volume = {11}, year = {2023}, } @article{14751, abstract = {We consider zero-error communication over a two-transmitter deterministic adversarial multiple access channel (MAC) governed by an adversary who has access to the transmissions of both senders (hence called omniscient ) and aims to maliciously corrupt the communication. None of the encoders, jammer and decoder is allowed to randomize using private or public randomness. This enforces a combinatorial nature of the problem. Our model covers a large family of channels studied in the literature, including all deterministic discrete memoryless noisy or noiseless MACs. In this work, given an arbitrary two-transmitter deterministic omniscient adversarial MAC, we characterize when the capacity region: 1) has nonempty interior (in particular, is two-dimensional); 2) consists of two line segments (in particular, has empty interior); 3) consists of one line segment (in particular, is one-dimensional); 4) or only contains (0,0) (in particular, is zero-dimensional). This extends a recent result by Wang et al. (201 9) from the point-to-point setting to the multiple access setting. Indeed, our converse arguments build upon their generalized Plotkin bound and involve delicate case analysis. One of the technical challenges is to take care of both “joint confusability” and “marginal confusability”. In particular, the treatment of marginal confusability does not follow from the point-to-point results by Wang et al. Our achievability results follow from random coding with expurgation.}, author = {Zhang, Yihan}, issn = {1557-9654}, journal = {IEEE Transactions on Information Theory}, keywords = {Computer Science Applications, Information Systems}, number = {7}, pages = {4093--4127}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Zero-error communication over adversarial MACs}}, doi = {10.1109/tit.2023.3257239}, volume = {69}, year = {2023}, } @article{14776, abstract = {Soluble chaperones residing in the endoplasmic reticulum (ER) play vitally important roles in folding and quality control of newly synthesized proteins that transiently pass through the ER en route to their final destinations. These soluble residents of the ER are themselves endowed with an ER retrieval signal that enables the cell to bring the escaped residents back from the Golgi. Here, by using purified proteins, we showed that Nicotiana tabacum phytaspase, a plant aspartate-specific protease, introduces two breaks at the C-terminus of the N. tabacum ER resident calreticulin-3. These cleavages resulted in removal of either a dipeptide or a hexapeptide from the C-terminus of calreticulin-3 encompassing part or all of the ER retrieval signal. Consistently, expression of the calreticulin-3 derivative mimicking the phytaspase cleavage product in Nicotiana benthamiana cells demonstrated loss of the ER accumulation of the protein. Notably, upon its escape from the ER, calreticulin-3 was further processed by an unknown protease(s) to generate the free N-terminal (N) domain of calreticulin-3, which was ultimately secreted into the apoplast. Our study thus identified a specific proteolytic enzyme capable of precise detachment of the ER retrieval signal from a plant ER resident protein, with implications for the further fate of the escaped resident.}, author = {Teplova, Anastasiia and Pigidanov, Artemii A. and Serebryakova, Marina V. and Golyshev, Sergei A. and Galiullina, Raisa A. and Chichkova, Nina V. and Vartapetian, Andrey B.}, issn = {1422-0067}, journal = {International Journal of Molecular Sciences}, keywords = {Inorganic Chemistry, Organic Chemistry, Physical and Theoretical Chemistry, Computer Science Applications, Spectroscopy, Molecular Biology, General Medicine, Catalysis}, number = {22}, publisher = {MDPI}, title = {{Phytaspase Is capable of detaching the endoplasmic reticulum retrieval signal from tobacco calreticulin-3}}, doi = {10.3390/ijms242216527}, volume = {24}, year = {2023}, } @article{14778, abstract = {We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshady, Ehsan and Novotný, Petr and Zárevúcky, Jiří and Zikelic, Dorde}, issn = {1433-299X}, journal = {Formal Aspects of Computing}, keywords = {Theoretical Computer Science, Software}, number = {2}, publisher = {Association for Computing Machinery}, title = {{On lexicographic proof rules for probabilistic termination}}, doi = {10.1145/3585391}, volume = {35}, year = {2023}, } @article{12154, abstract = {We review our theoretical results of the sound propagation in two-dimensional (2D) systems of ultracold fermionic and bosonic atoms. In the superfluid phase, characterized by the spontaneous symmetry breaking of the U(1) symmetry, there is the coexistence of first and second sound. In the case of weakly-interacting repulsive bosons, we model the recent measurements of the sound velocities of 39K atoms in 2D obtained in the weakly-interacting regime and around the Berezinskii–Kosterlitz–Thouless (BKT) superfluid-to-normal transition temperature. In particular, we perform a quite accurate computation of the superfluid density and show that it is reasonably consistent with the experimental results. For superfluid attractive fermions, we calculate the first and second sound velocities across the whole BCS-BEC crossover. In the low-temperature regime, we reproduce the recent measurements of first-sound speed with 6Li atoms. We also predict that there is mixing between sound modes only in the finite-temperature BEC regime.}, author = {Salasnich, Luca and Cappellaro, Alberto and Furutani, Koichiro and Tononi, Andrea and Bighin, Giacomo}, issn = {2073-8994}, journal = {Symmetry}, keywords = {Physics and Astronomy (miscellaneous), General Mathematics, Chemistry (miscellaneous), Computer Science (miscellaneous)}, number = {10}, publisher = {MDPI}, title = {{First and second sound in two-dimensional bosonic and fermionic superfluids}}, doi = {10.3390/sym14102182}, volume = {14}, year = {2022}, } @article{12156, abstract = {Models of transcriptional regulation that assume equilibrium binding of transcription factors have been less successful at predicting gene expression from sequence in eukaryotes than in bacteria. This could be due to the non-equilibrium nature of eukaryotic regulation. Unfortunately, the space of possible non-equilibrium mechanisms is vast and predominantly uninteresting. The key question is therefore how this space can be navigated efficiently, to focus on mechanisms and models that are biologically relevant. In this review, we advocate for the normative role of theory—theory that prescribes rather than just describes—in providing such a focus. Theory should expand its remit beyond inferring mechanistic models from data, towards identifying non-equilibrium gene regulatory schemes that may have been evolutionarily selected, despite their energy consumption, because they are precise, reliable, fast, or otherwise outperform regulation at equilibrium. We illustrate our reasoning by toy examples for which we provide simulation code.}, author = {Zoller, Benjamin and Gregor, Thomas and Tkačik, Gašper}, issn = {2452-3100}, journal = {Current Opinion in Systems Biology}, keywords = {Applied Mathematics, Computer Science Applications, Drug Discovery, General Biochemistry, Genetics and Molecular Biology, Modeling and Simulation}, number = {9}, publisher = {Elsevier}, title = {{Eukaryotic gene regulation at equilibrium, or non?}}, doi = {10.1016/j.coisb.2022.100435}, volume = {31}, year = {2022}, } @article{12286, abstract = {Inspired by the study of loose cycles in hypergraphs, we define the loose core in hypergraphs as a structurewhich mirrors the close relationship between cycles and $2$-cores in graphs. We prove that in the $r$-uniform binomial random hypergraph $H^r(n,p)$, the order of the loose core undergoes a phase transition at a certain critical threshold and determine this order, as well as the number of edges, asymptotically in the subcritical and supercritical regimes. Our main tool is an algorithm called CoreConstruct, which enables us to analyse a peeling process for the loose core. By analysing this algorithm we determine the asymptotic degree distribution of vertices in the loose core and in particular how many vertices and edges the loose core contains. As a corollary we obtain an improved upper bound on the length of the longest loose cycle in $H^r(n,p)$.}, author = {Cooley, Oliver and Kang, Mihyun and Zalla, Julian}, issn = {1077-8926}, journal = {The Electronic Journal of Combinatorics}, keywords = {Computational Theory and Mathematics, Geometry and Topology, Theoretical Computer Science, Applied Mathematics, Discrete Mathematics and Combinatorics}, number = {4}, publisher = {The Electronic Journal of Combinatorics}, title = {{Loose cores and cycles in random hypergraphs}}, doi = {10.37236/10794}, volume = {29}, year = {2022}, } @article{9311, abstract = {Partially observable Markov decision processes (POMDPs) are standard models for dynamic systems with probabilistic and nondeterministic behaviour in uncertain environments. We prove that in POMDPs with long-run average objective, the decision maker has approximately optimal strategies with finite memory. This implies notably that approximating the long-run value is recursively enumerable, as well as a weak continuity property of the value with respect to the transition function. }, author = {Chatterjee, Krishnendu and Saona Urmeneta, Raimundo J and Ziliotto, Bruno}, issn = {1526-5471}, journal = {Mathematics of Operations Research}, keywords = {Management Science and Operations Research, General Mathematics, Computer Science Applications}, number = {1}, pages = {100--119}, publisher = {Institute for Operations Research and the Management Sciences}, title = {{Finite-memory strategies in POMDPs with long-run average objectives}}, doi = {10.1287/moor.2020.1116}, volume = {47}, year = {2022}, } @article{10208, abstract = {It is practical to collect a huge amount of movement data and environmental context information along with the health signals of individuals because there is the emergence of new generations of positioning and tracking technologies and rapid advancements of health sensors. The study of the relations between these datasets and their sequence similarity analysis is of interest to many applications such as health monitoring and recommender systems. However, entering all movement parameters and health signals can lead to the complexity of the problem and an increase in its computational load. In this situation, dimension reduction techniques can be used to avoid consideration of simultaneous dependent parameters in the process of similarity measurement of the trajectories. The present study provides a framework, named CaDRAW, to use spatial–temporal data and movement parameters along with independent context information in the process of measuring the similarity of trajectories. In this regard, the omission of dependent movement characteristic signals is conducted by using an unsupervised feature selection dimension reduction technique. To evaluate the effectiveness of the proposed framework, it was applied to a real contextualized movement and related health signal datasets of individuals. The results indicated the capability of the proposed framework in measuring the similarity and in decreasing the characteristic signals in such a way that the similarity results -before and after reduction of dependent characteristic signals- have small differences. The mean differences between the obtained results before and after reducing the dimension were 0.029 and 0.023 for the round path, respectively.}, author = {Goudarzi, Samira and Sharif, Mohammad and Karimipour, Farid}, issn = {1868-5145}, journal = {Journal of Ambient Intelligence and Humanized Computing}, keywords = {general computer science}, pages = {2621–2635}, publisher = {Springer Nature}, title = {{A context-aware dimension reduction framework for trajectory and health signal analyses}}, doi = {10.1007/s12652-021-03569-z}, volume = {13}, year = {2022}, } @article{10643, abstract = {We prove a generalised super-adiabatic theorem for extended fermionic systems assuming a spectral gap only in the bulk. More precisely, we assume that the infinite system has a unique ground state and that the corresponding Gelfand–Naimark–Segal Hamiltonian has a spectral gap above its eigenvalue zero. Moreover, we show that a similar adiabatic theorem also holds in the bulk of finite systems up to errors that vanish faster than any inverse power of the system size, although the corresponding finite-volume Hamiltonians need not have a spectral gap. }, author = {Henheik, Sven Joscha and Teufel, Stefan}, issn = {2050-5094}, journal = {Forum of Mathematics, Sigma}, keywords = {computational mathematics, discrete mathematics and combinatorics, geometry and topology, mathematical physics, statistics and probability, algebra and number theory, theoretical computer science, analysis}, publisher = {Cambridge University Press}, title = {{Adiabatic theorem in the thermodynamic limit: Systems with a gap in the bulk}}, doi = {10.1017/fms.2021.80}, volume = {10}, year = {2022}, } @article{11556, abstract = {We revisit two basic Direct Simulation Monte Carlo Methods to model aggregation kinetics and extend them for aggregation processes with collisional fragmentation (shattering). We test the performance and accuracy of the extended methods and compare their performance with efficient deterministic finite-difference method applied to the same model. We validate the stochastic methods on the test problems and apply them to verify the existence of oscillating regimes in the aggregation-fragmentation kinetics recently detected in deterministic simulations. We confirm the emergence of steady oscillations of densities in such systems and prove the stability of the oscillations with respect to fluctuations and noise.}, author = {Kalinov, Aleksei and Osinskiy, A.I. and Matveev, S.A. and Otieno, W. and Brilliantov, N.V.}, issn = {0021-9991}, journal = {Journal of Computational Physics}, keywords = {Computer Science Applications, Physics and Astronomy (miscellaneous), Applied Mathematics, Computational Mathematics, Modeling and Simulation, Numerical Analysis}, publisher = {Elsevier}, title = {{Direct simulation Monte Carlo for new regimes in aggregation-fragmentation kinetics}}, doi = {10.1016/j.jcp.2022.111439}, volume = {467}, year = {2022}, } @article{12129, abstract = {Given a finite point set P in general position in the plane, a full triangulation of P is a maximal straight-line embedded plane graph on P. A partial triangulation of P is a full triangulation of some subset P′ of P containing all extreme points in P. A bistellar flip on a partial triangulation either flips an edge (called edge flip), removes a non-extreme point of degree 3, or adds a point in P∖P′ as vertex of degree 3. The bistellar flip graph has all partial triangulations as vertices, and a pair of partial triangulations is adjacent if they can be obtained from one another by a bistellar flip. The edge flip graph is defined with full triangulations as vertices, and edge flips determining the adjacencies. Lawson showed in the early seventies that these graphs are connected. The goal of this paper is to investigate the structure of these graphs, with emphasis on their vertex connectivity. For sets P of n points in the plane in general position, we show that the edge flip graph is ⌈n/2−2⌉-vertex connected, and the bistellar flip graph is (n−3)-vertex connected; both results are tight. The latter bound matches the situation for the subfamily of regular triangulations (i.e., partial triangulations obtained by lifting the points to 3-space and projecting back the lower convex hull), where (n−3)-vertex connectivity has been known since the late eighties through the secondary polytope due to Gelfand, Kapranov, & Zelevinsky and Balinski’s Theorem. For the edge flip-graph, we additionally show that the vertex connectivity is at least as large as (and hence equal to) the minimum degree (i.e., the minimum number of flippable edges in any full triangulation), provided that n is large enough. Our methods also yield several other results: (i) The edge flip graph can be covered by graphs of polytopes of dimension ⌈n/2−2⌉ (products of associahedra) and the bistellar flip graph can be covered by graphs of polytopes of dimension n−3 (products of secondary polytopes). (ii) A partial triangulation is regular, if it has distance n−3 in the Hasse diagram of the partial order of partial subdivisions from the trivial subdivision. (iii) All partial triangulations of a point set are regular iff the partial order of partial subdivisions has height n−3. (iv) There are arbitrarily large sets P with non-regular partial triangulations and such that every proper subset has only regular triangulations, i.e., there are no small certificates for the existence of non-regular triangulations.}, author = {Wagner, Uli and Welzl, Emo}, issn = {1432-0444}, journal = {Discrete & Computational Geometry}, keywords = {Computational Theory and Mathematics, Discrete Mathematics and Combinatorics, Geometry and Topology, Theoretical Computer Science}, number = {4}, pages = {1227--1284}, publisher = {Springer Nature}, title = {{Connectivity of triangulation flip graphs in the plane}}, doi = {10.1007/s00454-022-00436-2}, volume = {68}, year = {2022}, } @article{12134, abstract = {Standard epidemic models exhibit one continuous, second order phase transition to macroscopic outbreaks. However, interventions to control outbreaks may fundamentally alter epidemic dynamics. Here we reveal how such interventions modify the type of phase transition. In particular, we uncover three distinct types of explosive phase transitions for epidemic dynamics with capacity-limited interventions. Depending on the capacity limit, interventions may (i) leave the standard second order phase transition unchanged but exponentially suppress the probability of large outbreaks, (ii) induce a first-order discontinuous transition to macroscopic outbreaks, or (iii) cause a secondary explosive yet continuous third-order transition. These insights highlight inherent limitations in predicting and containing epidemic outbreaks. More generally our study offers a cornerstone example of a third-order explosive phase transition in complex systems.}, author = {Börner, Georg and Schröder, Malte and Scarselli, Davide and Budanur, Nazmi B and Hof, Björn and Timme, Marc}, issn = {2632-072X}, journal = {Journal of Physics: Complexity}, keywords = {Artificial Intelligence, Computer Networks and Communications, Computer Science Applications, Information Systems}, number = {4}, publisher = {IOP Publishing}, title = {{Explosive transitions in epidemic dynamics}}, doi = {10.1088/2632-072x/ac99cd}, volume = {3}, year = {2022}, } @article{12148, abstract = {We prove a general local law for Wigner matrices that optimally handles observables of arbitrary rank and thus unifies the well-known averaged and isotropic local laws. As an application, we prove a central limit theorem in quantum unique ergodicity (QUE): that is, we show that the quadratic forms of a general deterministic matrix A on the bulk eigenvectors of a Wigner matrix have approximately Gaussian fluctuation. For the bulk spectrum, we thus generalise our previous result [17] as valid for test matrices A of large rank as well as the result of Benigni and Lopatto [7] as valid for specific small-rank observables.}, author = {Cipolloni, Giorgio and Erdös, László and Schröder, Dominik J}, issn = {2050-5094}, journal = {Forum of Mathematics, Sigma}, keywords = {Computational Mathematics, Discrete Mathematics and Combinatorics, Geometry and Topology, Mathematical Physics, Statistics and Probability, Algebra and Number Theory, Theoretical Computer Science, Analysis}, publisher = {Cambridge University Press}, title = {{Rank-uniform local law for Wigner matrices}}, doi = {10.1017/fms.2022.86}, volume = {10}, year = {2022}, } @article{8940, abstract = {We quantise Whitney’s construction to prove the existence of a triangulation for any C^2 manifold, so that we get an algorithm with explicit bounds. We also give a new elementary proof, which is completely geometric.}, author = {Boissonnat, Jean-Daniel and Kachanovich, Siargey and Wintraecken, Mathijs}, issn = {1432-0444}, journal = {Discrete & Computational Geometry}, keywords = {Theoretical Computer Science, Computational Theory and Mathematics, Geometry and Topology, Discrete Mathematics and Combinatorics}, number = {1}, pages = {386--434}, publisher = {Springer Nature}, title = {{Triangulating submanifolds: An elementary and quantified version of Whitney’s method}}, doi = {10.1007/s00454-020-00250-8}, volume = {66}, year = {2021}, } @inproceedings{10002, abstract = {We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(nm−−√) symbolic operations and O(m−−√) symbolic space. A main open question is whether the worst-case O(n2) bound for symbolic operations can be beaten. We present a symbolic algorithm that requires O˜(n1.5) symbolic operations and O˜(n−−√) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0<ϵ≤1/2 the symbolic algorithm requires O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space ( O˜ hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of ω -regular objectives for MDPs. We consider the canonical parity objectives for ω -regular objectives, and for parity objectives with d -priorities we present an algorithm that computes the almost-sure winning region with O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space, for all 0<ϵ≤1/2 .}, author = {Chatterjee, Krishnendu and Dvorak, Wolfgang and Henzinger, Monika H and Svozil, Alexander}, booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science}, isbn = {978-1-6654-4896-3}, issn = {1043-6871}, keywords = {Computer science, Computational modeling, Markov processes, Probabilistic logic, Formal verification, Game Theory}, location = {Rome, Italy}, pages = {1--13}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Symbolic time and space tradeoffs for probabilistic verification}}, doi = {10.1109/LICS52264.2021.9470739}, year = {2021}, } @inproceedings{10004, abstract = {Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science}, isbn = {978-1-6654-4896-3}, issn = {1043-6871}, keywords = {Computer science, Heuristic algorithms, Memory management, Automata, Markov processes, Probability distribution, Complexity theory}, location = {Rome, Italy}, pages = {1--13}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Stochastic processes with expected stopping time}}, doi = {10.1109/LICS52264.2021.9470595}, year = {2021}, }