Showing 1–50 of 117 results for author: Schröder, L

Efficient Model Checking for the Alternating-Time μ-Calculus via Effectivity Frames

Authors: Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder

Abstract: The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time μ-calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in princi… ▽ More The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time μ-calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in principle allows for faster evaluation of coalitional modalities. In the present work, we investigate whether implementing a model checker based on effectivity frames leads to better performance in practice. We implement the translation from concurrent game frames to effectivity frames and analyse performance gains in model checking based on corresponding instantiations of a generic model checker for coalgebraic μ-calculi, using dedicated benchmark series as well as random systems and formulas. In the process, we also compare performance to the state-of-the-art ATL model checkerMCMAS. Our results indicate that on large systems, the overhead involved in converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking. △ Less

Submitted 1 June, 2025; originally announced June 2025.

Non-expansive Fuzzy ALC

Authors: Stefan Gebhart, Lutz Schröder, Paul Wild

Abstract: Fuzzy description logics serve the representation of vague knowledge, typically letting concepts take truth degrees in the unit interval. Expressiveness, logical properties, and complexity vary strongly with the choice of propositional base. The Lukasiewicz propositional base is generally perceived to have preferable logical properties but often entails high complexity or even undecidability. Cont… ▽ More Fuzzy description logics serve the representation of vague knowledge, typically letting concepts take truth degrees in the unit interval. Expressiveness, logical properties, and complexity vary strongly with the choice of propositional base. The Lukasiewicz propositional base is generally perceived to have preferable logical properties but often entails high complexity or even undecidability. Contrastingly, the less expressive Zadeh propositional base comes with low complexity but entails essentially no change in logical behaviour compared to the classical case. To strike a balance between these poles, we propose non-expansive fuzzy ALC, in which the Zadeh base is extended with Lukasiewicz connectives where one side is restricted to be a rational constant, that is, with constant shift operators. This allows, for instance, modelling dampened inheritance of properties along roles. We present an unlabelled tableau method for non-expansive fuzzy ALC, which allows reasoning over general TBoxes in EXPTIME like in two-valued ALC. △ Less

Submitted 21 May, 2025; v1 submitted 14 May, 2025; originally announced May 2025.

Temperature anisotropy instabilities of solar wind electrons with regularized Kappa-halos resolved with ALPS

Authors: Dustin L. Schröder, Horst Fichtner, Marian Lazar, Daniel Verscharen, Kristopher G. Klein

Abstract: Space plasmas in various astrophysical setups can often be both very hot and dilute, making them highly susceptible to waves and fluctuations, which are generally self-generated and maintained by kinetic instabilities. In this sense, we have in-situ observational evidence from the solar wind and planetary environments, which reveal not only wave fluctuations at kinetic scales of electrons and prot… ▽ More Space plasmas in various astrophysical setups can often be both very hot and dilute, making them highly susceptible to waves and fluctuations, which are generally self-generated and maintained by kinetic instabilities. In this sense, we have in-situ observational evidence from the solar wind and planetary environments, which reveal not only wave fluctuations at kinetic scales of electrons and protons, but also non-equilibrium distributions of particle velocities. This paper reports on the progress made in achieving a consistent modeling of the instabilities generated by temperature anisotropy, taking concrete example of those induced by anisotropic electrons, such as, electromagnetic electron-cyclotron (whistler) and firehose instabilities. The effects of the two main electron populations, the quasi-thermal core and the suprathermal halo indicated by the observations, are thus captured. The low-energy core is bi-Maxwellian, and the halo is described for the first time by a regularized (bi-)$κ$-distribution (RKD), which was recently introduced to fix inconsistencies of standard $κ$-distributions (SKD). In the absence of a analytical RKD dispersion kinetic formalism (involving tedious and laborious derivations), both the dispersion and (in)stability properties are directly solved numerically using the numerical Arbitrary Linear Plasma Solver (ALPS). The results have an increased degree of confidence, considering the successful testing of the ALPS on previous results with established distributions. △ Less

Submitted 22 April, 2025; originally announced April 2025.

Comments: 13 pages, 9 figures, 3 tables

Journal ref: Physics of Plasmas 32, 032109 (2025)

Bialgebraic Reasoning on Stateful Languages

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilit… ▽ More Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin's powerful theory of mathematical operational semantics (a.k.a. abstract GSOS) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to apply abstract GSOS to stateful languages have thus failed. We propose a novel approach to the operational semantics of stateful languages based on the formal distinction between readers (terms that expect an initial input store before being executed), and writers (running terms that have already been provided with a store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques. We demonstrate that our approach generates non-trivial compositionality results for stateful languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence. △ Less

Submitted 13 March, 2025; originally announced March 2025.

Disk draining in LIGO progenitor black hole binaries and its significance to electromagnetic counterparts

Authors: Xiaoshan Huang, Sierra Dodd, Sophie Lund Schrøder, Shane W. Davis, Enrico Ramirez-Ruiz

Abstract: The effect of tidal forces on transport within a relic accretion disk in binary black holes is studied here with a suite of two-dimensional hydrodynamic simulations. As the binary contracts due to the emission of gravitational waves, the accretion disk is truncated, and a two-armed spiral wave is excited, which remains stationary in the rotating reference frame of the coalescing binary. Such spira… ▽ More The effect of tidal forces on transport within a relic accretion disk in binary black holes is studied here with a suite of two-dimensional hydrodynamic simulations. As the binary contracts due to the emission of gravitational waves, the accretion disk is truncated, and a two-armed spiral wave is excited, which remains stationary in the rotating reference frame of the coalescing binary. Such spiral waves lead to increased transport of mass and angular momentum. Our findings suggest that even in the case of weakly ionized accretion disks, spiral density waves will drain the disk long before the orbit of the two black holes decays enough for them to merge, thus dimming prospects for a detectable electromagnetic counterpart. △ Less

Submitted 1 March, 2025; originally announced March 2025.

Comments: 12 pages, 6 figures, accepted for ApJL

Stationary distribution of node2vec random walks on household models

Authors: Lars Schroeder, Clara Stegehuis

