@article{18764,
  abstract     = {We prove that a class of weakly perturbed Hamiltonians of the form H_λ= H_0 + λW, with W being a Wigner matrix, exhibits prethermalization. That is, the time evolution generated by H_λ relaxes to its ultimate thermal state via an intermediate prethermal state with a lifetime of order λ^{-2}. Moreover, we obtain a general relaxation formula, expressing the perturbed dynamics via the unperturbed dynamics and the ultimate thermal state. The proof relies on a two-resolvent law for the deformed Wigner matrix H_λ.},
  author       = {Erdös, László and Henheik, Sven Joscha and Reker, Jana and Riabov, Volodymyr},
  issn         = {1424-0637},
  journal      = {Annales Henri Poincare},
  pages        = {1991--2033},
  publisher    = {Springer Nature},
  title        = {{Prethermalization for deformed Wigner matrices}},
  doi          = {10.1007/s00023-024-01518-y},
  volume       = {26},
  year         = {2025},
}

@unpublished{19552,
  abstract     = {Particle creation terms in quantum Hamiltonians are usually ultraviolet
divergent and thus mathematically ill defined. A rather novel way of solving
this problem is based on imposing so-called interior-boundary conditions on the
wave function. Previous papers showed that this approach works in the
non-relativistic regime, but particle creation is mostly relevant in the
relativistic case after all. In flat relativistic space-time (that is,
neglecting gravity), the approach was previously found to work only for certain
somewhat artificial cases. Here, as a way of taking gravity into account, we
consider curved space-time, specifically the super-critical
Reissner-Nordstr\"om space-time, which features a naked timelike singularity.
We find that the interior-boundary approach works fully in this setting; in
particular, we prove rigorously the existence of well-defined, self-adjoint
Hamiltonians with particle creation at the singularity, based on
interior-boundary conditions. We also non-rigorously analyze the asymptotic
behavior of the Bohmian trajectories and construct the corresponding Bohm-Bell
process of particle creation, motion, and annihilation. The upshot is that in
quantum physics, a naked space-time singularity need not lead to a breakdown of
physical laws, but on the contrary allows for boundary conditions governing
what comes out of the singularity and thereby removing the ultraviolet
divergence.},
  author       = {Henheik, Sven Joscha and Poudyal, Bipul and Tumulka, Roderich},
  booktitle    = {arXiv},
  title        = {{How a space-time singularity helps remove the ultraviolet divergence problem}},
  doi          = {10.48550/arXiv.2409.00677},
  year         = {2025},
}

@article{19785,
  abstract     = {We consider a family of totally asymmetric simple exclusion processes (TASEPs), consisting of particles on a lattice that require binding by a “token” in various physical configurations to advance over the lattice. Using a combination of theory and simulations, we address the following questions: (i) How does token binding kinetics affect the current-density relation on the lattice? (ii) How does this current-density relation depend on the scarcity of tokens? (iii) How do tokens propagate the effects of the locally imposed disorder (such as a slow site) over the entire lattice? (iv) How does a shared pool of tokens couple concurrent TASEPs running on multiple lattices? and (v) How do our results translate to TASEPs with open boundaries that exchange particles with the reservoir? Since real particle motion (including in biological systems that inspired the standard TASEP model, e.g., protein synthesis or movement of molecular motors) is often catalyzed, regulated, actuated, or otherwise mediated, the token-driven TASEP dynamics analyzed in this paper should allow for a better understanding of real systems and enable a closer match between TASEP theory and experimental observations.},
  author       = {Kavcic, Bor and Tkačik, Gašper},
  issn         = {2470-0053},
  journal      = {Physical Review E},
  number       = {5},
  publisher    = {American Physical Society},
  title        = {{Token-driven totally asymmetric simple exclusion processes}},
  doi          = {10.1103/physreve.111.054122},
  volume       = {111},
  year         = {2025},
}

