Manfred Droste

I&C Journal 2026 Journal Article

Descriptive complexity and weighted Turing machines

• Guillermo Badia
• Manfred Droste
• Carles Noguera
• Erik Paul

Fagin’s seminal result characterizing 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 NP [ S ], L [ S ], FP [ S ], FPLOG [ S ], FPSPACE [ S ], and FPSPACE p o l y [ S ] in terms of definability in suitable weighted logics for an arbitrary semiring S. In particular, we state and 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 P ) and the Abiteboul–Vianu–Vardi’s theorem (originally for PSPACE ). We also discuss a recent open problem proposed by Eiter and Kiesel. Recently, the above mentioned weighted complexity classes have been investigated in connection to classical counting complexity classes. Furthermore, several classical counting complexity classes have been characterized in terms of particular weighted logics over the semiring N of natural numbers. In this work, we cover several of these classes and obtain new results for others such as NPMV, ⊕ P, or the collection of real-valued languages realized by nondeterministic polynomial-time real-valued Turing machines. Furthermore, our results apply to classes based on many other important semirings, such as the max-plus and the min-plus semirings over the natural numbers which correspond to the classical classes MaxP [ O ( log n ) ] and MinP [ O ( log n ) ], respectively.

MFCS Conference 2024 Conference Paper

Logical Characterizations of Weighted Complexity Classes

• Guillermo Badia
• Manfred Droste
• Carles Noguera
• Erik Paul

Fagin’s seminal result characterizing 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 NP[𝒮], FP[𝒮], FPLOG[𝒮], FPSPACE[𝒮], and FPSPACE_poly[𝒮] in terms of definability in suitable weighted logics for an arbitrary semiring 𝒮. 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 𝖯) and the Abiteboul-Vianu-Vardi’s theorem (originally for PSPACE). We also discuss a recent open problem proposed by Eiter and Kiesel. Recently, the above mentioned weighted complexity classes have been investigated in connection to classical counting complexity classes. Furthermore, several classical counting complexity classes have been characterized in terms of particular weighted logics over the semiring ℕ of natural numbers. In this work, we cover several of these classes and obtain new results for others such as NPMV, ⊕𝖯, or the collection of real-valued languages realized by polynomial-time real-valued nondeterministic Turing machines. Furthermore, our results apply to classes based on many other important semirings, such as the max-plus and the min-plus semirings over the natural numbers which correspond to the classical classes MaxP[O(log n)] and MinP[O(log n)], respectively.

TCS Journal 2024 Journal Article

Undecidability of the universal support problem for weighted automata over zero-sum-free commutative semirings

• Manfred Droste
• Werner Kuich

We show that there is an effectively given zero-sum-free commutative semiring S, contained as the subsemiring of nonnegative elements in an effectively given commutative ordered ring, for which there are no procedures deciding, given a weighted finite automaton over S, whether its support is the language of all words or whether its support is infinite. In particular, by a result of D. Kirsten (2011), since S is zero-sum-free and commutative, the support is recognizable by a classical finite automaton, but such an automaton or even just a pushdown automaton for its support cannot be constructed effectively.

TCS Journal 2022 Journal Article

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

• Manfred Droste
• Zoltán Fülöp
• Dávid Kószó
• Heiko Vogler

We consider weighted tree automata over strong bimonoids (for short: wta). A wta A has the finite-image property if its recognized weighted tree language 〚 A 〛 has finite image; moreover, A has the preimage property if the preimage under 〚 A 〛 of each element of the underlying strong bimonoid is a recognizable tree language. For each wta A over a past-finite monotonic strong bimonoid we prove the following results. In terms of 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 A it is decidable whether 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 A has the preimage property. All our results also hold for weighted string automata.

I&C Journal 2022 Journal Article

Greibach normal form for ω-algebraic systems and weighted simple ω-pushdown automata