Abstract: The node2vec random walk has proven to be a key tool in network embedding algorithms. These random walks are tuneable, and their transition probabilities depend on the previous visited node and on the triangles containing the current and the previously visited node. Even though these walks are widely used in practice, most mathematical properties of node2vec walks are largely unexplored, including… ▽ More The node2vec random walk has proven to be a key tool in network embedding algorithms. These random walks are tuneable, and their transition probabilities depend on the previous visited node and on the triangles containing the current and the previously visited node. Even though these walks are widely used in practice, most mathematical properties of node2vec walks are largely unexplored, including their stationary distribution. We study the node2vec random walk on community-structured household model graphs. We prove an explicit description of the stationary distribution of node2vec walks in terms of the walk parameters. We then show that by tuning the walk parameters, the stationary distribution can interpolate between uniform, size-biased, or the simple random walk stationary distributions, demonstrating the wide range of possible walks. We further explore these effects on some specific graph settings. △ Less

Submitted 13 June, 2025; v1 submitted 26 February, 2025; originally announced February 2025.

Comments: 23 pages, 8 figures

The Danger of Overthinking: Examining the Reasoning-Action Dilemma in Agentic Tasks

Authors: Alejandro Cuadron, Dacheng Li, Wenjie Ma, Xingyao Wang, Yichuan Wang, Siyuan Zhuang, Shu Liu, Luis Gaspar Schroeder, Tian Xia, Huanzhi Mao, Nicholas Thumiger, Aditya Desai, Ion Stoica, Ana Klimovic, Graham Neubig, Joseph E. Gonzalez

Abstract: Large Reasoning Models (LRMs) represent a breakthrough in AI problem-solving capabilities, but their effectiveness in interactive environments can be limited. This paper introduces and analyzes overthinking in LRMs. A phenomenon where models favor extended internal reasoning chains over environmental interaction. Through experiments on software engineering tasks using SWE Bench Verified, we observ… ▽ More Large Reasoning Models (LRMs) represent a breakthrough in AI problem-solving capabilities, but their effectiveness in interactive environments can be limited. This paper introduces and analyzes overthinking in LRMs. A phenomenon where models favor extended internal reasoning chains over environmental interaction. Through experiments on software engineering tasks using SWE Bench Verified, we observe three recurring patterns: Analysis Paralysis, Rogue Actions, and Premature Disengagement. We propose a framework to study these behaviors, which correlates with human expert assessments, and analyze 4018 trajectories. We observe that higher overthinking scores correlate with decreased performance, with reasoning models exhibiting stronger tendencies toward overthinking compared to non-reasoning models. Our analysis reveals that simple efforts to mitigate overthinking in agentic environments, such as selecting the solution with the lower overthinking score, can improve model performance by almost 30% while reducing computational costs by 43%. These results suggest that mitigating overthinking has strong practical implications. We suggest that by leveraging native function-calling capabilities and selective reinforcement learning overthinking tendencies could be mitigated. We also open-source our evaluation framework and dataset to facilitate research in this direction at https://github.com/AlexCuadron/Overthinking. △ Less

Submitted 12 February, 2025; originally announced February 2025.

vCache: Verified Semantic Prompt Caching

Authors: Luis Gaspar Schroeder, Aditya Desai, Alejandro Cuadron, Kyle Chu, Shu Liu, Mark Zhao, Stephan Krusche, Alfons Kemper, Matei Zaharia, Joseph E. Gonzalez

Abstract: Semantic caches return cached LLM-generated responses for semantically similar prompts to reduce inference latency and cost. They embed cached prompts and store them alongside their response in a vector database. Embedding similarity metrics assign a numerical score to quantify the similarity between a request and its nearest neighbor prompt from the cache. Existing systems use the same static sim… ▽ More Semantic caches return cached LLM-generated responses for semantically similar prompts to reduce inference latency and cost. They embed cached prompts and store them alongside their response in a vector database. Embedding similarity metrics assign a numerical score to quantify the similarity between a request and its nearest neighbor prompt from the cache. Existing systems use the same static similarity threshold across all requests to determine whether two prompts can share similar responses. However, we observe that static thresholds do not give formal correctness guarantees, can result in unexpected error rates, and lead to suboptimal cache hit rates. This paper proposes vCache, the first verified semantic cache with user-defined error rate guarantees. It employs an online learning algorithm to estimate an optimal threshold for each cached prompt, enabling reliable cache responses without additional training. Our experiments show that vCache consistently meets the specified error bounds while outperforming state-of-the-art static-threshold and fine-tuned embedding baselines. We release the vCache implementation and benchmarks to support future research. △ Less

Submitted 27 May, 2025; v1 submitted 5 February, 2025; originally announced February 2025.

Relators and Notions of Simulation Revisited

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted, neighbourhood-based, and game-based systems. Universal coalgebra abstracts system types in this sense as set functors. Notions of (bi)simulation then arise by extendi… ▽ More Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted, neighbourhood-based, and game-based systems. Universal coalgebra abstracts system types in this sense as set functors. Notions of (bi)simulation then arise by extending the functor to act on relations in a suitable manner, turning it into what may be termed a relator. We contribute to the study of relators in the broadest possible sense, in particular in relation to their induced notions of (bi)similarity. Specifically, (i) we show that every functor that preserves a very restricted type of pullbacks (termed 1/4-iso pullbacks) admits a sound and complete notion of bisimulation induced by the coBarr relator; (ii) we establish equivalences between properties of relators and closure properties of the induced notion of (bi)simulation, showing in particular that the full set of expected closure properties requires the relator to be a lax extension, and that soundness of (bi)simulations requires preservation of diagonals; and (iii) we show that functors preserving inverse images admit a greatest lax extension. In a concluding case study, we apply (iii) to obtain a novel highly permissive notion of twisted bisimulation on labelled transition systems. △ Less

Submitted 21 May, 2025; v1 submitted 3 February, 2025; originally announced February 2025.

Behavioural Conformances based on Lax Couplings

Authors: Paul Wild, Lutz Schröder