@misc{20641,
  abstract     = {Protein conformational energy landscapes are shaped not only by intramolecular interactions but also by their environment. In protein crystals and protein-protein complexes, intermolecular contacts alter this energy landscape, but the exact nature of this alteration is difficult to decipher. Understanding how the crystal lattice affects protein dynamics is crucial for crystallography-based studies of motion, yet its influence on collective motions remains unclear. Aromatic ring flips in the hydrophobic core represent sensitive probes of such dynamics. Here, we compare the kinetics of aromatic ring flips in the protein GB1 in crystals, in complex with its binding partner IgG, and in solution, combining advanced isotope labeling with quantitative NMR methods. We show that rings in the core flip nearly a thousand times less frequently in crystals than in solution. Enhanced-sampling molecular dynamics simulations, based on a new crystal structure, reproduce these elevated barriers and reveal how the crystal restrains motions. },
  author       = {Becker, Lea Marie and Schanda, Paul},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Data for "Aromatic Ring Flips Reveal Reshaping of Protein Dynamics in Crystals and Complexes"}},
  doi          = {10.15479/AT-ISTA-20641},
  year         = {2025},
}

@article{18705,
  abstract     = {Given a non-singular diagonal cubic hypersurface X⊂Pn−1 over Fq(t) with char(Fq)≠3, we show that the number of rational points of height at most |P| is O(|P|3+ε) for n=6 and O(|P|2+ε) for n=4. In fact, if n=4 and char(Fq)>3 we prove that the number of rational points away from any rational line contained in X is bounded by O(|P|3/2+ε). From the result in 6 variables we deduce weak approximation for diagonal cubic hypersurfaces for n≥7 over Fq(t) when char(Fq)>3 and handle Waring's problem for cubes in 7 variables over Fq(t) when char(Fq)≠3. Our results answer a question of Davenport regarding the number of solutions of bounded height to x31+x32+x33=x34+x35+x36 with xi∈Fq[t].},
  author       = {Glas, Jakob and Hochfilzer, Leonhard},
  issn         = {1432-1807},
  journal      = {Mathematische Annalen},
  pages        = {5485--5533},
  publisher    = {Springer Nature},
  title        = {{On a question of Davenport and diagonal cubic forms over Fq(t)}},
  doi          = {10.1007/s00208-024-03035-z},
  volume       = {391},
  year         = {2025},
}

@article{18820,
  abstract     = {Feature selection is essential in the analysis of molecular systems and many other fields, but several uncertainties remain: What is the optimal number of features for a simplified, interpretable model that retains essential information? How should features with different units be aligned, and how should their relative importance be weighted? Here, we introduce the Differentiable Information Imbalance (DII), an automated method to rank information content between sets of features. Using distances in a ground truth feature space, DII identifies a low-dimensional subset of features that best preserves these relationships. Each feature is scaled by a weight, which is optimized by minimizing the DII through gradient descent. This allows simultaneously performing unit alignment and relative importance scaling, while preserving interpretability. DII can also produce sparse solutions and determine the optimal size of the reduced feature space. We demonstrate the usefulness of this approach on two benchmark molecular problems: (1) identifying collective variables that describe conformations of a biomolecule, and (2) selecting features for training a machine-learning force field. These results show the potential of DII in addressing feature selection challenges and optimizing dimensionality in various applications. The method is available in the Python library DADApy.},
  author       = {Wild, Romina and Wodaczek, Felix and Del Tatto, Vittorio and Cheng, Bingqing and Laio, Alessandro},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{Automatic feature selection and weighting in molecular systems using Differentiable Information Imbalance}},
  doi          = {10.1038/s41467-024-55449-7},
  volume       = {16},
  year         = {2025},
}

@article{20926,
  abstract     = {Most current machine learning interatomic potentials (MLIPs) rely on short-range approximations, without explicit treatment of long-range electrostatics. To address this, we recently developed the Latent Ewald Summation (LES) method, which infers electrostatic interactions, polarization, and Born effective charges (BECs), just by learning from energy and force training data. Here, we present LES as a standalone library, compatible with any short-range MLIP, and demonstrate its integration with methods such as MACE, NequIP, Allegro, CACE, CHGNet, and UMA. We benchmark LES-enhanced models on distinct systems, including bulk water, polar dipeptides, and gold dimer adsorption on defective substrates, and show that LES not only captures correct electrostatics but also improves accuracy. Additionally, we scale LES to large and chemically diverse data by training MACELES-OFF on the SPICE set containing molecules and clusters, making a universal MLIP with electrostatics for organic systems, including biomolecules. MACELES-OFF is more accurate than its short-range counterpart (MACE-OFF) trained on the same data set, predicts dipoles and BECs reliably, and has better descriptions of bulk liquids. By enabling efficient long-range electrostatics without directly training on electrical properties, LES paves the way for electrostatic foundation MLIPs.},
  author       = {Kim, Dongjin and Wang, Xiaoyu and Vargas, Santiago and Zhong, Peichen and King, Daniel S. and Inizan, Theo Jaffrelot and Cheng, Bingqing},
  issn         = {1549-9626},
  journal      = {Journal of Chemical Theory and Computation},
  number       = {24},
  pages        = {12709--12724},
  publisher    = {American Chemical Society},
  title        = {{A universal augmentation framework for long-range electrostatics in machine learning interatomic potentials}},
  doi          = {10.1021/acs.jctc.5c01400},
  volume       = {21},
  year         = {2025},
}