• Manfred Droste
• Sven Dziadek
• Werner Kuich

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 ω-context-free languages (as introduced by Cohen and Gold in 1977) and an extension of weighted context-free languages of finite words (that were already investigated by Chomsky and Schützenberger in 1963). As in the theory of formal grammars, these weighted context-free languages, or ω-algebraic series, can be represented as solutions of mixed ω-algebraic systems of equations and by weighted ω-pushdown automata. In our first main result, we show that (mixed) ω-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-reset automata do not use ϵ-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.

I&C Journal 2022 Journal Article

Logic for ω-pushdown automata

• Manfred Droste
• Sven Dziadek
• Werner Kuich

Context-free languages of infinite words have recently found increasing interest. Here, we will present a second-order logic with the same expressive power as Büchi or Muller pushdown automata for infinite words. This extends fundamental logical characterizations of Büchi, Elgot, Trakhtenbrot for regular languages of finite and infinite words and a more recent logical characterization of Lautemann, Schwentick and Thérien for context-free languages of finite words to ω-context-free languages. For our argument, we will investigate Greibach normal forms of ω-context-free grammars as well as a new type of Büchi pushdown automata which can alter their stack by at most one element and without ϵ-transitions. We show that they suffice to accept all ω-context-free languages. This enables us to use similar results recently developed for infinite nested words.

I&C Journal 2022 Journal Article

Weighted operator precedence languages

• Manfred Droste
• Stefan Dück
• Dino Mandrioli
• Matteo Pradella

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 by the original grammar family, in terms of an automata family (OPA) and an MSO logic; furthermore they significantly generalize the well-known visibly pushdown languages (VPL). A different area of research investigates quantitative evaluations of formal languages by adding weights to strings. 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üchi-like theorem, we show that weighted OPA are expressively equivalent to a weighted MSO-logic for OPL.

I&C Journal 2020 Journal Article

McCarthy-Kleene fuzzy automata and MSO logics

• Manfred Droste
• Temur Kutsia
• George Rahonis
• Wolfgang Schreiner