Abstract: Behavioural conformances -- e.g. behavioural equivalences, distances, preorders -- on a wide range of system types (non-deterministic, probabilistic, weighted etc.) can be dealt with uniformly in the paradigm of universal coalgebra. One of the most commonly used constructions for defining behavioural distances on coalgebras arises as a generalization of the well-known Wasserstein metric. In this c… ▽ More Behavioural conformances -- e.g. behavioural equivalences, distances, preorders -- on a wide range of system types (non-deterministic, probabilistic, weighted etc.) can be dealt with uniformly in the paradigm of universal coalgebra. One of the most commonly used constructions for defining behavioural distances on coalgebras arises as a generalization of the well-known Wasserstein metric. In this construction, couplings of probability distributions are replaced with couplings of more general objects, depending on the functor describing the system type. In many cases, however, the set of couplings of two functor elements is empty, which causes such elements to have infinite distance even in situations where this is not desirable. We propose an approach to defining behavioural distances and preorders based on a more liberal notion of coupling where the coupled elements are matched laxly rather than on-the-nose. We thereby substantially broaden the range of behavioural conformances expressible in terms of couplings, covering, e.g., refinement of modal transition systems and behavioural distance on metric labelled Markov chains. △ Less

Submitted 31 January, 2025; originally announced February 2025.

MSC Class: 68Q85; 03B70 ACM Class: F.4.1

Large Language Models with Human-In-The-Loop Validation for Systematic Review Data Extraction

Authors: Noah L. Schroeder, Chris Davis Jaldi, Shan Zhang

Abstract: Systematic reviews are time-consuming endeavors. Historically speaking, knowledgeable humans have had to screen and extract data from studies before it can be analyzed. However, large language models (LLMs) hold promise to greatly accelerate this process. After a pilot study which showed great promise, we investigated the use of freely available LLMs for extracting data for systematic reviews. Usi… ▽ More Systematic reviews are time-consuming endeavors. Historically speaking, knowledgeable humans have had to screen and extract data from studies before it can be analyzed. However, large language models (LLMs) hold promise to greatly accelerate this process. After a pilot study which showed great promise, we investigated the use of freely available LLMs for extracting data for systematic reviews. Using three different LLMs, we extracted 24 types of data, 9 explicitly stated variables and 15 derived categorical variables, from 112 studies that were included in a published scoping review. Overall we found that Gemini 1.5 Flash, Gemini 1.5 Pro, and Mistral Large 2 performed reasonably well, with 71.17%, 72.14%, and 62.43% of data extracted being consistent with human coding, respectively. While promising, these results highlight the dire need for a human-in-the-loop (HIL) process for AI-assisted data extraction. As a result, we present a free, open-source program we developed (AIDE) to facilitate user-friendly, HIL data extraction with LLMs. △ Less

Submitted 20 January, 2025; originally announced January 2025.

Rendezfood: A Design Case Study of a Conversational Location-based Approach in Restaurants

Authors: Philip Weber, Kevin Krings, Lukas Schröder, Lea Katharina Michel, Thomas Ludwig

Abstract: The restaurant industry is currently facing a challenging socio-economic situation caused by the rise of delivery services, inflation, and typically low margins. Often, technological opportunities for process optimization or customer retention are not fully utilized. In our design case study, we investigate which technologies are already being used to improve the customer experience in restaurants… ▽ More The restaurant industry is currently facing a challenging socio-economic situation caused by the rise of delivery services, inflation, and typically low margins. Often, technological opportunities for process optimization or customer retention are not fully utilized. In our design case study, we investigate which technologies are already being used to improve the customer experience in restaurants and explore a novel new approach to this issue. We designed, implemented, and evaluated a platform with customers and restaurateurs to increase visibility and emotional connection to nearby restaurants through their dishes. Some of our key findings include the enormous potential of combining location-based systems and conversational agents, but also the difficulties in creating content for such platforms. We contribute to the field of Human-Food Interaction by (1) identifying promising design spaces as well as customer and restaurateur requirements for technology in this domain, (2) presenting an innovative design case study to improve the user experience, and (3) exploring the broader implications of our design case study findings for approaching a real-world metaverse. △ Less

Submitted 7 January, 2025; originally announced January 2025.

Comments: 32 pages, 8 figures

ACM Class: J.4

Conformance Games for Graded Semantics

Authors: Jonas Forster, Lutz Schröder, Paul Wild

Abstract: Game-theoretic characterizations of process equivalences traditionally form a central topic in concurrency; for example, most equivalences on the classical linear-time / branching-time spectrum come with such characterizations. Recent work on so-called graded semantics has led to a generic behavioural equivalence game that covers the mentioned games on the linear-time~/ branching-time spectrum and… ▽ More Game-theoretic characterizations of process equivalences traditionally form a central topic in concurrency; for example, most equivalences on the classical linear-time / branching-time spectrum come with such characterizations. Recent work on so-called graded semantics has led to a generic behavioural equivalence game that covers the mentioned games on the linear-time~/ branching-time spectrum and moreover applies in coalgebraic generality, and thus instantiates also to equivalence games on systems with non-relational branching type (probabilistic, weighted, game-based etc.). In the present work, we generalize this approach to cover other types of process comparison beyond equivalence, such as behavioural preorders or pseudometrics. At the most general level, we abstract such notions of behavoiural conformance in terms of topological categories, and later specialize to conformances presented as relational structures to obtain a concrete syntax. We obtain a sound and complete generic game for behavioural conformances in this sense. We present a number of instantiations, obtaining game characterizations of, e.g., trace inclusion, probabilistic trace distance, bisimulation topologies, and simulation distances on metric labelled transition systems. △ Less

Submitted 27 January, 2025; v1 submitted 5 November, 2024; originally announced November 2024.

MSC Class: 68Q85 (Primary) ACM Class: F.3.1; F.3.2; F.4.1

Relational Connectors and Heterogeneous Bisimulations

Authors: Pedro Nora, Jurriaan Rot, Lutz Schröder, Paul Wild

Abstract: While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-b… ▽ More While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances. △ Less

Submitted 6 February, 2025; v1 submitted 18 October, 2024; originally announced October 2024.

Comments: Full version of conference paper in Foundations of Software Science and Computation Structures, FoSSaCS 2025

MSC Class: 68Q85; 03B70; 03B45; 18A25 ACM Class: F.3.1; F.4.1

Identity-Preserving Lax Extensions and Where to Find Them

Authors: Sergey Goncharov, Dirk Hofmaan, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fa… ▽ More Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems. △ Less

