arXiv subjects

Manfred Droste

Publications and source records attributed to Manfred Droste.

At least 19 recordsLinked to original sources

arXiv2026

The Value Generating Power of Weighted Tree Automata with Initial Algebra Semantics

We consider the generating power of the initial algebra semantics of weighted tree automata over strong bimonoids (hence also over semirings) and the question under which conditions the weighted tree automata can produce only finitely many values. We show that there exists a right-distributive strong bimonoid which is bi-locally finite but not locally finite. We also show that if the ranked alphabet contains a symbol with rank at least two, then for any finitely generated strong bimonoid, weighted tree automata can generate, via their initial algebra semantics, all elements of the strong bimonoid. As a consequence of these results, for bi-locally finite right-distributive strong bimonoids which are not locally finite, weighted tree automata can generate infinitely many values, provided that the input ranked alphabet contains a symbol with rank at least two. This is in sharp contrast to the setting of weighted string automata, which can generate only finitely many values. As a further consequence, for any finitely generated semiring, there exists a weighted tree automaton which generates, via its run semantics, all elements of the semiring.

cs.FL↗

arXiv2026

Discrete Linear Ensemble Logic

We study the discrete point-based fragment of Ensemble Logic $\EL(\Nat)$ over the natural numbers, a logic combining displacement $\varphi_u$, bounded metric modalities $\boldBox_t$ and $\mdiamond_t$ with additive bounds, Boolean connectives, and first-order quantification over $\Nat$. Motivated by the need for a unified symbolic layer for biomedical knowledge with temporal, spatial, genomic, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of $\EL(\Nat)$ over a finite proposition set $\mathcal{P}$ into first-order monadic Presburger arithmetic $\FO(\Nat,<,+;\mathcal{P})$. This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter machines with recurring control states proves that satisfiability is $\Sigma^1_1$-complete and validity is dually $\Pi^1_1$-complete. Expressively, $\EL(\Nat)$ strictly extends the star-free $\omega$-languages and is incomparable with the $\omega$-regular languages: it defines the non-$\omega$-regular counting language $\{a^mb^mc^md^m\mid m\geq 1\}\cdot\Sigma^\omega$, whereas a delimited parity language remains outside the logic by classical Presburger-arithmetic lower bounds. On the proof-theoretic side, we present a sound Hilbert system $\HEL$ and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible.

cs.LO↗

arXiv2026

Weighted Automata and Regular Expressions for Financial Systems

We introduce weighted finite finance automata (WFFA), a formal framework for modeling and analyzing quantitative properties of financial systems driven by uncertain economic variables such as stock prices, interest rates, and exchange rates. The model provides a compositional and language-theoretic approach to scenario-based financial analysis, enabling systematic evaluation of financial instruments and trading strategies. To specify such systems, we introduce weighted finance regular expressions, a declarative language for quantitative financial properties. We establish a Kleene-Sch\"utzenberger-type correspondence between WFFAs and weighted finance regular expressions, together with effective translation procedures between the two formalisms. On the algorithmic side, we investigate fundamental decision and optimization problems for WFFAs, including the computation of extremal payoffs, and identify expressive yet computationally tractable subclasses. These results provide a foundation for formal, compositional, and efficient analysis of financial systems under multiple market scenarios.

cs.FL↗

arXiv2025

Free polynomial strong bimonoids

Recently, in weighted automata theory the weight structure of strong bimonoids has found much interest; they form a generalization of semirings and are closely related to near-semirings studied in algebra. Here, we define polynomials over a set $X$ of indeterminates as well as an addition and a multiplication. We show that with these operations, they form a right-distributive strong bimonoid, that this polynomial strong bimonoid is free over $X$ in the class of all right-distributive strong bimonoids and that it is both left- and right-cancellative. We show by purely algebraic reasoning that two arbitrary terms are equivalent modulo the laws of right-distributive strong bimonoids if and only if their representing polynomials are equivalent by the laws of only associativity and commutativity of addition and associativity of multiplication. We give effective procedures for constructing the representing polynomials. As a consequence, we obtain that the equivalence of arbitrary terms modulo the laws of right-distributive strong bimonoids can be decided in exponential time. Using term-rewriting methods, we show that each term can be reduced to a unique polynomial as normal form. We also derive corresponding results for the free idempotent right-distributive polynomial strong bimonoid over $X$. We construct an idempotent strong bimonoid which is weakly locally finite but not locally finite and show an application of it in weighted automata theory.

