Search

We study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning tree and keeps communication continuous on the tree. We make the reconfiguration explicit in the language allowing both a centralized automaton as well as the distributed processes to share relevant information about the current communication configuration. We show that Zielonka's seminal result regarding distribution of regular languages for asynchronous automata can be generalized in this setting, incorporating both reconfiguration and more than binary tree architectures.

Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state.

Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to single moves in the original (obliging) game. Here, we propose a novel, large-step view on obliging games, reducing them to standard games in which single moves encode long-term behaviors in the original game. This not only allows us to give a meaningful definition of the environment winning in obliging games, but also leads to significantly improved bounds on both strategy sizes and the solution runtime for obliging games., Comment: extended version of paper accepted for publication at CONCUR 2024

In the present paper, a fluid-particle coupling method is directly derived from the Navier-Stokes equations (NSE) by applying the concept of volume-filtering, yielding a physically consistent methodology to incorporate solid wall boundary conditions in the volume-filtered flow solution, thereby allowing to solve the governing flow equations on non-body conforming meshes. The resulting methodology possesses similarities with a continuous forcing immersed boundary method (IBM) and is, therefore, termed physically consistent IBM (PC-IBM). Based on the recent findings of arXiv:2402.05842v1, the closures arising in the volume-filtered NSE are closed by suitable models or even expressed analytically. The PC-IBM is fully compatible with the large eddy simulation framework, as the volume-filtered NSE converge to the filtered NSE away from solid boundaries. The potential of the PC-IBM is demonstrated by means of different particle-laden flow applications, including a dense packing of fixed particles and periodic settling of 500 particles. The new methodology turns out to be capable of accurately predicting the fluid forces on particles with relatively coarse mesh resolutions. For the flow around isolated spheres, a spatial resolution of six fluid mesh cells per diameter is sufficient to predict the drag force with less than 10% deviation from highly resolved simulation for the investigated particle Reynolds numbers ranging from 10 to 250.

We propose a formalism to capture the structure of the equivariant bordism rings of smooth manifolds with commuting involutions. We introduce the concept of an oriented el$_2^{RO}$-algebra, an algebraic structure featuring representation graded rings for all elementary abelian 2-groups, connected by restriction homomorphisms, a pre-Euler class, and an inverse Thom class; this data is subject to one exactness property. Besides equivariant bordism, oriented global ring spectra also give rise to oriented el$_2^{RO}$-algebras, so examples abound. Inverting the inverse Thom classes yields a global 2-torsion group law. In this sense, our oriented el$_2^{RO}$-algebras are delocalized generalizations of global 2-torsion group laws. Our main result shows that equivariant bordism for elementary abelian 2-groups is an initial oriented el$_2^{RO}$-algebra. Several other interesting equivariant homology theories can also be characterized, on elementary abelian 2-groups, by similar universal properties. We prove that stable equivariant bordism is an initial el$_2^{RO}$-algebra with an invertible orientation; that Bredon homology with constant mod 2 coefficients is an initial el$_2^{RO}$-algebra with an additive orientation; and that Borel equivariant homology with mod 2 coefficients is an initial el$_2^{RO}$-algebra with an orientation that is both additive and invertible.

We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earlier convergence. We also present an economic later-appearence-record construction that takes Emerson-Lei games to parity games, and show that it preserves DAG sub-structures; it follows that the proposed method can be used also for the accelerated solution of Emerson-Lei games.

We calculate the representation-graded Bredon homology rings of all elementary abelian 2-groups with coefficients in the constant mod-2 Mackey functor. We show that these rings are domains, and we exhibit minimal presentations as quotients of the polynomial algebra on the pre-Euler and inverse Thom classes of all nontrivial characters, subject to an explicit finite list of relations arising from orientability properties. Two corollaries of our presentation are the calculation, originally due to Holler and Kriz, of the geometric fixed point rings, and a strengthening of a calculation of Balmer and Gallauer of the localized twisted cohomology ring.