Submitted 11 January, 2025; v1 submitted 18 October, 2024; originally announced October 2024.

Comments: Full version of STACS 2025 paper

Alternating Nominal Automata with Name Allocation

Authors: Florian Frank, Daniel Hausmann, Stefan Milius, Lutz Schröder, Henning Urbat

Abstract: 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 regis… ▽ More 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. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-$μ$TL, a fixed-point logic with name allocation over finite data words, by one exponential level. △ Less

Submitted 19 May, 2025; v1 submitted 7 August, 2024; originally announced August 2024.

MSC Class: 68Q45 ACM Class: F.4.3

Higher-Order Bialgebraic Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory… ▽ More Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term \emph{(pointed) higher-order GSOS laws}. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the $λ$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances. △ Less

Submitted 26 March, 2025; v1 submitted 26 May, 2024; originally announced May 2024.

Comments: Submitted to J. Funct. Program. Extended and updated version of arXiv:2210.13387

Nominal Tree Automata With Name Allocation

Authors: Simon Prucker, Lutz Schröder

Abstract: Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based on storing data values encountered on the tree in registers for subsequent comparison with further data values. Already on word languages, the expressiveness of… ▽ More Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based on storing data values encountered on the tree in registers for subsequent comparison with further data values. Already on word languages, the expressiveness of such automata models typically increases with the power of control (e.g. deterministic, non-deterministic, alternating). Language inclusion is typically undecidable for non-deterministic or alternating models unless the number of registers is radically restricted, and even then often remains non-elementary. We present an automaton model for data trees that retains a reasonable level of expressiveness, in particular allows non-determinism and any number of registers, while admitting language inclusion checking in elementary complexity, in fact in parametrized exponential time. We phrase the description of our automaton model in the language of nominal sets, building on the recently introduced paradigm of explicit name allocation in nominal automata. △ Less

Submitted 11 July, 2024; v1 submitted 23 May, 2024; originally announced May 2024.

MSC Class: 68Q45 ACM Class: F.4.3

Optimizing LLM Queries in Relational Data Analytics Workloads

Authors: Shu Liu, Asim Biswal, Amog Kamsetty, Audrey Cheng, Luis Gaspar Schroeder, Liana Patel, Shiyi Cao, Xiangxi Mo, Ion Stoica, Joseph E. Gonzalez, Matei Zaharia

Abstract: Batch data analytics is a growing application for Large Language Models (LLMs). LLMs enable users to perform a wide range of natural language tasks, such as classification, entity extraction, and translation, over large datasets. However, LLM inference is highly costly and slow: for example, an NVIDIA L4 GPU running Llama3-8B can only process 6 KB of text per second, taking about a day to handle 1… ▽ More Batch data analytics is a growing application for Large Language Models (LLMs). LLMs enable users to perform a wide range of natural language tasks, such as classification, entity extraction, and translation, over large datasets. However, LLM inference is highly costly and slow: for example, an NVIDIA L4 GPU running Llama3-8B can only process 6 KB of text per second, taking about a day to handle 15 GB of data; processing a similar amount of data costs around $10K on OpenAI's GPT-4o. In this paper, we propose novel techniques that can significantly reduce the cost of LLM calls for relational data analytics workloads. Our key contribution is developing efficient algorithms for reordering the rows and the fields within each row of an input table to maximize key-value (KV) cache reuse when performing LLM serving. As such, our approach can be easily applied to existing analytics systems and serving platforms. Our evaluation shows that our solution can yield up to 3.4x improvement in job completion time on a benchmark of diverse LLM-based queries using Llama 3 models. Our solution also achieves a 32% cost savings under OpenAI and Anthropic pricing models. △ Less

Submitted 9 April, 2025; v1 submitted 9 March, 2024; originally announced March 2024.

Logical Predicates in Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a… ▽ More We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part. △ Less

Submitted 12 January, 2024; v1 submitted 11 January, 2024; originally announced January 2024.

Comments: Extended version

Generic Model Checking for Modal Fixpoint Logics in COOL-MC

Authors: Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder, Aaron Strahlberger

Abstract: 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 $μ$-calculus, CO… ▽ More 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 $μ$-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the $μ$-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. △ Less

Submitted 3 November, 2023; v1 submitted 2 November, 2023; originally announced November 2023.

Comments: Full Version of VMCAI 2024 publication

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

Authors: Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, Paul Wild

Abstract: We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out… ▽ More We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances). △ Less

Submitted 31 January, 2024; v1 submitted 9 October, 2023; originally announced October 2023.

Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Karla Messing

Abstract: Coalgebra, as the abstract study of state-based systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide wi… ▽ More Coalgebra, as the abstract study of state-based systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide with language equivalence. Language equivalence can be captured as behavioural equivalence on the determinization, which is obtained via the standard powerset construction. This construction can be lifted to coalgebraic generality, assuming a so-called Eilenberg-Moore distributive law between the functor termining the type of accepted structure (e.g.\ word languages) and a monad capturing the branching type (e.g.\ nondeterministic, weighted, probabilistic). Eilenberg-Moore-style coalgebraic semantics in this sense has been shown to be essentially subsumed by the more general framework of graded semantics, which is centrally based on graded monads. Graded semantics comes with a range of generic results, in particular regarding invariance and, under suitable conditions, expressiveness of dedicated modal logics for a given semantics; notably, these logics are evaluated on the original state space. We show that the instantiation of such graded logics to the case of Eilenberg-Moore-style semantics works extremely smoothly, and yields expressive modal logics in essentially all cases of interest. We additionally parametrize the framework over a quantale of truth values, thus in particular covering both the two-valued notions of equivalence and quantitative ones, i.e. behavioural distances. △ Less

Submitted 26 April, 2024; v1 submitted 27 July, 2023; originally announced July 2023.

MSC Class: 03B45 (Primary) 03B52 (Secondary) ACM Class: F.4.1

Quantitative Graded Semantics and Spectra of Behavioural Metrics

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing

Abstract: Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable… ▽ More Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems. △ Less

Submitted 27 January, 2025; v1 submitted 2 June, 2023; originally announced June 2023.

MSC Class: 03B45; 03B52; 68Q85 ACM Class: F.4.1

