arXiv subjects

Lutz Schröder

Publications and source records attributed to Lutz Schröder.

At least 19 recordsLinked to original sources

arXiv2026

Graded Semantics of Nominal Systems

Nominal automata models and transition systems serve as formalisms for languages and processes carrying data, and as such relate closely to classical register-based models. The paradigm of name allocation in nominal systems helps alleviate the pervasive computational hardness of register-based models in a tradeoff between expressiveness and computational tractability. For instance, regular nondeterministic nominal automata (RNNAs) correspond, under their local freshness semantics, to a form of lossy register automata. Unlike the full register automaton model, RNNAs allow for inclusion checking in elementary complexity (parametrized PSPACE); similarly, trace inclusion in the underlying nominal transition systems is in parametrized PSPACE. In the present work, we develop a unified algebraic treatment of spectra of behavioural equivalences on nominal systems in the framework of graded monads, working in the setting of universal coalgebra. In particular, we extend the associated notion of graded algebraic theory to the nominal setting, and use this to give an algebraic axiomatization of the (linear-time) global and local freshness semantics of nominal systems with name allocation. As an illustration of the benefits of graded monads, we develop a nominal version of the generic game characterization of graded semantics, which we instantiate to obtain trace equivalence games for nominal transition systems under global and local freshness semantics.

cs.LO↗

arXiv2026

