@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 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},
}
@inproceedings{10003,
abstract = {In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime verification to monitors that attempt to estimate numerical values of quantitative trace properties (instead of attempting to conclude boolean values of trace specifications), such as maximal or average response time along a trace. Quantitative monitors are approximate: with every finite prefix, they can improve their estimate of the infinite trace's unknown property value. Consequently, quantitative monitors can be compared with regard to a precision-cost trade-off: better approximations of the property value require more monitor resources, such as states (in the case of finite-state monitors) or registers, and additional resources yield better approximations. We introduce a formal framework for quantitative and approximate monitoring, show how it conservatively generalizes the classical boolean setting for monitoring, and give several precision-cost trade-offs for monitors. For example, we prove that there are quantitative properties for which every additional register improves monitoring precision.},
author = {Henzinger, Thomas A and Sarac, Naci E},
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, Runtime, Registers, Time factors, Monitoring},
location = {Rome, Italy},
pages = {1--14},
publisher = {Institute of Electrical and Electronics Engineers},
title = {{Quantitative and approximate monitoring}},
doi = {10.1109/LICS52264.2021.9470547},
year = {2021},
}
@article{10024,
abstract = {In this paper, we introduce a random environment for the exclusion process in obtained by assigning a maximal occupancy to each site. This maximal occupancy is allowed to randomly vary among sites, and partial exclusion occurs. Under the assumption of ergodicity under translation and uniform ellipticity of the environment, we derive a quenched hydrodynamic limit in path space by strengthening the mild solution approach initiated in Nagy (2002) and Faggionato (2007). To this purpose, we prove, employing the technology developed for the random conductance model, a homogenization result in the form of an arbitrary starting point quenched invariance principle for a single particle in the same environment, which is a result of independent interest. The self-duality property of the partial exclusion process allows us to transfer this homogenization result to the particle system and, then, apply the tightness criterion in Redig et al. (2020).},
author = {Floreani, Simone and Redig, Frank and Sau, Federico},
issn = {0304-4149},
journal = {Stochastic Processes and their Applications},
keywords = {hydrodynamic limit, random environment, random conductance model, arbitrary starting point quenched invariance principle, duality, mild solution},
pages = {124--158},
publisher = {Elsevier},
title = {{Hydrodynamics for the partial exclusion process in random environment}},
doi = {10.1016/j.spa.2021.08.006},
volume = {142},
year = {2021},
}
@phdthesis{9733,
abstract = {This thesis is the result of the research carried out by the author during his PhD at IST Austria between 2017 and 2021. It mainly focuses on the Fröhlich polaron model, specifically to its regime of strong coupling. This model, which is rigorously introduced and discussed in the introduction, has been of great interest in condensed matter physics and field theory for more than eighty years. It is used to describe an electron interacting with the atoms of a solid material (the strength of this interaction is modeled by the presence of a coupling constant α in the Hamiltonian of the system). The particular regime examined here, which is mathematically described by considering the limit α →∞, displays many interesting features related to the emergence of classical behavior, which allows for a simplified effective description of the system under analysis. The properties, the range of validity and a quantitative analysis of the precision of such classical approximations are the main object of the present work. We specify our investigation to the study of the ground state energy of the system, its dynamics and its effective mass. For each of these problems, we provide in the introduction an overview of the previously known results and a detailed account of the original contributions by the author.},
author = {Feliciangeli, Dario},
issn = {2663-337X},
pages = {180},
publisher = {IST Austria},
title = {{The polaron at strong coupling}},
doi = {10.15479/at:ista:9733},
year = {2021},
}
@article{9428,
abstract = {Thermalization is the inevitable fate of many complex quantum systems, whose dynamics allow them to fully explore the vast configuration space regardless of the initial state---the behaviour known as quantum ergodicity. In a quest for experimental realizations of coherent long-time dynamics, efforts have focused on ergodicity-breaking mechanisms, such as integrability and localization. The recent discovery of persistent revivals in quantum simulators based on Rydberg atoms have pointed to the existence of a new type of behaviour where the system rapidly relaxes for most initial conditions, while certain initial states give rise to non-ergodic dynamics. This collective effect has been named ”quantum many-body scarring’by analogy with a related form of weak ergodicity breaking that occurs for a single particle inside a stadium billiard potential. In this Review, we provide a pedagogical introduction to quantum many-body scars and highlight the emerging connections with the semiclassical quantization of many-body systems. We discuss the relation between scars and more general routes towards weak violations of ergodicity due to embedded algebras and non-thermal eigenstates, and highlight possible applications of scars in quantum technology.},
author = {Serbyn, Maksym and Abanin, Dmitry A. and Papić, Zlatko},
issn = {1745-2481},
journal = {Nature Physics},
number = {6},
pages = {675–685},
title = {{Quantum many-body scars and weak breaking of ergodicity}},
doi = {10.1038/s41567-021-01230-2},
volume = {17},
year = {2021},
}
@article{9999,
abstract = {The developmental strategies used by progenitor cells to endure a safe journey from their induction place towards the site of terminal differentiation are still poorly understood. Here we uncovered a progenitor cell allocation mechanism that stems from an incomplete process of epithelial delamination that allows progenitors to coordinate their movement with adjacent extra-embryonic tissues. Progenitors of the zebrafish laterality organ originate from the surface epithelial enveloping layer by an apical constriction process of cell delamination. During this process, progenitors retain long-term apical contacts that enable the epithelial layer to pull a subset of progenitors along their way towards the vegetal pole. The remaining delaminated progenitors follow apically-attached progenitors’ movement by a co-attraction mechanism, avoiding sequestration by the adjacent endoderm, ensuring their fate and collective allocation at the differentiation site. Thus, we reveal that incomplete delamination serves as a cellular platform for coordinated tissue movements during development. Impact Statement: Incomplete delamination serves as a cellular platform for coordinated tissue movements during development, guiding newly formed progenitor cell groups to the differentiation site.},
author = {Pulgar, Eduardo and Schwayer, Cornelia and Guerrero, Néstor and López, Loreto and Márquez, Susana and Härtel, Steffen and Soto, Rodrigo and Heisenberg, Carl Philipp and Concha, Miguel L.},
issn = {2050-084X},
journal = {eLife},
keywords = {cell delamination, apical constriction, dragging, mechanical forces, collective 18 locomotion, dorsal forerunner cells, zebrafish},
publisher = {eLife Sciences Publications},
title = {{Apical contacts stemming from incomplete delamination guide progenitor cell allocation through a dragging mechanism}},
doi = {10.7554/eLife.66483},
volume = {10},
year = {2021},
}
@article{10023,
abstract = {We study the temporal dissipation of variance and relative entropy for ergodic Markov Chains in continuous time, and compute explicitly the corresponding dissipation rates. These are identified, as is well known, in the case of the variance in terms of an appropriate Hilbertian norm; and in the case of the relative entropy, in terms of a Dirichlet form which morphs into a version of the familiar Fisher information under conditions of detailed balance. Here we obtain trajectorial versions of these results, valid along almost every path of the random motion and most transparent in the backwards direction of time. Martingale arguments and time reversal play crucial roles, as in the recent work of Karatzas, Schachermayer and Tschiderer for conservative diffusions. Extensions are developed to general “convex divergences” and to countable state-spaces. The steepest descent and gradient flow properties for the variance, the relative entropy, and appropriate generalizations, are studied along with their respective geometries under conditions of detailed balance, leading to a very direct proof for the HWI inequality of Otto and Villani in the present context.},
author = {Karatzas, Ioannis and Maas, Jan and Schachermayer, Walter},
issn = {1526-7555},
journal = {Communications in Information and Systems},
keywords = {Markov Chain, relative entropy, time reversal, steepest descent, gradient flow},
number = {4},
pages = {481--536},
publisher = {International Press},
title = {{Trajectorial dissipation and gradient flow for the relative entropy in Markov chains}},
doi = {10.4310/CIS.2021.v21.n4.a1},
volume = {21},
year = {2021},
}
@article{9250,
abstract = {Aprotic alkali metal–O2 batteries face two major obstacles to their chemistry occurring efficiently, the insulating nature of the formed alkali superoxides/peroxides and parasitic reactions that are caused by the highly reactive singlet oxygen (1O2). Redox mediators are recognized to be key for improving rechargeability. However, it is unclear how they affect 1O2 formation, which hinders strategies for their improvement. Here we clarify the mechanism of mediated peroxide and superoxide oxidation and thus explain how redox mediators either enhance or suppress 1O2 formation. We show that charging commences with peroxide oxidation to a superoxide intermediate and that redox potentials above ~3.5 V versus Li/Li+ drive 1O2 evolution from superoxide oxidation, while disproportionation always generates some 1O2. We find that 1O2 suppression requires oxidation to be faster than the generation of 1O2 from disproportionation. Oxidation rates decrease with growing driving force following Marcus inverted-region behaviour, establishing a region of maximum rate.},
author = {Petit, Yann K. and Mourad, Eléonore and Prehal, Christian and Leypold, Christian and Windischbacher, Andreas and Mijailovic, Daniel and Slugovc, Christian and Borisov, Sergey M. and Zojer, Egbert and Brutti, Sergio and Fontaine, Olivier and Freunberger, Stefan Alexander},
issn = {1755-4330},
journal = {Nature Chemistry},
keywords = {General Chemistry, General Chemical Engineering},
number = {5},
pages = {465--471},
publisher = {Springer Nature},
title = {{Mechanism of mediated alkali peroxide oxidation and triplet versus singlet oxygen formation}},
doi = {10.1038/s41557-021-00643-z},
volume = {13},
year = {2021},
}
@phdthesis{9992,
abstract = {Blood – this is what animals use to heal wounds fast and efficient. Plants do not have blood circulation and their cells cannot move. However, plants have evolved remarkable capacities to regenerate tissues and organs preventing further damage. In my PhD research, I studied the wound healing in the Arabidopsis root. I used a UV laser to ablate single cells in the root tip and observed the consequent wound healing. Interestingly, the inner adjacent cells induced a
division plane switch and subsequently adopted the cell type of the killed cell to replace it. We termed this form of wound healing “restorative divisions”. This initial observation triggered the questions of my PhD studies: How and why do cells orient their division planes, how do they feel the wound and why does this happen only in inner adjacent cells.
For answering these questions, I used a quite simple experimental setup: 5 day - old seedlings were stained with propidium iodide to visualize cell walls and dead cells; ablation was carried out using a special laser cutter and a confocal microscope. Adaptation of the novel vertical microscope system made it possible to observe wounds in real time. This revealed that restorative divisions occur at increased frequency compared to normal divisions. Additionally,
the major plant hormone auxin accumulates in wound adjacent cells and drives the expression of the wound-stress responsive transcription factor ERF115. Using this as a marker gene for wound responses, we found that an important part of wound signalling is the sensing of the collapse of the ablated cell. The collapse causes a radical pressure drop, which results in strong tissue deformations. These deformations manifest in an invasion of the now free spot specifically by the inner adjacent cells within seconds, probably because of higher pressure of the inner tissues. Long-term imaging revealed that those deformed cells continuously expand towards the wound hole and that this is crucial for the restorative division. These wound-expanding cells exhibit an abnormal, biphasic polarity of microtubule arrays
before the division. Experiments inhibiting cell expansion suggest that it is the biphasic stretching that induces those MT arrays. Adapting the micromanipulator aspiration system from animal scientists at our institute confirmed the hypothesis that stretching influences microtubule stability. In conclusion, this shows that microtubules react to tissue deformation
and this facilitates the observed division plane switch. This puts mechanical cues and tensions at the most prominent position for explaining the growth and wound healing properties of plants. Hence, it shines light onto the importance of understanding mechanical signal transduction. },
author = {Hörmayer, Lukas},
issn = {2663-337X},
pages = {168},
publisher = {IST Austria},
title = {{Wound healing in the Arabidopsis root meristem}},
doi = {10.15479/at:ista:9992},
year = {2021},
}