The volume-filtering of the Navier-Stokes equations allows to consider the effect that particles have on the fluid without further assumptions, but closures arise of which the implications are not fully understood. In the present paper, we carefully study every closure in the volume-filtered fluid momentum equation and investigate their impact on the momentum and energy transfer dependent on the filtering characteristics. We provide an analytical expression for the viscous closure that arises because filter and spatial derivative in the viscous term do not commute. An analytical expression for the regularization of the particle momentum source of a single sphere in the Stokes regime is derived. Furthermore, we propose a model for the subfilter stress tensor, which originates from filtering the advective term. The model for the subfilter stress tensor is shown to agree well with the subfilter stress tensor for small filter widths relative to the size of the particle. We show that the subfilter stress tensor requires modeling and should not be neglected. For small filter widths, we find that the commonly applied Gaussian regularization of the particle momentum source is a poor approximation of the spatial distribution of the particle momentum source, but for larger filter widths the spatial distribution approaches a Gaussian. Furthermore, we propose a modified advective term in the volume-filtered momentum equation that consistently circumvents the common stability issues observed at locally small fluid volume fractions and identify inconsistencies in previous studies of the phase-averaged kinetic energy of the volume-filtered fluid velocity. Finally, we propose a generally applicable form of the volume-filtered momentum equation and its closures based on clear and well-founded assumptions and propose guidelines for point-particle simulations based on the new findings.

The 2nd generation VLTI instrument GRAVITY is a two-field infrared interferometer operating in the K band between 1.97 and 2.43 $\mu$m with either the four 8 m or the four 1.8 m telescopes of the Very Large Telescope (VLT). Beams collected by the telescopes are corrected with adaptive optics systems and the fringes are stabilized with a fringe-tracking system. A metrology system allows the measurement of internal path lengths in order to achieve high-accuracy astrometry. High sensitivity and high interferometric accuracy are achieved thanks to (i) correction of the turbulent phase, (ii) the use of low-noise detectors, and (iii) the optimization of photometric and coherence throughput. Beam combination and most of the beam transport are performed with single-mode waveguides in vacuum and at low temperature. In this paper, we present the functions and performance achieved with weakly birefringent standard single-mode fiber systems in GRAVITY. Fibered differential delay lines (FDDLs) are used to dynamically compensate for up to 6 mm of delay between the science and reference targets. Fibered polarization rotators allow us to align polarizations in the instrument and make the single-mode beam combiner close to polarization neutral. The single-mode fiber system exhibits very low birefringence (less than 23{\deg}), very low attenuation (3.6-7 dB/km across the K band), and optimized differential dispersion (less than 2.04 $\mu$rad cm2 at zero extension of the FDDLs). As a consequence, the typical fringe contrast losses due to the single-mode fibers are 6% to 10% in the lowest-resolution mode and 5% in the medium- and high-resolution modes of the instrument for a photometric throughput of the fiber chain of the order of 90%. There is no equivalent of this fiber system to route and modally filter beams with delay and polarization control in any other K-band beamcombiner., Comment: 14 pages including 2 appendices, 8 figures in the main text plus 2 figures in the appendices, final version published in A&A

This paper reviews the new highly interdisciplinary research field studying the behavior of condensed matter systems exposed to radiation. The paper highlights several relevant examples of recent advances in the field and provides a roadmap for the development of the field in the next decade. Condensed matter systems exposed to radiation may have very different natures, being inorganic, organic or biological, finite or infinite, be composed of many different molecular species or materials, existing in different phases (solid, liquid, gaseous or plasma) and operating under different thermodynamic conditions. The essential and novel element of this research is that, despite the vast diversity of such systems, many of the key phenomena related to the behavior of irradiated systems (such as radiation-induced damage, mechanisms of damage repair and control, radiation protection, etc.) are very similar and can be understood based on the same fundamental theoretical principles and computational approaches. One of the essential features of the aforementioned phenomena concerns their multiscale nature as the manifestation of the radiation-induced effects occurring at different spatial and temporal scales ranging from the atomic to the macroscopic. The multiscale nature of the effects and similarity of their manifestation in systems of different origins necessarily brings together different disciplines, such as physics, chemistry, biology, materials and nano-science, and biomedical research, demonstrating numerous interlinks and commonalities between them. This research field is highly relevant to many novel and emerging technologies and medical applications., Comment: Roadmap paper; 376 pages, 32 figures. Submitted to Chemical Reviews