We introduce McCarthy-Kleene fuzzy automata (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üchi type theorem.

I&C Journal 2019 Journal Article

A Kleene theorem for weighted tree automata over tree valuation monoids

• Doreen Götze
• Zoltán Fülöp
• Manfred Droste

We investigate weighted tree automata over Cauchy tree valuation monoids, a new type of weight structure which includes all commutative semirings and, in addition, average and discounted computations of weights for trees. We define rational tree series over these weight structures, and we prove Kleene's classical theorem for this setting: a tree series over a Cauchy tree valuation monoid is recognizable by a weighted tree automaton if and only if it is rational. The proof works via direct automata-theoretic constructions. Along the way, our results yield a new characterization of weighted tree automata over commutative semirings by rational expressions.

MFCS Conference 2019 Conference Paper

Aperiodic Weighted Automata and Weighted First-Order Logic

• Manfred Droste
• Paul Gastin

By fundamental results of Schützenberger, 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.

TCS Journal 2019 Journal Article

Preface

• Manfred Droste
• Ilias Kotsireas
• Robert Rolland

I&C Journal 2019 Journal Article

Weighted automata with storage

• Luisa Herrmann
• Heiko Vogler
• Manfred Droste

We consider finite-state automata that are equipped with a storage. Moreover, the transitions are weighted by elements of a unital valuation monoid. A weighted automaton with storage recognizes a weighted language, which is a mapping from input strings to elements of the carrier set of the unital valuation monoid. For the class of weighted languages recognizable by such automata we prove closure properties, a Chomsky-Schützenberger theorem, and a Büchi-Elgot-Trakhtenbrot theorem. In case of idempotent, locally finite, and sequential unital valuation monoids, the recognized weighted languages are step functions.

TCS Journal 2019 Journal Article

Weighted simple reset pushdown automata

• Manfred Droste
• Sven Dziadek
• Werner Kuich

We define a new normal form for weighted pushdown automata. The new type of automaton uses a stack but has only limited access to it. Only three stack commands are available: popping a symbol, pushing a symbol or leaving the stack unaltered. Additionally, ϵ-transitions are not used. We prove that this automaton model can recognize all weighted context-free languages (i. e. , generates all algebraic power series).

MFCS Conference 2018 Conference Paper

A Feferman-Vaught Decomposition Theorem for Weighted MSO Logic

• Manfred Droste
• Erik Paul

We prove a weighted Feferman-Vaught decomposition theorem for disjoint unions and products of finite structures. The classical Feferman-Vaught Theorem describes how the evaluation of a first order sentence in a generalized product of relational structures can be reduced to the evaluation of sentences in the contributing structures and the index structure. The logic we employ for our weighted extension is based on the weighted MSO logic introduced by Droste and Gastin to obtain a Büchi-type result for weighted automata. We show that for disjoint unions and products of structures, the evaluation of formulas from two respective fragments of the logic can be reduced to the evaluation of formulas in the contributing structures. We also prove that the respective restrictions are necessary. Surprisingly, for the case of disjoint unions, the fragment is the same as the one used in the Büchi-type result of weighted automata. In fact, even the formulas used to show that the respective restrictions are necessary are the same in both cases. However, here proving that they do not allow for a Feferman-Vaught-like decomposition is more complex and employs Ramsey's Theorem. We also show how translation schemes can be applied to go beyond disjoint unions and products.

TCS Journal 2018 Journal Article

Weighted register automata and weighted logic on data words

• Parvaneh Babari
• Manfred Droste
• Vitaly Perevoshchikov

Data words are sequences of pairs where the first element is taken from a finite alphabet and the second element is taken from an infinite data domain. Register automata provide a widely studied model for reasoning on data words. In this paper, we investigate automata models for quantitative aspects of systems with infinite data domains, e. g. , the costs of storing data on a remote server or the consumption of resources (e. g. , memory, energy, time) during a data analysis. We introduce weighted register automata on data words over commutative data semirings equipped with a collection of binary data functions, and we investigate their closure properties. Unlike the other models considered in the literature, we allow data comparison by means of an arbitrary collection of binary data relations. This enables us to incorporate timed automata and weighted timed automata into our framework. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic; for the proof we employ a new class of determinizable visibly register automata.

GandALF Workshop 2017 Workshop Paper

MK-fuzzy Automata and MSO Logics

• Manfred Droste
• Temur Kutsia
• George Rahonis
• Wolfgang Schreiner

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üchi type theorem.

I&C Journal 2017 Journal Article

Weighted automata and logics for infinite nested words

• Manfred Droste
• Stefan Dück

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üchi'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.

MFCS Conference 2017 Conference Paper

Weighted Operator Precedence Languages

• Manfred Droste
• Stefan Dück
• Dino Mandrioli
• Matteo Pradella

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 (OPA) 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üchi-like theorem, we show that weighted OPA are expressively equivalent to a weighted MSO-logic for OPL.

GandALF Workshop 2016 Workshop Paper

Weighted Linear Dynamic Logic

• Manfred Droste
• George Rahonis

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ützenberger 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.

TCS Journal 2014 Journal Article

Preface

• Manfred Droste
• Heiko Vogler

TCS Journal 2013 Journal Article

Weighted finite automata over hemirings

• Manfred Droste
• Werner Kuich

Quantitative automata computing the maximal average consumption of resources are currently intensively investigated. We introduce Conway hemirings and show that a few equational axioms suffice to imply a Kleene theorem for the possible behaviors of quantitative automata characterizing them as rational series, and we derive several further natural identities for rational operations on such series. We also obtain a more abstract Kleene theorem for Conway hemiring automata. This extends classical results of Conway and Schützenberger for recognizable languages resp. semiring-weighted automata.

TCS Journal 2012 Journal Article

Weighted automata and multi-valued logics over arbitrary bounded lattices

• Manfred Droste
• Heiko Vogler

We show that L -weighted automata, L -rational series, and L -valued monadic second order logic have the same expressive power, for any bounded lattice L and for finite and infinite words. We also prove that aperiodicity, star-freeness, and L -valued first-order and LTL-definability coincide. This extends classical results of Kleene, Büchi–Elgot–Trakhtenbrot, and others to arbitrary bounded lattices, without any distributivity assumption that is fundamental in the theory of weighted automata over semirings. In fact, we obtain these results for large classes of strong bimonoids which properly contain all bounded lattices.

I&C Journal 2012 Journal Article

Weighted automata and weighted MSO logics for average and long-time behaviors

• Manfred Droste
• Ingmar Meinecke

Weighted automata model quantitative aspects of systems like memory or power consumption. Recently, Chatterjee, Doyen, and Henzinger introduced a new kind of weighted automata which compute objectives like the average cost or the long-time peak power consumption. In these automata, operations like average, limit superior, limit inferior, limit average, or discounting are used to assign values to finite or infinite words. In general, these weighted automata are not semiring weighted anymore. Here, we establish a connection between such new kinds of weighted automata and weighted logics. We show that suitable weighted MSO logics and these new weighted automata are expressively equivalent, both for finite and infinite words. The constructions employed are effective, leading to decidability results for the weighted logic formulas considered.

TCS Journal 2011 Journal Article

A Kleene–Schützenberger theorem for weighted timed automata

• Manfred Droste
• Karin Quaas

During the last years, weighted timed automata have received much interest in the real-time community. Weighted timed automata form an extension of timed automata and allow us to assign weights (costs) to both locations and edges. This model, introduced by Alur et al. (2001) and Behrmann et al. (2001), permits the treatment of continuous consumption of resources and has led to much research on scheduling problems, optimal reachability and model checking. Also, several authors have derived Kleene-type characterizations of (unweighted) timed automata and their accepted timed languages. The goal of this paper is to provide a characterization of the behaviours of weighted timed automata by rational power series. We define weighted timed automata with weights taken in an arbitrary semiring, resulting in a model that subsumes several weighted timed automata concepts of the literature. For our main result, we combine the methods of Schützenberger, a recent approach for a Kleene-type theorem for unweighted timed automata by Bouyer and Petit as well as new techniques. Our main result also implies Kleene-type theorems for several subclasses of weighted timed automata investigated before, e. g. , for timed automata and timed automata with stopwatch observers.

MFCS Conference 2010 Conference Paper

Describing Average- and Longtime-Behavior by Weighted MSO Logics

• Manfred Droste
• Ingmar Meinecke

Abstract Weighted automata model quantitative aspects of systems like memory or power consumption. Recently, Chatterjee, Doyen, and Henzinger introduced a new kind of weighted automata which compute objectives like the average cost or the longtime peak power consumption. In these automata, operations like average, limit superior, limit inferior, limit average, or discounting are used to assign values to finite or infinite words. In general, these weighted automata are not semiring weighted anymore. Here, we establish a connection between such new kinds of weighted automata and weighted logics. We show that suitable weighted MSO logics and these new weighted automata are expressively equivalent, both for finite and infinite words. The constructions employed are effective, leading to decidability results for the weighted logic formulas considered.

TCS Journal 2009 Journal Article

Weighted automata and weighted logics with discounting

• Manfred Droste
• George Rahonis

We introduce a weighted logic with discounting and we establish the Büchi–Elgot theorem for weighted automata over finite words and arbitrary commutative semirings. Then we investigate Büchi and Muller automata with discounting over the max-plus and the min-plus semiring. We show their expressive equivalence with weighted MSO-sentences with discounting. In this case our logic has a purely syntactic definition. For the finite case, we obtain a purely syntactically defined weighted logic if the underlying semiring is additively locally finite.

TCS Journal 2007 Journal Article

Weighted automata and weighted logics

• Manfred Droste
• Paul Gastin

Weighted automata are used to describe quantitative properties in various areas such as probabilistic systems, image compression, speech-to-text processing. The behaviour of such an automaton is a mapping, called a formal power series, assigning to each word a weight in some semiring. We generalize Büchi’s and Elgot’s fundamental theorems to this quantitative setting. We introduce a weighted version of MSO logic and prove that, for commutative semirings, the behaviours of weighted automata are precisely the formal power series definable with particular sentences of our weighted logic. We also consider weighted first-order logic and show that aperiodic series coincide with the first-order definable ones, if the semiring is locally finite, commutative and has some aperiodicity property.

TCS Journal 2006 Journal Article

Skew and infinitary formal power series

• Manfred Droste
• Dietrich Kuske

We investigate finite-state systems with weights. Departing from the classical theory, in this paper the weight of an action does not only depend on the state of the system, but also on the time when it is executed; this reflects the usual human evaluation practices in which later events are considered less urgent and carry less weight than close events. We first characterize the terminating behaviors of such systems in terms of rational formal power series. This generalizes a classical result of Schützenberger. Secondly, we deal with nonterminating behaviors and their weights. This includes an extension of the Büchi-acceptance condition from finite automata to weighted automata and provides a characterization of these nonterminating behaviors in terms of ω -rational formal power series. This generalizes a classical theorem of Büchi.

TCS Journal 2006 Journal Article

Weighted tree automata and weighted logics

• Manfred Droste
• Heiko Vogler

We define a weighted monadic second order logic for trees where the weights are taken from a commutative semiring. We prove that a restricted version of this logic characterizes the class of formal tree series which are accepted by weighted bottom-up finite state tree automata. The restriction on the logic can be dropped if additionally the semiring is locally finite. This generalizes corresponding classical results of Thatcher, Wright, and Doner for tree languages and it extends recent results of Droste and Gastin [Weighted automata and weighted logics, in: Automata, Languages and Programming—32nd International Colloquium, ICALP 2005, Lisbon, Portugal, 2005, Proceedings, Lecture Notes in Computer Science, Vol. 3580, Springer, Berlin, 2005, pp. 513–525, full version in Theoretical Computer Science, to appear. ] from formal power series on words to formal tree series.

I&C Journal 2003 Journal Article

On transformations of formal power series

• Manfred Droste
• Guo-Qiang Zhang

Formal power series are an extension of formal languages. Recognizable formal power series can be captured by the so-called weighted finite automata, generalizing finite state machines. In this paper, motivated by codings of formal languages, we introduce and investigate two types of transformations for formal power series. We characterize when these transformations preserve recognizability, generalizing the recent results of Zhang [16] to the formal power series setting. We show, for example, that the “square-root” operation, while preserving regularity for formal languages, preserves recognizability for formal power series when the underlying semiring is commutative or locally finite, but not in general.

TCS Journal 2000 Journal Article

Asynchronous cellular automata for pomsets

• Manfred Droste
• Paul Gastin
• Dietrich Kuske

This paper extends to pomsets without auto-concurrency the fundamental notion of asynchronous cellular automata (ACA) which was originally introduced for traces by Zielonka. We generalize to pomsets the notion of asynchronous mapping introduced by Cori, Métivier and Zielonka and we show how to construct a deterministic ACA~from an asynchronous mapping. Then we investigate the relation between the expressiveness of monadic second-order logic, nondeterministic ACAs and deterministic ACAs. We can generalize Büchi's theorem for finite words to a class of pomsets without auto-concurrency which satisfy a natural axiom. This axiom ensures that an asynchronous cellular automaton works on the pomset as a concurrent read and exclusive owner write machine. More precisely, in this class nondeterministic ACAs, deterministic ACAs and monadic second-order logic have the same expressive power. Then we consider a class where deterministic ACAs are strictly weaker than nondeterministic ones. But in this class nondeterministic ACAs still capture monadic second-order logic. Finally, it is shown that even this equivalence does not hold in the class of all pomsets since there the class of recognizable pomset languages is not closed under complementation.

I&C Journal 1999 Journal Article

The Kleene–Schützenberger Theorem for Formal Power Series in Partially Commuting Variables

• Manfred Droste
• Paul Gastin

Kleene's theorem on the coincidence of regular and rational languages in free monoids has been generalized by Schützenberger to a description of the recognizable formal power series in noncommuting variables over arbitrary semirings and by Ochmański to a characterization of the recognizable languages in trace monoids. We will describe the recognizable formal power series over arbitrary semirings and in partially commuting variables, i. e. over trace monoids. We prove that the recognizable series are certain rational power series, which can be constructed from the polynomials by using the operations sum, product, and a restricted star which is applied only to series for which the elements in the support all have the same connected alphabet. The converse is true if the underlying semiring is commutative. Moreover, if in addition the semiring is idempotent then the same result holds with a star restricted to series for which the elements in the support have connected (possibly different) alphabets. It is shown that these assumptions over the semiring are necessary. This provides a joint generalization of Kleene's, Schützenberger's and Ochmański's theorems.

TCS Journal 1997 Journal Article

Representation of computations in concurrent automata by dependence orders

• Felipe Bracho
• Manfred Droste
• Dietrich Kuske

An automaton with concurrency relations A is a labelled transition system with a collection of binary relations indicating when two actions in a given state of the automaton can occur independently of each other. The concurrency relations induce a natural equivalence relation for finite computation sequences. We investigate two graph-theoretic representations of the equivalence classes of computation sequences and obtain that under suitable assumptions on A they are isomorphic. Furthermore, the graphs are shown to carry a monoid operation reflecting precisely the composition of computations. This generalizes fundamental graph-theoretical representation results due to Mazurkiewicz in trace theory.

I&C Journal 1996 Journal Article

Aperiodic Languages in Concurrency Monoids

• Manfred Droste

Automata with concurrency relations A are labelled transition systems with a collection of binary relations indicating when two events, in a given state of the automaton, are concurrent. We investigate concurrency monoidsM( A ) comprising all finite computation sequences of A, modulo a canonical congruence induced by the concurrency relations, with composition as monoid operation. Under suitable assumptions on A we obtain a characterization of the star- free languages ofM( A ). This generalizes a classical result of M. P. Schützenberger and a result of G. Guaiana, A. Restivo and S. Salemi in trace theory.

CSL Conference 1996 Conference Paper

Languages and Logical Definability in Concurrency Monoids

• Manfred Droste
• Dietrich Kuske

Abstract Automata with concurrency relations A are labeled transition systems with a collection of binary relations describing when two actions in a given state of the automaton can occur independently of each other. The concurrency monoid M ( A ) comprises all finite computation sequences of A, modulo a canonical congruence induced by the concurrency relations, with composition as monoid operation; its elements can be represented by labeled partially ordered sets. Under suitable assumptions on A, we show that a language L in M( A ) is recognizable iff it is definable by a formula of monadic second order logic. We also investigate the relationship between aperiodic and first-order definable languages in M( A ). This generalizes various recent results in trace theory.

TCS Journal 1995 Journal Article

Recognizable languages in concurrency monoids

• Manfred Droste

Automata with concurrency relations A are labelled transition systems with a collection of binary relations indicating when two actions, in a given state of the automaton, are concurrent. We investigate concurrency monoids M( A ) comprising all finite computation sequences of A, modulo a canonical congruence induced by the concurrency relations, with composition as monoid operation. Under suitable assumptions on A we obtain a Kleene-type characterization of the recognizable languages of M( A ). This generalizes results of Cori, Métivier, Perrin and Ochmanski in trace theory.

TCS Journal 1994 Journal Article

Labelled domains and automata with concurrency

• Felipe Bracho
• Manfred Droste

We investigate an operational model of concurrent systems, called automata with concurrency relations. These are labelled transition systems A in which the event set is endowed with a collection of binary concurrency relations which indicate when two events, in a particular state of the automaton, commute. This model generalizes asynchronous transition systems, and as in trace theory we obtain, through a permutation equivalence for computation sequences of A, an induced domain (D( A ), ⩽). Here, we construct a categorical equivalence between a large category of (“cancellative”) automata with concurrency relations and the associated domains. We show that each cancellative automaton can be reduced to a minimal cancellative automaton generating, up to isomorphism, the same domain. Furthermore, when fixing the event set, this minimal automaton is unique.

TCS Journal 1993 Journal Article

On stable domains

• Manfred Droste

In denotational semantics of programming languages, various categories of domains, with continuous functions as morphisms, and their closure properties under operations like taking products or function space have been intensively studied. However, classes of domains which, like bifinite domains, are also closed under the Plotkin powerdomain operation are rare. Here we investigate stable domains. They naturally generalize the concept of dI-domains studied by Berry and others and satisfy a strong finiteness condition for compact elements, but in general no distributivity assumption. These classes recently were shown (in joint work with R. Göbel) to contain universal objects. We first derive an order-theoretic characterization of stability and then show that the class of all stable domains is closed under countable cartesian products, stable function space and the Plotkin powerdomain operation. As a consequence, we also obtain that the categories of all stable L-domains and of all distributive stable L-domains, with stable functions as morphisms, are cartesian-closed.

I&C Journal 1991 Journal Article

Universal homogeneous event structures and domains

• Manfred Droste

In the theory of denotational semantics of programming languages, several authors established the existence of particular kinds of “universal” domains. Here, we use a general model-theoretic result to show that there exists a unique countable universal homogeneous event structure. From this, we deduce that the category of all event domains, with stable embedding-projection pairs as morphisms, contains a universal object. Similarly, we also obtain a universal dI-domain. We also show that the category of all event domains is closed under inverse limits. Similar results are derived for Kahn and Plotkin's concrete data structures and concrete domains.

CSL Conference 1990 Conference Paper

Effectively Given Information Systems and Domains

• Manfred Droste
• Rüdiger Göbel

TCS Journal 1990 Journal Article

Non-deterministic information systems and their domains

• Manfred Droste
• Rüdiger Göbel

In the theory of denotational semantics of programming languages Dedekind-complete, algebraic partial orders (domains) frequently have been considered since Scott's and Strachey's fundamental work in 1971 (Stoy, 1977). As Scott (1982) showed, these domains can be represented canonically by (deterministic) information systems. However, recently, more complicated constructions (such as power domains) have led to more general domains (Plotkin, 1976; Smyth and Plotkin, 1977; Smyth, 1983). We introduce non-deterministic information systems and establish the representation theorem similar to Scott (1982) for these more general domains. This result will be the basis for solving recursive domain equations.

TCS Journal 1989 Journal Article

Event structures and domains

• Manfred Droste

In the theory of denotational semantics, we study event structures which generalize Kahn and Plotkin's concrete data structures and which model computational processes. With each event structure we associate canonically an event domain (a particular algebraic complete partial order), and conversely we derive a representation result for event domains. For a particular class of event structures, the canonical event structures, we obtain that any two canonical event structures are isomorphic iff they have order-isomorphic canonical domains.

I&C Journal 1989 Journal Article

Recursive domain equations for concrete data structures

• Manfred Droste

In the theory of denotational semantics of programming languages, we study event structures which combine features of Scott's information systems and Kahn and Plotkin's concrete data structures and model computational processes. We show that a simple approximation concept for event structures allows us to obtain straightforward solutions of recursive domain equations for event domains. From this, we derive a generalization of corresponding theorems of Kahn and Plotkin respectively Berry and Curien for concrete data structures and concrete domains.