Higher-order bialgebraic semantics

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 (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 lambda-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.

cs.LO↗

arXiv2026

Towards a Higher-Order Mathematical Operational Semantics

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.

cs.LO↗

arXiv2026

Nominal Automata with Name Deallocation

Data words with binders formalize concurrently allocated memory. Most name-binding mechanisms in formal languages, such as the $λ$-calculus, adhere to properly nested scoping. In contrast, stateful programming languages with explicit memory allocation and deallocation, such as C, commonly interleave the scopes of allocated memory regions. This phenomenon is captured in dedicated formalisms such as dynamic sequences and bracket algebra, which similarly feature explicit allocation and deallocation of letters. One of the classical formalisms for data languages are register automata, which have been shown to be equivalent to automata models over nominal sets. In the present work, we introduce a nominal automaton model for languages of data words with explicit allocation and deallocation that strongly resemble dynamic sequences, extending existing nominal automata models by adding deallocating transitions. Using a finite NFA-type representation of the model, we establish a Kleene theorem that shows equivalence with a natural expression language. Moreover, we show that our non-deterministic model allows for determinization, a quite unusual phenomenon in the realm of nominal and register automata.

cs.FL↗

arXiv2026

Generalized Kantorovich-Rubinstein Duality beyond Hausdorff and Kantorovich

The classical Kantorovich-Rubinstein duality guarantees coincidence between metrics on the space of probability distributions defined on the one hand via transport plans (couplings) and on the other hand via price functions. Both constructions have been lifted to the level of generality of set functors, with the construction based on couplings referred to as the Wasserstein or simply the coupling-based lifting, and the price-function-based construction as the Kantorovich or codensity lifting, both based on a choice of quantitative modalities for the given functor. It is known that every coupling-based lifting can be expressed as a price-function-based lifting; however, the latter in general needs to use additional modalities. We give an example showing that this cannot be avoided in general. We refer to cases in which the same modalities can be used as satisfying the generalized Kantorovich-Rubinstein duality. We establish the generalized Kantorovich-Rubinstein duality in this sense for two important cases: The Lévy-Prokhorov distance on distributions, which finds wide-spread applications in machine learning due to its favourable stability properties, and the standard metric on convex sets of distributions that arises by combining the Hausdorff and Kantorovich-Rubinstein distances.

cs.LO↗

arXiv2026

The Only Distributive Law Over the Powerset Monad Is the One You Know

Distributive laws of set functors over the powerset monad (also known as Kleisli laws for the powerset monad) are well-known to be in one-to-one correspondence with extensions of set functors to functors on the category of sets and relations. We study the question of existence and uniqueness of such distributive laws. Our main result entails that an accessible set functor admits a distributive law over the powerset monad if and only if it preserves weak pullbacks, in which case the so-called power law (which induces the Barr extension) is the unique one. Furthermore, we show that the powerset functor admits exactly three distributive laws over the powerset monad, revealing that uniqueness may fail for non-accessible functors.

cs.LO↗

arXiv2026

Non-Expansive Fuzzy Coalgebraic Logic

Fuzzy logic extends the classical truth values "true" and "false" with additional truth degrees in between. More specifically, fuzzy modal logics in this sense are given by a choice of fuzzy modalities and a fuzzy propositional base. It has been noted that fuzzy modal logics over the Zadeh base, which interprets disjunction as maximum, are often computationally tractable but on the other hand add little in the way of expressivity to their classical counterparts. Contrastingly, fuzzy modal logics over the more expressive Lukasiewicz base have attractive logical properties but are often computationally less tractable or even undecidable. In the basic case of the modal logic of fuzzy relations, sometimes termed fuzzy ALC, it has recently been shown that an intermediate non-expansive propositional base, known from characteristic logics for behavioural distances of quantitative systems, strikes a balance between these poles: It provides increased expressiveness over the Zadeh base while avoiding the computational problems of the Lukasiewicz base, in fact allowing for reasoning in PSpace. Modal logics, in particular fuzzy modal logics, generally vary widely in terms of syntax and semantics, involving, for instance, probabilistic, preferential, or weighted structures. Coalgebraic modal logic provides a unifying framework for wide ranges of semantically different modal logics, both two-valued and fuzzy. In the present work, we focus on non-expansive coalgebraic fuzzy modal logics, providing a criterion for decidability in PSpace. Using this criterion, we recover the mentioned complexity result for non-expansive fuzzy ALC and moreover obtain new PSpace upper bounds for various quantitative modal logics over probabilistic and metric transition systems. Notably, we show that the logic of generally, which has recently been shown to characterize e-distance on Markov chains, is decidable in PSpace.

cs.LO↗

arXiv2026

Computing Distinguishing Formulae for Threshold-Based Behavioural Distances

Behavioural distances generally offer more fine-grained means of comparing quantitative systems than two-valued behavioural equivalences. They often relate to quantitative modalities, which generate quantitative modal logics that characterize a given behavioural distance in terms of the induced logical distance. We develop a unified framework for behavioural distances and logics induced by a special type of modalities that lift two-valued predicates to quantitative predicates. A typical example is the probability operator, which maps a two-valued predicate $A$ to a quantitative predicate on probability distributions assigning to each distribution the respective probability of $A$. Correspondingly, the prototypical example of our framework is $ε$-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular Lévy-Prokhorov distance on distributions. Other examples include behavioural distance on metric transition systems and Hausdorff behavioural distance on fuzzy transition systems. Our main generic results concern the polynomial-time extraction of distinguishing formulae in two characteristic modal logics: A two-valued logic with a notion of satisfaction up to $ε$, and a quantitative modal logic. These results instantiate to new results in many of the mentioned examples. Notably, we obtain polynomial-time extraction of distinguishing formulae for $ε$-bisimulation distance of Markov chains in a quantitative logic featuring a `generally' modality used in probabilistic knowledge representation.

cs.LO↗

arXiv2025

Non-expansive Fuzzy ALC

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.

cs.LO↗

arXiv2025

Bialgebraic Reasoning on Stateful Languages

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.

cs.PL↗

arXiv2025

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

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.

cs.LO↗

arXiv2025

Relators and Notions of Simulation Revisited

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.

cs.LO↗

arXiv2025

Alternating Nominal Automata with Name Allocation

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.

cs.FL↗

arXiv2025

Relational Connectors and Heterogeneous Bisimulations

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.

cs.LO↗

arXiv2025

Behavioural Conformances based on Lax Couplings

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.

cs.LO↗

arXiv2025

Conformance Games for Graded Semantics

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.

cs.LO↗

arXiv2025

Quantitative Graded Semantics and Spectra of Behavioural Metrics

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.

cs.LO↗

arXiv2025

Identity-Preserving Lax Extensions and Where to Find Them

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.

cs.LO↗