math.RA↗

arXiv2025

Fagin's Theorem for Semiring Turing Machines

In recent years, quantitative complexity over semirings has been intensively investigated. In this context, Eiter and Kiesel (Semiring Reasoning Frameworks in AI and Their Computational Complexity, J. Artif. Intell. Res., 2023) introduced non-deterministic Turing Machines with semiring-weighted transitions (SRTMs) to capture the complexity of a manifold of semiring frameworks. Beyond computational complexity, they posed the question of how we can relate the computational power of SRTMs to logical expressiveness. While this question was partially addressed for a more limited machine model by Badia et al.\ (Logical characterizations of weighted complexity classes, MFCS, 2024), the full question remained open. To answer it, we present an improved version of Eiter and Kiesel's SRTM model of computation. First and foremost, this enables us to prove a Fagin Theorem for the SRTM model, i.e., we show that the quantitative complexity class $\text{NP}_\infty(R)$, which comprises non-deterministic polynomial time computability in the improved SRTM model over a commutative semiring $R$, is captured by a version of weighted existential second-order logic that allows for predicates interpreted as semiring-annotated relations over $R$. Furthermore, we argue that the new SRTM model is preferable over the original one and show that it reclaims some important results from Eiter and Kiesel (2023) that were flawed with respect to the latter.

cs.CC↗

arXiv2024

Run supports and initial algebra supports of weighted automata

We consider weighted automata over words and over trees where the weight algebras are strong bimonoids, i.e., semirings which may lack distributivity. It is well known that, for each such weighted automaton, its run semantics and its initial algebra semantics can be different, due to the absence of distributivity. Here we investigate the question under which conditions on a zero-sum-free strong bimonoid the support of the run semantics equals the support of the initial algebra semantics. We prove a characterization of this equality both for weighted automata over words and for weighted automata over trees in terms of two weakened distributivity laws for the strong bimonoids which are required to hold only for expressions evaluating to zero. This provides a natural extension of two classical results on the coincidence of the run semantics and the initial algebra semantics. We also consider shortly the images of the two semantics functions.

cs.FL↗

arXiv2024

The generating power of weighted tree automata with initial algebra semantics

We consider the images of the initial algebra semantics of weighted tree automata over strong bimonoids (hence also over semirings). These images are subsets of the carrier set of the underlying strong bimonoid. We consider locally finite, weakly locally finite, and bi-locally finite strong bimonoids. We show that there exists a strong bimonoid which is weakly locally finite and not locally finite. We also show that if the ranked alphabet contains a binary symbol, then for any finitely generated strong bimonoid, weighted tree automata can generate, via their initial algebra semantics, all elements of the strong bimonoid. As a consequence of these results, for weakly locally finite strong bimonoids which are not locally finite, weighted tree automata can generate infinite images provided that the input ranked alphabet contains at least one binary symbol. This is in sharp contrast to the setting of weighted string automata, where each such image is known to be finite. As a further consequence, for any finitely generated semiring, there exists a weighted tree automaton which generates, via its run semantics, all elements of the semiring.

cs.FL↗

arXiv2024

Logical Characterizations of Weighted Complexity Classes