@article{20990,
  abstract     = {Modeling the response of material and chemical systems to electric fields remains a longstanding challenge. Machine learning interatomic potentials (MLIPs) offer an efficient and scalable alternative to quantum mechanical methods, but do not by themselves incorporate electrical response. Here, we show that polarization and Born effective charge (BEC) tensors can be directly extracted from long-range MLIPs within the Latent Ewald Summation (LES) framework, solely by learning from energy and force data. Using this approach, we predict the infrared spectra of bulk water under zero or finite external electric fields, ionic conductivities of high-pressure superionic ice, and the phase transition and hysteresis in ferroelectric PbTiO3 perovskite. This work thus extends the capability of MLIPs to predict electrical response –without training on charges or polarization or BECs– and enables accurate modeling of electric-field-driven processes in diverse systems at scale.},
  author       = {Zhong, Peichen and Kim, Dongjin and King, Daniel S. and Cheng, Bingqing},
  issn         = {2057-3960},
  journal      = {npj Computational Materials},
  publisher    = {Springer Nature},
  title        = {{Machine learning interatomic potential can infer electrical response}},
  doi          = {10.1038/s41524-025-01911-z},
  volume       = {11},
  year         = {2025},
}

@article{20492,
  abstract     = {The glassy thermal conductivities observed in crystalline inorganic perovskites such as Cs3Bi2I6Cl3 are perplexing and lacking theoretical explanations. Here, we first experimentally measure its thermal transport behavior from 20 to 300 K, after synthesizing Cs3Bi2I6Cl3 single crystals. Using path-integral molecular dynamics simulations driven by machine learning potentials, we reveal that Cs3Bi2I6Cl3 has large lattice distortions at low temperatures, which may be related to the large atomic size mismatch. Employing the Wigner formulation of thermal transport, we reproduce theexperimental thermal conductivities based on lattice-distorted structures. This studythus provides a framework for predicting and understanding glassy thermal transportin materials with strong lattice disorder.},
  author       = {Zeng, Zezhu and Fan, Zheyong and Simoncelli, Michele and Chen, Chen and Liang, Ting and Chen, Yue and Thornton, Geoff and Cheng, Bingqing},
  issn         = {1091-6490},
  journal      = {Proceedings of the National Academy of Sciences},
  number       = {41},
  pages        = {e2415664122},
  publisher    = {National Academy of Sciences},
  title        = {{Lattice distortion leads to glassy thermal transport in crystalline Cs3Bi2I6Cl3}},
  doi          = {10.1073/pnas.2415664122},
  volume       = {122},
  year         = {2025},
}

@article{20011,
  abstract     = {Heat transport in glasses over a wide temperature range is critical for applications in gate dielectrics and thermal insulators but remains poorly understood due to the challenges in modeling vibrational anharmonicity and configurational dynamics across the glass transition. Recent predictions show an unusual decrease in thermal conductivity (κ) with temperature in amorphous hafnia (a-HfO2), contrasting with the typical trend in glasses. Using molecular dynamics with a machine-learning-based neuroevolution potential, we compute κ of a-HfO2 from 50 K to 2000 K. At low temperatures, the Wigner transport equation captures both anharmonicity and quantum statistics. Above 1200 K, atomic diffusion invalidates the quasiparticle picture, and we resort to the Green–Kubo method to capture convective transport. We further extend the Wigner transport equation to supercooled a-HfO2, revealing the crucial role of low-frequency modes in facilitating heat transport. The computed κ, based on both Green–Kubo and Wigner transport theories, increases continuously with temperature up to 2000 K.},
  author       = {Zeng, Zezhu and Liang, Xia and Fan, Zheyong and Chen, Yue and Simoncelli, Michele and Cheng, Bingqing},
  issn         = {2639-4979},
  journal      = {ACS Materials Letters},
  pages        = {2695--2701},
  publisher    = {American Chemical Society},
  title        = {{Thermal transport of amorphous hafnia across the glass transition}},
  doi          = {10.1021/acsmaterialslett.5c00263},
  year         = {2025},
}