We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (nondeterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal $\mu$-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the $\mu$-calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets., Comment: Full Version of VMCAI 2024 publication

We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip such games with two $\omega$-regular winning conditions $\alpha$ and $\beta$ deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called "fair $\alpha/\beta$ games". We formalize fair $\alpha/\beta$ games and show that they are determined. For fair parity/parity games, i.e., fair $\alpha/\beta$ games where $\alpha$ and $\beta$ are given each by a parity condition over $G$, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games where only one player is restricted by fair moves.

This implementation guidance focuses on carbon removal and sequestration via wood harvesting and storage (WHS), a process where woody biomass, with the embedded carbon, is stored for long timescales in shallow geologic storage. The engineering structure designed to ensure such durable storage by preventing biomass decomposition is called a Wood Vault. This guidance contains the requirements for a basic Wood Vault project, and is intended to aid project developers, verifiers, and registries in this space. It describes a set of requirements that govern the end-to-end process of carbon removal and sequestration. This includes carbon accounting, wood sourcing via wood residual (WR) utilization, Wood Vault construction and maintenance, as well as processes for monitoring, verification, and credit issuance. Carbon accounting requirements include baseline, or counterfactual specification, and full life cycle analysis (LCA) within a specified process boundary. For the vault itself, the guidance describes a buried vault with the burial chamber covered by a layer of low permeability material to create anoxic condition. Other types of vaults can also be used to adjust to local environmental, transport, and economic constraints. Monitoring and verification requirements include in-situ sensors, gas sampling, sample excavations, and site maintenance. This guidance also contemplates land ownership and legal assurances, as well as environmental and societal impact assessments. The implementation guidance concludes with recommendations regarding auditing, certification and carbon credit issuance.

Let $A$ be an abelian compact Lie group. In this paper we compute the spectrum of invariant prime ideals of the $A$-equivariant Lazard ring, or equivalently the spectrum of points of the moduli stack of $A$-equivariant formal groups. We further show that this spectrum is homeomorphic to the Balmer spectrum of compact $A$-spectra, with the comparison map induced by equivariant complex bordism homology., Comment: 43 pages, comments welcome

The Page-Wootters formalism is a proposal for reconciling the background-dependent, quantum-mechanical notion of time with the background-independence of general relativity. However, the physical meaning of this framework remains debated. In this work, we compare two consistent approaches to the Page-Wootters formalism to clarify the operational meaning of evolution and measurements with respect to a quantum temporal reference frame. The so-called "twirled observable" approach implements measurements as operators that are invariant with respect to the Hamiltonian constraint. The "purified measurement" approach instead models measurements dynamically by modifying the constraint itself. While both approaches agree in the limit of ideal clocks, a natural generalization of the purified measurement approach to the case of non-ideal, finite-resource clocks yields a radically different picture. We discuss the physical origin of this discrepancy and argue that the approaches describe operationally distinct situations. Moreover, we show that, for non-ideal clocks, the purified measurement approach yields time non-local, non-unitary evolution and implies a fundamental limitation to the operational definition of the temporal order of events. Nevertheless, unitarity and definite temporal order can be restored if we assume that time is discrete.

There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded $\mu$-calculus and the alternating-time $\mu$-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded $\mu$-calculus., Comment: Final version (corrected slight mistake in Rabin-type formula series)

We propose a novel model to obtain the subgrid-scale velocity in the context of large-eddy simulation (LES) of particle-laden turbulent flows, to recover accurate particle statistics. In the new wavelet enrichment model, the subgrid-scale velocity is discretized with a divergence-free wavelet vector basis, and the coefficients of the expansion are obtained by minimizing the squared error of the linearized subfilter Navier-Stokes equations (SFNSE). The compact support of the wavelet basis is exploited to achieve continuously varying subgrid-scale velocity statistics across the domain. The performance of the new wavelet enrichment model is evaluated in single-phase and particle-laden flow simulations, comparing the results with the results of direct numerical simulations (DNS). The simulations show that the model can generate inhomogeneous and anisotropic velocity statistics, accurate strain-rotation relations, and a good approximation of the kinetic energy spectrum of the corresponding DNS. Furthermore, the model significantly improves the prediction of the particle-pair dispersion, the clustering of the particles, and the turbulence modulation by particles in two-way coupled simulations. The proposed model recovers the most important interactions between fluid turbulence and the behavior of the particles, while maintaining the computational cost on the order of a LES.

Emerson-Lei conditions have recently attracted attention due to their succinctness and compositionality properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition gives rise naturally to a new reduction to parity games. This reduction, however, does not result in optimal analysis. Second, we show based on the first reduction (and the Zielonka tree) how to provide a direct fixpoint-based characterization of the winning region. The fixpoint-based characterization allows for symbolic analysis. It generalizes the solutions of games with known winning conditions such as B\"uchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known symbolic algorithms and complexity results. We also show how the capabilities of the proposed algorithm can be exploited in reactive synthesis, suggesting a new expressive fragment of LTL that can be handled symbolically. Our fragment combines a safety specification and a liveness part. The safety part is unrestricted and the liveness part allows to define Emerson-Lei conditions on occurrences of letters. The symbolic treatment is enabled due to the simplicity of determinization in the case of safety languages and by using our new algorithm for game solving. This approach maximizes the number of steps solved symbolically in order to maximize the potential for efficient symbolic implementations.