The Alternating-Time μ-Calculus With Disjunctive Explicit Strategies

Authors: Merlin Humml, Lutz Schröder, Dirk Pattinson

Abstract: Alternating-time temporal logic (ATL) and its extensions, including the alternating-time $μ$-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let som… ▽ More Alternating-time temporal logic (ATL) and its extensions, including the alternating-time $μ$-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let some of the agents (revocably) commit to using certain named strategies, as in ATL with explicit strategies (ATLES). In the present work, we extend ATLES with fixpoint operators and strategy disjunction, arriving at the alternating-time $μ$-calculus with disjunctive explicit strategies (AMCDES), which allows for a more flexible formulation of temporal properties (e.g. fairness) and, through strategy disjunction, a form of controlled nondeterminism in commitments. Our main result is an ExpTime upper bound for satisfiability checking (which is thus ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and NP $\cap$ coNP for model checking under fixed interpretations of explicit strategies, and NP under open interpretation. Our key technical tool is a treatment of the AMCDES within the generic framework of coalgebraic logic, which in particular reduces the analysis of most reasoning tasks to the treatment of a very simple one-step logic featuring only propositional operators and next-step operators without nesting; we give a new model construction principle for this one-step logic that relies on a set-valued variant of first-order resolution. △ Less

Submitted 30 May, 2023; originally announced May 2023.

Comments: Full version with appendix as well as corrected set-valued resolution method

ACM Class: F.4.1; I.2.11

Journal ref: Göttlinger, M., Schröder, L., & Pattinson, D. CSL 2021, Leibniz International Proceedings in Informatics (LIPIcs) (pp. 26:1-26:22)

COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics

Authors: Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder

Abstract: 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… ▽ More 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 $μ$-calculus and the alternating-time $μ$-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 $μ$-calculus. △ Less

Submitted 15 June, 2023; v1 submitted 18 May, 2023; originally announced May 2023.

Comments: Final version (corrected slight mistake in Rabin-type formula series)

Weak Similarity in Higher-Order Mathematical Operational Semantics

Authors: Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, Lutz Schröder

Abstract: Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak simil… ▽ More Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the lambda-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method. △ Less

Submitted 28 September, 2023; v1 submitted 16 February, 2023; originally announced February 2023.

Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi

Authors: Daniel Hausmann, Lutz Schröder

Abstract: The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step… ▽ More The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step modalities that are sufficiently well-behaved in a formally defined sense; in particular, rule matches need to be representable by polynomial-sized codes, and the sequent duals of the rules need to absorb cut. While such rule sets have been identified for some important cases, they are not known to exist in all cases of interest, in particular ones involving either integer weights as in the graded $μ$-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying one-step logic, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Notably, our approach directly accommodates unguarded formulae, and thus avoids use of the guardedness transformation. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded $μ$-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic $μ$-calculus with polynomial inequalities. △ Less

Submitted 22 July, 2024; v1 submitted 21 December, 2022; originally announced December 2022.

MSC Class: 03B70; 03B44 ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 20, Issue 3 (July 23, 2024) lmcs:10532

Common Knowledge of Abstract Groups

Authors: Merlin Humml, Lutz Schröder

Abstract: Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in `it is common knowledge among economists'. We introduce such a logic of common knowledge, which we term abstract-group epistemic logic (AGEL). That is, AGEL features a common knowledge op… ▽ More Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in `it is common knowledge among economists'. We introduce such a logic of common knowledge, which we term abstract-group epistemic logic (AGEL). That is, AGEL features a common knowledge operator for groups of agents given by concepts in a separate agent logic that we keep generic, with one possible agent logic being ALC. We show that AGEL is EXPTIME-complete, with the lower bound established by reduction from standard group epistemic logic, and the upper bound by a satisfiability-preserving embedding into the full $μ$-calculus. Further main results include a finite model property (not enjoyed by the full $μ$-calculus) and a complete axiomatization. △ Less

Submitted 29 November, 2022; originally announced November 2022.

Comments: Version with appendix of the AAAI23 publication

MSC Class: 03B42

Towards a Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the pr… ▽ More Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. △ Less

Submitted 26 October, 2022; v1 submitted 24 October, 2022; originally announced October 2022.

Quantitative Hennessy-Milner Theorems via Notions of Density

Authors: Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on… ▽ More The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e.g.~in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo-)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstrass theorem; this allows us to cover, for instance, behavioural ultrametrics. △ Less

Submitted 30 August, 2022; v1 submitted 19 July, 2022; originally announced July 2022.

Uniform Interpolation in Coalgebraic Modal Logic

Authors: Fatemeh Seifan, Lutz Schröder, Dirk Pattinson

Abstract: A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula -- the interpolant -- to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularizati… ▽ More A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula -- the interpolant -- to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above. △ Less

Submitted 1 May, 2022; originally announced May 2022.

Comments: Full version of conference paper in Algebra and Coalgebra in Computer Science (CALCO 2017)

MSC Class: 03B45; 18A35 ACM Class: F.4.1; I.2.4; I.2.3

Graded Monads and Behavioural Equivalence Games

Authors: Chase Ford, Harsh Beohar, Barbara König, Stefan Milius, Lutz Schröder

Abstract: The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pe… ▽ More The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand. △ Less

Submitted 7 May, 2024; v1 submitted 29 March, 2022; originally announced March 2022.

Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence

Authors: Thorsten Wißmann, Stefan Milius, Lutz Schröder