@article{19495,
  abstract     = {Machine learning interatomic potentials (MLIPs) often neglect long-range interactions, such as electrostatic and dispersion forces. In this work, we introduce a straightforward and efficient method to account for long-range interactions by learning a hidden variable from local atomic descriptors and applying an Ewald summation to this variable. We demonstrate that in systems including charged and polar molecular dimers, bulk water, and water-vapor interface, standard short-ranged MLIPs can lead to unphysical predictions even when employing message passing. The long-range models effectively eliminate these artifacts, with only about twice the computational cost of short-range MLIPs.},
  author       = {Cheng, Bingqing},
  issn         = {2057-3960},
  journal      = {npj Computational Materials},
  publisher    = {Springer Nature},
  title        = {{Latent Ewald summation for machine learning of long-range interactions}},
  doi          = {10.1038/s41524-025-01577-7},
  volume       = {11},
  year         = {2025},
}

@article{20702,
  abstract     = {Qualitative and quantitative orbital properties such as bonding/antibonding character, localization, and orbital energies are critical to how chemists understand reactivity, catalysis, and excited-state behavior. Despite this, representations of orbitals in deep learning models have been very underdeveloped relative to representations of molecular geometries and Hamiltonians. Here, we apply state-of-the-art equivariant deep learning architectures to the task of assigning global labels to orbitals, namely energies characterizations, given the molecular coefficients from Hartree–Fock or density functional theory. The architecture we have developed, the Cartesian Equivariant Orbital Network (CEONET), shows how molecular orbital coefficients are readily featurized as equivariant node features common to all graph-based machine-learned potentials. We find that CEONET performs well at predicting difficult quantitative labels such as the orbital energy and orbital entropy. Furthermore, we find that the CEONET representation provides an intuitive latent space for differentiating orbital character for the qualitative assignment of e.g. bonding or antibonding character. In addition to providing a useful representation for further integrating deep learning with electronic structure theory, we expect CEONET to be useful for automatizing and interpreting the results of advanced electronic structure methods such as complete active space self-consistent field theory. In particular, the ability of CEONET to infer multireference character via the orbital entropy paves the way toward the machine-learned selection of active spaces.},
  author       = {King, Daniel S. and Grzenda, Daniel and Zhu, Ray and Hudson, Nathaniel and Foster, Ian and Cheng, Bingqing and Gagliardi, Laura},
  issn         = {1091-6490},
  journal      = {Proceedings of the National Academy of Sciences},
  number       = {48},
  publisher    = {National Academy of Sciences},
  title        = {{Cartesian equivariant representations for learning and understanding molecular orbitals}},
  doi          = {10.1073/pnas.2510235122},
  volume       = {122},
  year         = {2025},
}