Fagin's seminal result characterizing $\mathsf{NP}$ in terms of existential second-order logic started the fruitful field of descriptive complexity theory. In recent years, there has been much interest in the investigation of quantitative (weighted) models of computations. In this paper, we start the study of descriptive complexity based on weighted Turing machines over arbitrary semirings. We provide machine-independent characterizations (over ordered structures) of the weighted complexity classes $\mathsf{NP}[\mathcal{S}], \mathsf{FP}[\mathcal{S}]$, $\mathsf{FPLOG}[\mathcal{S}]$, $\mathsf{FPSPACE}[\mathcal{S}]$, and $\mathsf{FPSPACE}_{poly}[\mathcal{S}]$ in terms of definability in suitable weighted logics for an arbitrary semiring $\mathcal{S}$. In particular, we prove weighted versions of Fagin's theorem (even for arbitrary structures, not necessarily ordered, provided that the semiring is idempotent and commutative), the Immerman--Vardi's theorem (originally for $\mathsf{P}$) and the Abiteboul--Vianu--Vardi's theorem (originally for $\mathsf{PSPACE}$). We also address a recent open problem proposed by Eiter and Kiesel.

math.LO↗

arXiv2021

Finite-image property of weighted tree automata over past-finite monotonic strong bimonoids

We consider weighted tree automata over strong bimonoids (for short: wta). A wta $\mathcal{A}$ has the finite-image property if its recognized weighted tree language $[\![\mathcal{A}]\!]$ has finite image; moreover, $\mathcal{A}$ has the preimage property if the preimage under $[\![\mathcal{A}]\!]$ of each element of the underlying strong bimonoid is a recognizable tree language. For each wta $\mathcal{A}$ over a past-finite monotonic strong bimonoid we prove the following results. In terms of $\mathcal{A}$'s structural properties, we characterize whether it has the finite-image property. We characterize those past-finite monotonic strong bimonoids such that for each wta $\mathcal{A}$ it is decidable whether $\mathcal{A}$ has the finite-image property. In particular, the finite-image property is decidable for wta over past-finite monotonic semirings. Moreover, we prove that $\mathcal{A}$ has the preimage property. All our results also hold for weighted string automata.

cs.FL↗

arXiv2020

Greibach Normal Form for $\omega$-Algebraic Systems and Weighted Simple $\omega$-Pushdown Automata

In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of $\omega$-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Sch\"utzenberger 1963). As in the theory of formal grammars, these weighted context-free languages, or $\omega$-algebraic series, can be represented as solutions of mixed $\omega$-algebraic systems of equations and by weighted $\omega$-pushdown automata. In our first main result, we show that (mixed) $\omega$-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple $\omega$-reset pushdown automata recognize all $\omega$-algebraic series. Simple $\omega$-reset automata do not use $\epsilon$-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.

cs.FL↗

arXiv2019

Aperiodic Weighted Automata and Weighted First-Order Logic

By fundamental results of Sch\"utzenberger, McNaughton and Papert from the 1970s, the classes of first-order definable and aperiodic languages coincide. Here, we extend this equivalence to a quantitative setting. For this, weighted automata form a general and widely studied model. We define a suitable notion of a weighted first-order logic. Then we show that this weighted first-order logic and aperiodic polynomially ambiguous weighted automata have the same expressive power. Moreover, we obtain such equivalence results for suitable weighted sublogics and finitely ambiguous or unambiguous aperiodic weighted automata. Our results hold for general weight structures, including all semirings, average computations of costs, bounded lattices, and others.

cs.FL↗

arXiv2017

MK-fuzzy Automata and MSO Logics

We introduce MK-fuzzy automata over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a B\"uchi type theorem.

cs.FL↗

arXiv2017

The Triple-Pair Construction for Weighted $\omega$-Pushdown Automata

Let S be a complete star-omega semiring and Sigma be an alphabet. For a weighted omega-pushdown automaton P with stateset 1...n, n greater or equal to 1, we show that there exists a mixed algebraic system over a complete semiring-semimodule pair ((S< >)^nxn, (S< >)^n) such that the behavior ||P|| of P is a component of a solution of this system. In case the basic semiring is the Boolean semiring or the semiring of natural numbers (augmented with infinity), we show that there exists a mixed context-free grammar that generates ||P||. The construction of the mixed context-free grammar from P is a generalization of the well known triple construction and is called now triple-pair construction for omega-pushdown automata.

cs.FL↗

arXiv2017

Weighted Operator Precedence Languages