Abstract: We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we const… ▽ More We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time O((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was O(mn). △ Less

Submitted 17 November, 2023; v1 submitted 21 March, 2022; originally announced March 2022.

Comments: Journal version of arXiv:2105.00669, thus text overlap with arXiv:2105.00669. (v4: notes on funding added)

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 4 (November 17, 2022) lmcs:9941

Stateful Structural Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We intr… ▽ More Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences. △ Less

Submitted 11 May, 2022; v1 submitted 22 February, 2022; originally announced February 2022.

Kantorovich Functors and Characteristic Logics for Behavioural Distances

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take… ▽ More Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo-)metrics, and probabilistic (pseudo-)metrics. Coalgebraic behavioural distances have been based either on liftings of SET-functors to categories of metric spaces, or on lax extensions of SET-functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic. △ Less

Submitted 2 May, 2023; v1 submitted 14 February, 2022; originally announced February 2022.

A Point-free Perspective on Lax extensions and Predicate liftings

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Lax extensions of set functors play a key role in various areas including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundame… ▽ More Lax extensions of set functors play a key role in various areas including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result. △ Less

Submitted 7 December, 2023; v1 submitted 23 December, 2021; originally announced December 2021.

Journal ref: Mathematical Structures in Computer Science. 2023:1-30

The Evolution of Binaries under the Influence of Radiation-Driven Winds from a Stellar Companion

Authors: Sophie Lund Schrøder, Morgan MacLeod, Enrico Ramirez-Ruiz, Ilya Mandel, Tassos Fragos, Abraham Loeb, Rosa Wallace Everson

Abstract: Interacting binaries are of general interest as laboratories for investigating the physics of accretion, which gives rise to the bulk of high-energy radiation in the Galaxy. They allow us to probe stellar evolution processes that cannot be studied in single stars. Understanding the orbital evolution of binaries is essential in order to model the formation of compact binaries. Here we focus our att… ▽ More Interacting binaries are of general interest as laboratories for investigating the physics of accretion, which gives rise to the bulk of high-energy radiation in the Galaxy. They allow us to probe stellar evolution processes that cannot be studied in single stars. Understanding the orbital evolution of binaries is essential in order to model the formation of compact binaries. Here we focus our attention on studying orbital evolution driven by angular momentum loss through stellar winds in massive binaries. We run a suite of hydrodynamical simulations of binary stars hosting one mass losing star with varying wind velocity, mass ratio, wind velocity profile and adiabatic index, and compare our results to analytic estimates for drag and angular momentum loss. We find that, at leading order, orbital evolution is determined by the wind velocity and the binary mass ratio. Small ratios of wind to orbital velocities and large accreting companion masses result in high angular momentum loss and a shrinking of the orbit. For wider binaries and binaries hosting lighter mass-capturing companions, the wind mass-loss becomes more symmetric, which results in a widening of the orbit. We present a simple analytic formula that can accurately account for angular momentum losses and changes in the orbit, which depends on the wind velocity and mass ratio. As an example of our formalism, we compare the effects of tides and winds in driving the orbital evolution of high mass X-ray binaries, focusing on Vela X-1 and Cygnus X-1 as examples. △ Less

Submitted 20 July, 2021; originally announced July 2021.

Comments: 22 pages, 16 figures, submitted to ApJ, comments welcome

Monads on Categories of Relational Structures

Authors: Chase Ford, Stefan Milius, Lutz Schröder

Abstract: We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity $λ$ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders ($λ=ω$) or metric spaces ($λ=ω_1$). We establish a bijective correspondence between… ▽ More We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity $λ$ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders ($λ=ω$) or metric spaces ($λ=ω_1$). We establish a bijective correspondence between $λ$-accessible enriched monads on the given category of relational structures and a notion of $λ$-ary algebraic theories (i.e. with operations of arity $<λ$), with the syntax of algebraic theories induced by the relational signature (e.g. inequations or equations-up-to-$ε$). We provide a generic sound and complete derivation system for such relational algebraic theories, thus in particular recovering (extensions of) recent systems of this type for monads on partial orders and metric spaces by instantiation. In particular, we present an $ω_1$-ary algebraic theory of metric completion. The theory-to-monad direction of our correspondence remains true for the case of $κ$-ary algebraic theories and $κ$-accessible monads for $κ<λ$, e.g. for finitary theories over metric spaces. △ Less

Submitted 8 July, 2021; originally announced July 2021.

Comments: 36 pages

Nominal Büchi Automata with Name Allocation

Authors: Henning Urbat, Daniel Hausmann, Stefan Milius, Lutz Schröder

Abstract: Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach omega-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from inpu… ▽ More Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach omega-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking. △ Less

Submitted 10 July, 2021; v1 submitted 7 July, 2021; originally announced July 2021.

Fallback supernova assembly of heavy binary neutron stars and light black hole-neutron star pairs and the common stellar ancestry of GW190425 and GW200115

Authors: Alejandro Vigna-Gómez, Sophie L. Schrøder, Enrico Ramirez-Ruiz, David R. Aguilera-Dena, Aldo Batta, Norbert Langer, Reinhold Willcox

Abstract: The detection of the unusually heavy binary neutron star merger GW190425 marked a stark contrast to the mass distribution from known Galactic pulsars in double neutron star binaries and gravitational-wave source GW170817. We suggest here a formation channel for heavy binary neutron stars and light black hole - neutron star binaries in which massive helium stars, which had their hydrogen envelope r… ▽ More The detection of the unusually heavy binary neutron star merger GW190425 marked a stark contrast to the mass distribution from known Galactic pulsars in double neutron star binaries and gravitational-wave source GW170817. We suggest here a formation channel for heavy binary neutron stars and light black hole - neutron star binaries in which massive helium stars, which had their hydrogen envelope removed during a common envelope phase, remain compact and avoid mass transfer onto the neutron star companion, possibly avoiding pulsar recycling. We present three-dimensional simulations of the supernova explosion of the massive stripped helium star and follow the mass fallback evolution and the subsequent accretion onto the neutron star companion. We find that fallback leads to significant mass growth in the newly formed neutron star. This can explain the formation of heavy binary neutron star systems such as GW190425, as well as predict the assembly of light black hole - neutron star systems such as GW200115. This formation avenue is consistent with the observed mass-eccentricity correlation of binary neutron stars in the Milky Way. Finally, avoiding mass transfer suggests an unusually long spin-period population of pulsar binaries in our Galaxy. △ Less

Submitted 22 September, 2021; v1 submitted 23 June, 2021; originally announced June 2021.

Comments: 7 main pages, 3 main figures, plus appendices. Accepted for publication in ApJ Letters

Explaining Behavioural Inequivalence Generically in Quasilinear Time

Authors: Thorsten Wißmann, Stefan Milius, Lutz Schröder

Abstract: We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we const… ▽ More We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time $\mathcal{O}((m+n) \log n)$ on systems with $n$ states and $m$ transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was $\mathcal{O}(m n)$. △ Less

Submitted 28 September, 2021; v1 submitted 3 May, 2021; originally announced May 2021.

Comments: Full version with appendix containing all proofs

The hydrodynamic evolution of binary black holes embedded within the vertically stratified disks of active galactic nuclei

Authors: Nicholas Kaaz, Sophie Lund Schrøder, Jeff J. Andrews, Andrea Antoni, Enrico Ramirez-Ruiz

Abstract: Stellar-mass black holes can become embedded within the gaseous disks of active galactic nuclei (AGNs). Afterwards, their interactions are mediated by their gaseous surroundings. In this work, we study the evolution of stellar-mass binary black holes (BBHs) embedded within AGN disks using a combination of three-dimensional hydrodynamic simulations and analytic methods, focusing on environments in… ▽ More Stellar-mass black holes can become embedded within the gaseous disks of active galactic nuclei (AGNs). Afterwards, their interactions are mediated by their gaseous surroundings. In this work, we study the evolution of stellar-mass binary black holes (BBHs) embedded within AGN disks using a combination of three-dimensional hydrodynamic simulations and analytic methods, focusing on environments in which the AGN disk scale height $H$ is $\gtrsim$ the BBH sphere of influence. We model the local surroundings of the embedded BBHs using a wind tunnel formalism and characterize different accretion regimes based on the local properties of the disk, which range from wind-dominated to quasi-spherical. We use our simulations to develop prescriptions for mass accretion and drag for embedded BBHs. We use these prescriptions, along with AGN disk models that can represent the Toomre-unstable outer regions of AGN disks, to study the long-term evolution of the BBHs as they migrate through the disk. We find that BBHs typically merge within $\lesssim 5-30\,{\rm Myr}$, increasing their mass significantly in the process, allowing BBHs to enter (or cross) the pair-instability supernova mass gap. The rate at which gas is supplied to these BBHs often exceeds the Eddington limit, sometimes by several orders of magnitude. We conclude that most embedded BBHs will merge before migrating significantly in the disk. Depending on the conditions of the ambient gas and the distance to the system, LISA can detect the transition between the gas-dominated and gravitational wave dominated regime for inspiraling BBHs that are formed sufficiently close to the AGN ($\lesssim$ 0.1 pc). We also discuss possible electromagnetic signatures during and following the inspiral, finding that it is generally unlikely but not inconceivable for the bolometric luminosity of the BBH to exceed that of the host AGN. △ Less

Submitted 25 January, 2023; v1 submitted 22 March, 2021; originally announced March 2021.

Comments: 19 pages, 8 figures, accepted to ApJ

Finitary Monads on the Category of Posets

Authors: Jiří Adámek, Chase Ford, Stefan Milius, Lutz Schröder

Abstract: Finitary monads on $\mathsf{Pos}$ are characterized as the precisely the free-algebra monads of varieties of algebras. These are classes of ordered algebras specified by inequations in context. Analagously, finitary enriched monads on $\mathsf{Pos}$ are characterized: here we work with varieties of coherent algebras which means that their operations are monotone. Finitary monads on $\mathsf{Pos}$ are characterized as the precisely the free-algebra monads of varieties of algebras. These are classes of ordered algebras specified by inequations in context. Analagously, finitary enriched monads on $\mathsf{Pos}$ are characterized: here we work with varieties of coherent algebras which means that their operations are monotone. △ Less

Submitted 30 November, 2020; originally announced November 2020.

Behavioural Preorders via Graded Monads

Authors: Chase Ford, Stefan Milius, Lutz Schröder

Abstract: Like notions of process equivalence, behavioural preorders on processes come in many flavours, ranging from fine-grained comparisons such as ready simulation to coarse-grained ones such as trace inclusion. Often, such behavioural preorders are characterized in terms of theory inclusion in dedicated characteristic logics; e.g. simulation is characterized by theory inclusion in the positive fragment… ▽ More Like notions of process equivalence, behavioural preorders on processes come in many flavours, ranging from fine-grained comparisons such as ready simulation to coarse-grained ones such as trace inclusion. Often, such behavioural preorders are characterized in terms of theory inclusion in dedicated characteristic logics; e.g. simulation is characterized by theory inclusion in the positive fragment of Hennessy-Milner logic. We introduce a unified semantic framework for behavioural preorders and their characteristic logics in which we parametrize the system type as a functor on the category $\mathsf{Pos}$ of partially ordered sets following the paradigm of universal coalgebra, while behavioural preorders are captured as graded monads on $\mathsf{Pos}$, in generalization of a previous approach to notions of process equivalence. We show that graded monads on $\mathsf{Pos}$ are induced by a form of graded inequational theories that we introduce here. Moreover, we provide a general notion of modal logic compatible with a given graded behavioural preorder, along with a criterion for expressiveness, in the indicated sense of characterization of the behavioural preorder by theory inclusion. We illustrate our main result on various behavioural preorders on labelled transition systems and probabilistic transition systems. △ Less

Submitted 30 April, 2021; v1 submitted 29 November, 2020; originally announced November 2020.

MSC Class: 18C15; 03B45 ACM Class: F.4.1; F.3.1

Successful Common Envelope Ejection and Binary Neutron Star Formation in 3D Hydrodynamics

Authors: Jamie A. P. Law-Smith, Rosa Wallace Everson, Enrico Ramirez-Ruiz, Selma E. de Mink, Lieke A. C. van Son, Ylva Götberg, Stefan Zellmann, Alejandro Vigna-Gómez, Mathieu Renzo, Samantha Wu, Sophie L. Schrøder, Ryan J. Foley, Tenley Hutchinson-Smith

Abstract: A binary neutron star merger has been observed in a multi-messenger detection of gravitational wave (GW) and electromagnetic (EM) radiation. Binary neutron stars that merge within a Hubble time, as well as many other compact binaries, are expected to form via common envelope evolution. Yet five decades of research on common envelope evolution have not yet resulted in a satisfactory understanding o… ▽ More A binary neutron star merger has been observed in a multi-messenger detection of gravitational wave (GW) and electromagnetic (EM) radiation. Binary neutron stars that merge within a Hubble time, as well as many other compact binaries, are expected to form via common envelope evolution. Yet five decades of research on common envelope evolution have not yet resulted in a satisfactory understanding of the multi-spatial multi-timescale evolution for the systems that lead to compact binaries. In this paper, we report on the first successful simulations of common envelope ejection leading to binary neutron star formation in 3D hydrodynamics. We simulate the dynamical inspiral phase of the interaction between a 12$M_\odot$ red supergiant and a 1.4$M_\odot$ neutron star for different initial separations and initial conditions. For all of our simulations, we find complete envelope ejection and final orbital separations of $a_{\rm f} \approx 1.3$-$5.1 R_\odot$ depending on the simulation and criterion, leading to binary neutron stars that can merge within a Hubble time. We find $α_{\rm CE}$-equivalent efficiencies of $\approx 0.1$-$2.7$ depending on the simulation and criterion, but this may be specific for these extended progenitors. We fully resolve the core of the star to $\lesssim 0.005 R_\odot$ and our 3D hydrodynamics simulations are informed by an adjusted 1D analytic energy formalism and a 2D kinematics study in order to overcome the prohibitive computational cost of simulating these systems. The framework we develop in this paper can be used to simulate a wide variety of interactions between stars, from stellar mergers to common envelope episodes leading to GW sources. △ Less

Submitted 22 July, 2022; v1 submitted 12 November, 2020; originally announced November 2020.

Comments: 28 pages, 16 figures. v2: ran some additional simulations to address comments from the community. Included new criterion for calculating a_f and alpha_CE, resulting in new range of values. Added Table 1, updated Fig 3, added Fig 4, updated Fig 12, updated Fig 13, added Fig 14, added Fig 15, added Fig 16. Now submitted to ApJ

A Linear-Time Nominal $μ$-Calculus with Name Allocation

Authors: Daniel Hausmann, Stefan Milius, Lutz Schröder

Abstract: Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding no… ▽ More Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-muTL for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-muTL allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-muTL over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter. △ Less

Submitted 20 August, 2021; v1 submitted 21 October, 2020; originally announced October 2020.

Comments: Extended version (shorter version published at MFCS 2021)

The Young Supernova Experiment: Survey Goals, Overview, and Operations

Authors: D. O. Jones, R. J. Foley, G. Narayan, J. Hjorth, M. E. Huber, P. D. Aleo, K. D. Alexander, C. R. Angus, K. Auchettl, V. F. Baldassare, S. H. Bruun, K. C. Chambers, D. Chatterjee, D. L. Coppejans, D. A. Coulter, L. DeMarchi, G. Dimitriadis, M. R. Drout, A. Engel, K. D. French, A. Gagliano, C. Gall, T. Hung, L. Izzo, W. V. Jacobson-Galán , et al. (46 additional authors not shown)

Abstract: Time domain science has undergone a revolution over the past decade, with tens of thousands of new supernovae (SNe) discovered each year. However, several observational domains, including SNe within days or hours of explosion and faint, red transients, are just beginning to be explored. Here, we present the Young Supernova Experiment (YSE), a novel optical time-domain survey on the Pan-STARRS tele… ▽ More Time domain science has undergone a revolution over the past decade, with tens of thousands of new supernovae (SNe) discovered each year. However, several observational domains, including SNe within days or hours of explosion and faint, red transients, are just beginning to be explored. Here, we present the Young Supernova Experiment (YSE), a novel optical time-domain survey on the Pan-STARRS telescopes. Our survey is designed to obtain well-sampled $griz$ light curves for thousands of transient events up to $z \approx 0.2$. This large sample of transients with 4-band light curves will lay the foundation for the Vera C. Rubin Observatory and the Nancy Grace Roman Space Telescope, providing a critical training set in similar filters and a well-calibrated low-redshift anchor of cosmologically useful SNe Ia to benefit dark energy science. As the name suggests, YSE complements and extends other ongoing time-domain surveys by discovering fast-rising SNe within a few hours to days of explosion. YSE is the only current four-band time-domain survey and is able to discover transients as faint $\sim$21.5 mag in $gri$ and $\sim$20.5 mag in $z$, depths that allow us to probe the earliest epochs of stellar explosions. YSE is currently observing approximately 750 square degrees of sky every three days and we plan to increase the area to 1500 square degrees in the near future. When operating at full capacity, survey simulations show that YSE will find $\sim$5000 new SNe per year and at least two SNe within three days of explosion per month. To date, YSE has discovered or observed 8.3% of the transient candidates reported to the International Astronomical Union in 2020. We present an overview of YSE, including science goals, survey characteristics and a summary of our transient discoveries to date. △ Less

Submitted 5 January, 2021; v1 submitted 19 October, 2020; originally announced October 2020.

Comments: ApJ, in press; more information at https://yse.ucsc.edu/

Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

Authors: Clemens Kupke, Dirk Pattinson, Lutz Schröder

Abstract: We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequali… ▽ More We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka's linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e. in coalgebraic hybrid logic. △ Less

Submitted 27 November, 2021; v1 submitted 2 September, 2020; originally announced September 2020.

Comments: Extended version of conference paper in FCT 2015

MSC Class: 03B70; 03B45; 03B35 ACM Class: F.4.1; I.2.3; I.2.4

Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions

Authors: Paul Wild, Lutz Schröder

Abstract: In systems involving quantitative data, such as probabilistic, fuzzy, or metric systems, behavioural distances provide a more fine-grained comparison of states than two-valued notions of behavioural equivalence or behaviour inclusion. Like in the two-valued case, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this… ▽ More In systems involving quantitative data, such as probabilistic, fuzzy, or metric systems, behavioural distances provide a more fine-grained comparison of states than two-valued notions of behavioural equivalence or behaviour inclusion. Like in the two-valued case, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy (bi-)simulations that need not themselves be hemi- or pseudometrics; this is analogous to classical simulations and bisimulations, which need not be preorders or equivalence relations, respectively. The known generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For nonexpansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic. All our results explicitly hold also for asymmetric distances (hemimetrics), i.e. notions of quantitative simulation. △ Less

Submitted 14 June, 2022; v1 submitted 2 July, 2020; originally announced July 2020.

MSC Class: 68Q85; 03B45; 03B52 ACM Class: F.4.1; I.2.4

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 2 (June 15, 2022) lmcs:7351