@article{20704,
  abstract     = {Generative models have advanced significantly in sampling material systems with continuous variables, such as atomistic structures. However, their application to discrete variables, like atom types or spin states, remains underexplored. In this work, we introduce a discrete flow matching model, tailored for systems with discrete phase-space coordinates (e.g., the Ising model or a multicomponent system on a lattice). This approach enables a single model to sample free energy surfaces over a wide temperature range with minimal training overhead, and the model generation is scalable to larger lattice sizes than those in the training set. We demonstrate our approach on the 2D Ising model, showing efficient and reliable free energy sampling. These results highlight the potential of flow matching for low-cost, scalable free energy sampling in discrete systems and suggest promising extensions to alchemical degrees of freedom in crystalline materials. The codebase developed for this work is openly available at https://github.com/tuoping/alchemicalFES.},
  author       = {Tuo, Ping and Zeng, Zezhu and Chen, Jiale and Cheng, Bingqing},
  issn         = {1549-9626},
  journal      = {Journal of Chemical Theory and Computation},
  number       = {22},
  pages        = {11427--11435},
  publisher    = {American Chemical Society},
  title        = {{Scalable multitemperature free energy sampling of classical Ising spin states}},
  doi          = {10.1021/acs.jctc.5c01248},
  volume       = {21},
  year         = {2025},
}

@phdthesis{20357,
  author       = {Ruzickova, Natalia},
  isbn         = {978-3-99078-066-4},
  issn         = {2663-337X},
  keywords     = {gene regulation, networks, omnigenic model, pancreas, collective behaviour},
  pages        = {156},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Effect propagation in biological networks}},
  doi          = {10.15479/AT-ISTA-20357},
  year         = {2025},
}

@article{19593,
  abstract     = {Prenatal immune challenges pose significant risks to human embryonic brain and eye development. However, our knowledge about the safe usage of anti-inflammatory drugs during pregnancy is still limited. While human induced pluripotent stem cells (hIPSC)-derived brain organoid models have started to explore functional consequences upon viral stimulation, these models commonly lack microglia, which are susceptible to and promote inflammation. Furthermore, microglia are actively involved in neuronal development. Here, we generate hIPSC-derived microglia precursor cells and assemble them into retinal organoids. Once the outer plexiform layer forms, these hIPSC-derived microglia (iMG) fully integrate into the retinal organoids. Since the ganglion cell survival declines by this time in 3D-retinal organoids, we adapted the model into 2D and identify that the improved ganglion cell number significantly decreases only with iMG presence. In parallel, we applied the immunostimulant POLY(I:C) to mimic a fetal viral infection. While POLY(I:C) exposure alters the iMG phenotype, it does not hinder their interaction with ganglion cells. Furthermore, iMG significantly enhance the supernatant’s inflammatory secretome and increase retinal cell proliferation. Simultaneous exposure with the non-steroidal anti-inflammatory drug (NSAID) ibuprofen dampens POLY(I:C)-mediated changes of the iMG phenotype and ameliorates cell proliferation. Remarkably, while POLY(I:C) disrupts neuronal calcium dynamics independent of iMG, ibuprofen rescues this effect only if iMG are present. Mechanistically, ibuprofen targets the enzymes cyclooxygenase 1 and 2 (COX1/PTGS1 and COX2/PTGS2) simultaneously, from which iMG mainly express COX1. Selective COX1 blockage fails to restore the calcium peak amplitude upon POLY(I:C) stimulation, suggesting ibuprofen’s beneficial effect depends on the presence and interplay of COX1 and COX2. These findings underscore the importance of microglia in the context of prenatal immune challenges and provide insight into the mechanisms by which ibuprofen exerts its protective effects during embryonic development.},
  author       = {Hübschmann, Verena and Korkut, Medina and Venturino, Alessandro and Maya-Arteaga, Juan Pablo and Siegert, Sandra},
  issn         = {1742-2094},
  journal      = {Journal of Neuroinflammation},
  number       = {1},
  publisher    = {Springer Nature},
  title        = {{Microglia determine an immune-challenged environment and facilitate ibuprofen action in human retinal organoids}},
  doi          = {10.1186/s12974-025-03366-x},
  volume       = {22},
  year         = {2025},
}