In the last years renewed investigation of operator precedence languages (OPL) led to discover important properties thereof: OPL are closed with respect to all major operations, are characterized, besides the original grammar family, in terms of an automata family and an MSO logic; furthermore they significantly generalize the well-known visibly pushdown languages (VPL). In another area of research, quantitative models of systems are also greatly in demand. In this paper, we lay the foundation to marry these two research fields. We introduce weighted operator precedence automata and show how they are both strict extensions of OPA and weighted visibly pushdown automata. We prove a Nivat-like result which shows that quantitative OPL can be described by unweighted OPA and very particular weighted OPA. In a B\"uchi-like theorem, we show that weighted OPA are expressively equivalent to a weighted MSO-logic for OPL.

cs.FL↗

arXiv2017

Weighted omega-Restricted One Counter Automata

Let $S$ be a complete star-omega semiring and $\Sigma$ be an alphabet. For a weighted $\omega$-restricted one-counter automaton $\mathcal{C}$ with set of states $\{1, \dots, n\}$, $n \geq 1$, we show that there exists a mixed algebraic system over a complete semiring-semimodule pair ${((S \ll \Sigma^* \gg)^{n\times n}, (S \ll \Sigma^{\omega}\gg)^n)}$ such that the behavior $\Vert\mathcal{C} \Vert$ of $\mathcal{C}$ is a component of a solution of this system. In case the basic semiring is $\mathbb{B}$ or $\mathbb{N}^{\infty}$ we show that there exists a mixed context-free grammar that generates $\Vert\mathcal{C} \Vert$. The construction of the mixed context-free grammar from $\mathcal{C}$ is a generalization of the well-known triple construction in case of restricted one-counter automata and is called now triple-pair construction for $\omega$-restricted one-counter automata.

cs.FL↗

arXiv2016

Weighted Linear Dynamic Logic

We introduce a weighted linear dynamic logic (weighted LDL for short) and show the expressive equivalence of its formulas to weighted rational expressions. This adds a new characterization for recognizable series to the fundamental Sch\"utzenberger theorem. Surprisingly, the equivalence does not require any restriction to our weighted LDL. Our results hold over arbitrary (resp. totally complete) semirings for finite (resp. infinite) words. As a consequence, the equivalence problem for weighted LDL formulas over fields is decidable in doubly exponential time. In contrast to classical logics, we show that our weighted LDL is expressively incomparable to weighted LTL for finite words. We determine a fragment of the weighted LTL such that series over finite and infinite words definable by LTL formulas in this fragment are definable also by weighted LDL formulas.

cs.LO↗

arXiv2015

Weighted Automata and Logics for Infinite Nested Words

Nested words introduced by Alur and Madhusudan are used to capture structures with both linear and hierarchical order, e.g. XML documents, without losing valuable closure properties. Furthermore, Alur and Madhusudan introduced automata and equivalent logics for both finite and infinite nested words, thus extending B\"uchi's theorem to nested words. Recently, average and discounted computations of weights in quantitative systems found much interest. Here, we will introduce and investigate weighted automata models and weighted MSO logics for infinite nested words. As weight structures we consider valuation monoids which incorporate average and discounted computations of weights as well as the classical semirings. We show that under suitable assumptions, two resp. three fragments of our weighted logics can be transformed into each other. Moreover, we show that the logic fragments have the same expressive power as weighted nested word automata.

cs.FL↗

arXiv2015

Multi-weighted Automata and MSO Logic

Weighted automata are non-deterministic automata where the transitions are equipped with weights. They can model quantitative aspects of systems like costs or energy consumption. The value of a run can be computed, for example, as the maximum, limit average, or discounted sum of transition weights. In multi-weighted automata, transitions carry several weights and can model, for example, the ratio between rewards and costs, or the efficiency of use of a primary resource under some upper bound constraint on a secondary resource. Here, we introduce a general model for multi-weighted automata as well as a multiweighted MSO logic. In our main results, we show that this multi-weighted MSO logic and multi-weighted automata are expressively equivalent both for finite and infinite words. The translation process is effective, leading to decidability results for our multi-weighted MSO logic.

cs.LO↗