@phdthesis{20074,
  abstract     = {Prenatal immune challenges pose significant risks to human embryonic brain and eye development. However, we still lack knowledge about the safe usage of anti-inflammatory drugs during pregnancy. Human induced pluripotent stem cell (hIPSC)-derived brain organoid models provide a unique opportunity to investigate neuronal development and have started to explore functional consequences upon viral infection. However, brain organoids usually lack microglia, the brain-resident immune cells. They are present in the early human embryonic brain and actively participate in neuronal circuit development. At the same time, microglia are known for their immune-sensing properties and will influence viral-mediated effects. In my thesis, I was interested to study the multifunctional role of human microglia during retinal development. 
In chapter 1, I characterize the innate occurrence of IBA1+-microglia-like cells within the retinal organoid differentiation (Bartalska et al., 2022). Therefore, we differentiate hIPSC using an unguided retinal organoid differentiation protocol and observe the presence of IBA1+-microglia-like cells alongside retinal cups between week 3 and 4 in 2.5D culture. However, instead of infiltrating the neuroectodermal sides, they enrich within non-pigmented, 3D-cystic compartments that develop in low numbers parallel to 3D-retinal organoids. To enrich for IBA1+-microglia precursors (preMG), we guided the differentiation with a low-dosed BMP4 application, which prevents retinal cup development and enhances microglia and 3D-cysts formation. We characterize the differentiated preMG for their microglia-like identity and validated their functionality. In parallel, mass spectrometry identifies the 3D-cysts to express mesenchymal and epithelial markers. We confirm that comparable 3D-cysts are also the preferential environment for IBA1+-microglia-like cells within the unguided retinal organoid differentiation. 
In chapter 2, I investigate how microglia influence retinal development and whether they contribute to viral-mediated consequences (Schmied et al., 2025). Here, we assemble preMG, which we have characterized in chapter 1, into 3D-retinal organoids. Once the outer plexiform layer forms, microglia-like cells (iMG) populate them and interact with retinal cell types. However, at this developmental stage, the ganglion cell number decreases in 3D-retinal organoids. Thus, we adapted the model into 2D which promotes their survival. Integrated iMG engulf ganglion cells and control their cell number. In parallel, we apply the immunostimulant POLY(I:C) to mimic a fetal viral infection. Although POLY(I:C) stimulation affects iMG phenotype, it does not influence their interaction with ganglion cells. Furthermore, iMG presence significantly contributes to the supernatant’s inflammatory secretome and increases retinal cell proliferation. Simultaneous exposure to the non-steroidal anti-inflammatory drug (NSAID) ibuprofen dampens POLY(I:C)-mediated consequences of the iMG phenotype and ameliorates cell proliferation. Remarkably, while POLY(I:C) disrupts neuronal calcium dynamics independent of iMG presence, ibuprofen rescues this effect only in the presence of iMG. Mechanistically, ibuprofen blocks the enzymes cyclooxygenase 1 and 2 (COX1/ PTGS1 and COX2/ PTGS2) simultaneously, from which iMG predominantly express COX1. Selective inhibition of COX1 does not restore the calcium peak amplitude upon POLY(I:C) stimulation, indicating ibuprofen’s effect depends on the presence and interplay of both, COX1 and COX2. 
In summary, we characterized the 3D-retinal organoid model for the occurrence of IBA1+-microglia like cells. As the innately developing IBA1+-cells enrich in mesenchymal over retinal structures, we optimized a protocol to differentiate IBA1+-microglia precursors. By combining these two models we generate microglia-assembled retinal organoids. Our results underscore the importance of microglia during neurodevelopment, in the context of prenatal immune challenges and provide insight into the mechanisms by which ibuprofen exerts its protective effects during embryonic development.},
  author       = {Hübschmann, Verena},
  isbn         = {978-3-99078-060-2},
  issn         = {2663-337X},
  pages        = {151},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Human microglia impact neuronal development in retinal organoids}},
  doi          = {10.15479/AT-ISTA-20074},
  year         = {2025},
}

@article{19372,
  abstract     = {We consider the confined Fröhlich polaron and establish an asymptotic series for the low-energy eigenvalues in negative powers of the coupling constant. The coefficients of the series are derived through a two-fold perturbation approach, involving expansions around the electron Pekar minimizer and the excitations of the quantum field.},
  author       = {Brooks, Morris and Mitrouskas, David Johannes},
  issn         = {2690-1005},
  journal      = {Probability and Mathematical Physics},
  number       = {1},
  pages        = {281--325},
  publisher    = {Mathematical Sciences Publishers},
  title        = {{Asymptotic series for low-energy excitations of the Fröhlich polaron at strong coupling}},
  doi          = {10.2140/pmp.2025.6.281},
  volume       = {6},
  year         = {2025},
}

@article{20342,
  abstract     = {Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In the quantitative setting, properties are arbitrary functions from infinite words to partially-ordered domains. Extending this paradigm to the quantitative domain, where properties are arbitrary functions mapping infinite words to partially-ordered domains, we introduce and study the notions of quantitative safety and liveness. First, we formally define quantitative safety and liveness, and prove that our definitions induce conservative quantitative generalizations of both the safety-progress hierarchy and the safety-liveness decomposition of boolean properties. Consequently, like their boolean counterparts, quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. We further establish a connection between quantitative safety and topological continuity and provide alternative characterizations of quantitative safety and liveness in terms of their boolean analogs. Second, we instantiate our framework with the specific classes of quantitative properties expressed by automata. These quantitative automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totally-ordered domain of real numbers. For all common value functions, we provide a procedure for deciding whether a given automaton is safe or live, we show how to construct its safety closure, and we present a min-decomposition into safe and live automata.},
  author       = {Boker, Udi and Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E},
  issn         = {1860-5974},
  journal      = {Logical Methods in Computer Science},
  number       = {2},
  publisher    = {EPI Sciences},
  title        = {{Safety and liveness of quantitative properties and automata}},
  doi          = {10.46298/lmcs-21(2:2)2025},
  volume       = {21},
  year         = {2025},
}

@phdthesis{20147,
  abstract     = {Quantitative properties offer a framework for specifying and verifying system behaviors beyond the traditional boolean perspective. For example, while a boolean property may specify whether a server eventually grants every request it receives, a quantitative one may map each server execution to its average response time. This quantitative view is relatively well-studied in the context of static verification. However, although such properties often appear in practice as performance or robustness measures in a dynamic verification context, a general theoretical framework for their analysis and classification from a monitoring perspective is still missing.

In this thesis, we aim to develop such a framework that takes resource-precision tradeoffs of monitors as a central consideration. We present the first theory of monitorability for quantitative properties where monitors can be naturally approximate and compared regarding their precision and resource use. In particular, we show that additional monitor resources such as registers or states lead to strictly better approximations for some properties. To enable such analyses in a machine-model independent way, we describe an abstract notion of monitors that can be instantiated with concrete models of monitors. Within this framework, we study how abstract monitors behave and identify classes of properties amenable to approximate monitoring with resource-precision considerations. We then extend the boolean safety-liveness dichotomy and safety-progress hierarchy to the quantitative setting with a monitoring perspective. In particular, we prove that every property is the pointwise minimum of a safety property and a liveness property, and properties that are both safe and co-safe can be approximately monitored arbitrarily precisely using only finitely many states. We also study the classes of quantitative properties definable by finite-state quantitative automata and provide algorithms for deciding their safety or liveness as well as their safety-liveness decompositions. Finally, we present the first general-purpose tool for automating the analysis, verification, and monitoring of quantitative automata.


},
  author       = {Sarac, Naci E},
  issn         = {2663-337X},
  pages        = {149},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{A monitoring-oriented theory and classification of quantitative specifications}},
  doi          = {10.15479/AT-ISTA-20147},
  year         = {2025},
}

@article{19701,
  abstract     = {Living systems are characterized by controlled flows of matter, energy, and information. While the biophysics community has productively engaged with the first two, addressing information flows has been more challenging, with some scattered success in evolutionary theory and a more coherent track record in neuroscience. Nevertheless, interdisciplinary work of the past two decades at the interface of biophysics, quantitative biology, and engineering has led to an emerging mathematical language for describing information flows at the molecular scale. This is where the central processes of life unfold: from detection and transduction of environmental signals to the readout or copying of genetic information and the triggering of adaptive cellular responses. Such processes are coordinated by complex biochemical reaction networks that operate at room temperature, are out of equilibrium, and use low copy numbers of diverse molecular species with limited interaction specificity. Here we review how flows of information through biochemical networks can be formalized using information-theoretic quantities, quantified from data, and computed within various modeling frameworks. Optimization of information flows is presented as a candidate design principle that navigates the relevant time, energy, crosstalk, and metabolic constraints to predict reliable cellular signaling and gene regulation architectures built of individually noisy components.},
  author       = {Tkačik, Gašper and Wolde, Pieter Rein Ten},
  issn         = {1936-1238},
  journal      = {Annual Review of Biophysics},
  pages        = {249--274},
  publisher    = {Annual Reviews},
  title        = {{Information processing in biochemical networks}},
  doi          = {10.1146/annurev-biophys-060524-102720},
  volume       = {54},
  year         = {2025},
}