Abstracts of Droste's Publications
Theoretical Computer Science - Theoretical Computer Science - Theoretical Computer Science - Theoretical Computer Science - Theoretical Computer Science - Theoretical


Skew and infinitary formal power series.
(
with D. Kuske), in: Automata Languages and Programming (30th ICALP, Eindhoven)
Lecture Notes in Computer Science 2719, 2003, pp. 426 - 438

Abstract.
We investigate finite-state systems with costs. Departing from the classical theory, in this paper the cost 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 costs. 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 $/omega$-rational formal power series. This generalizes a classical theorem of Büchi.


Automata with concurrency relations - a survey.
(
with D. Kuske), in: Advances in Logic, Artificial Intelligence and Robotics,
(eds. J. Abe, J. da Silva Filho), IOS Press, 2002, pp. 152 - 172; invited survey.
Abstract:
Automata with concurrency relations, which occured in the verification methods of concurrent programs, are labeled transition systems with state-dependent concurrency relations on the actions. They generalize the asynchronous transition systems and trace alphabets. Here we survey results obtained on such automata with connections to domain theory, Petri nets, graph-theoretic representations and algebraic and logical definability of languages.


A Kleene theorem for weighted tree automata.
(with H. Vogler), Theory of Computing Systems, to appear
.
Abstract.
In this paper we prove Kleene's result for tree series over a commutative and idempotent semiring A (which is not necessarily complete or continuous), i.e., the class of recognizable tree series over A and the class of rational tree series over A are equal. We show the result by direct automata-theoretic constructions and prove their correctness.


Rational transformations of formal power series
(with G.-Q. Zhang), in: Automata, Languages and Programming (28th ICALP, Crete),
Lecture Notes in Computer Science 2076, Springer 2001, 555 - 566.
Abstract.
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 rationality, generalizing the recent results of Zhang [15] to the formal power series setting. We show, for example, that the "square-root" operation, while preserving regularity for formal languages, preserves rationality for formal power series when the underlying semiring is commutative or locally finite, but not in general.


Continuous Petri nets and transition systems
(with R.M. Shortt), in:"Unifying Petri Nets" , (H. Ehrig, G. Juhas, J. Padberg, G. Rozenberg, eds.)
Lecture Notes in Computer Science 2128, Springer 2001, pp. 457 - 484; invited contribution.
Abstract.
In many systems, the values of finitely many parameters can be influenced in a continuous way by controls acting with possibly varying strength over intervals of time. For this, we present general models of continuous Petri nets and of continuous transition systems with situation-dependent concurrency. With a suitable concept of morphisms, we obtain a categorial adjunction between these two models, and often even a coreflection. This shows that the concept of regions is also applicable in this continuous setting. Finally, we prove that our categories of continuous Petri nets and of continuous automata with concurrency have products and conditional coproducts.


Recognizable languages in divisibility monoids
(with D. Kuske),  Mathem. Structures in Comp. Science 11 (2001), pp. 743 - 770.
Abstract.
We define the class of divisibility monoids which arise as quotients of the free monoid $\sum*$ modulo certain equations of the form ab=cd. These form a much larger class than free partially commutative monoids, and we show, under certain assumptions, that the recognizable  languages in these divisibility monoids coincide with c-rational languages. The proofs rely on Ramsey's theorem, distributive lattice theory and on Hashigushi's rank function generalized to these monoids. We obtain Ochmañski's theorem on recognizable languages in free partially commutative monoids as a consequence.


From Petri nets to automata with concurrency
(with  R.M. Shortt), Applied Categorical Structures 10 (2002), 173 - 191.
Abstract.
Automata with concurency relations are labelled transition systems with a collection of state-dependent binary independence relations for the actions. We show how to associate with each Petri net (place/transition net) such an automaton having the same dynamic behaviour. We characterize the automata arising in this way, and with suitable notions of morphisms for Petri nets and for automata with concurrency relations we extend this correspondence to a coreflection between the associated categories. As a consequence, we derive, that these categories have products and conditional oproducts.


Universal homogeneous graph-like structures and domains
(with P. Boldi and F. Cardone), Mathem. Structures in Comp. Science 12 (2002), 91 - 109.
Abstract.
We present explicit constructions of universal homogeneous objects in categories of domains with stable embedding-projection pairs as arrows. These results make use of a representation of such domains through graph-like structures and apply a generalization of Rado's result on the existence of the universal homogeneous countable graph. In particular, we build universal homogeneous objects in the categories of coherence spaces and qualitative domains, introduced by (Girard 1987; Girard 1986), and two categories of hypercoherences recently studied by (Ehrhard 1993). Our constructions reply upon basic numerical notions. We also show that a suitable random construction of Rado's graph and its generalizations produces with probability 1 the universal homogeneous structures presented here.


On aperiodic and star-free formal power series in partially commuting variables
(with P. Gastin), in: Formal Power Series and Algebraic Combinatorics (D. Krob, A.A. Mikhalev,
A.V. Mikhalev, eds.), 12th Int. Conf., Moscow, Springer 2000, pp. 158 - 169.
Abstract.
Formal power series over non-commuting variables have been investigated as representations of the behaviour of automata with multiplicities. Here we introduce and investigate the concepts of aperiodic and of star-free formal power series over semirings and partially commuting variables. We prove that if the semiring K is idempotent and commutative, or if K is idempotent and the variables are non-commuting, then the product of any two aperiodic series is again aperiodic. We also show that if K is idempotent and the matrix monoids over K have a Burnside property (satisfied, e.g. by tropical semiring), then the aperiodic and the star-free series coincide.


Asynchronous cellular automata for pomsets
(with P. Gastin and D. Kuske), Theoret. Comp. Science 247 (2000), 1 - 38 (fundamental study).
Abstract.
This paper extends to pomsets without auto-concurrency the fundamental notion of asynchronous 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 pomsets since there the class of recognizable pomset languages is not closed under complementation.


On recognizable languages in divisibility monoids
(with D. Kuske),  in: 12th Int. Symp. on Fundamentals of Computation Theory (FCT, Iasi)
Lecture Notes in Comp. Science, Springer 1684, 1999, pp. 246 - 257.
Abstract.
Kleene's theorem on recognizable languages in free monoids is considered to be of eminent importance in theoretical computer science. It has been generalized into various directions, including trace and rational monoids. Here, we investigate divisibility monoids which are defined by and capture algebraic properties sufficient to obtain a characterization of the recognizable languages by certain rational expressions as known from trace theory. The proofs rely on Ramsey's theorem, distributive lattice theory and on Hashigushi's rank function generalized to our divisibility  monoids. We obtain chmañski's theorem on recognizable languages in free partially commutative monoids as a consequence.


The Kleene-Schützenberger theorem for formal power series in partially commuting variables
(with P. Gastin), Information and Computation 153 (1999), 47 - 80.
Abstract.
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.


On recognizable and rational formal power series in partially commuting variables
(with P. Gastin), in: Automata, Languages and Programming (24th ICALP, Bologna).
Abstract.
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.


Recognizable and logically definable languages of finite computations in concurrent automata
(with  D. Kuske), Intern. J. of Foundations of Comp. Sc. 9 (1998), 295 - 313.
Abstract.
Automata with concurrency relations A, which occured in formal verification methods of concurrent programs, are labeled transition systems with a collection of binary relations describing when two actions in a given state of the automaton can happen 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. Then $M^{\infty}(A)$ denotes the set of all infinite products in M(A); its elements can be represented by labeled partially ordered sets. Under suitable assumptions on A, we show that a language L in $M^{\infty}(A)$ is recognizable iff it is definable by a formula of monadic second order logic, and that it is recognizable iff it can be constructed from recognizable languages in M(A) using co-rational expressions. This generalizes various recent results in trace theory.


Representation of computations in concurrent automata by dependence orders
(with F. Bracho and D. Kuske), Theoret. Comp. Science 174 (1997), 67 - 96.
Abstract.
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.


Asynchronous cellular automata for pomsets without auto-concurrency
(with P. Gastin), in: 7th Int. Conf. on Concurrency Theory (CONCUR, Pisa),
Lecture Notes in Comp. Science 1119, Springer, 1996, pp. 627 - 638.
Abstract.
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 Zielonka and we show how to construct a
deterministic ACA from an asynchronous mapping. Our main result generalizes Büchi's theorem for 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 owner write machine. More precisely, we prove the equivalence between non deterministic ACA, deterministic ACA and
monadic second order logic for this class of pomsets.


Trace languages definable with modular quantifiers
(with D. Kuske), in: Developments in Language Theory, 2nd int. Conf., Magdeburg,
World Scientific Publ., 1996, pp. 386 - 395.
Abstract.
We study an extension of first-order logic obtained by adjoining quantifiers that count with respect to an integer modulus. It is shown that the trace languages definable in the framework are precisely the regular trace languages whose syntactic monoids contain only solvable groups. Also, we consider the languages that are definable by sentences that contain only these modular quantifiers. Our results generalize corresponding results of Straubing, Thérien and Thomas on words.


Aperiodic languages in concurrency monoids
Information and Computation 126 (1996), 105 - 113.
Abstract.
Automata with concurrency relations A are labeled transition systems with a collection of binary relations indicating when two events, 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 characterization of the star-free languages of M(A). This generalizes a classical result of G. Guaiana, A. Restivo and S. Salemi in trace theory.


Languages and logical definability in concurrency monoids
(with D. Kuske), in "Computer Science Logic", Paderborn 1995,
Lecture Notes in Computer Science 1092, Springer, 1996, pp. 233 - 251.
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 ba labelled partially ordered sets. Under suitable assumptions on A, we show that a language L in M(A) is recorgnizable iff it is definable ba 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.


Dependence orders for computations of concurrent automata
(with F. Bracho and D. Kuske), in: STACS '95, Lecture Notes in Comp. Science 900,
Springer, 1995, pp. 467 - 478.
Abstract.
An automaton with concurrency relations A is a labeled transition systems with a collection of binary relations indicating when two events in a given state of the automaton can happen independently from 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.


Recognizable languages in concurrency monoids
Theoret. Comp. Science 150, 1995, 77 - 108.
Abstract.
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.


A Kleene theorem for recognizable languages over Concurrency monoids
in: Automata, Languages and Programming (21st ICALP, Jerusalem),
Lecture Notes in Comp. Science 820, Springer, 1994, pp. 388 - 399.
Abstract.
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 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.


Labelled domains and automata with concurrency
(with F. Bracho), Theoret. Comp. Science 135 (1994), 289 - 318.
Abstract.
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 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.


Petri nets and automata with concurrency relations - an adjunction
(with R. Shortt), in: "Semantics of programming Languages and Model Theory"
(M. Droste, Y. Gurevich, eds.), Gordon and Breach Science Publ., OPA (Amsterdam), 1993, 69 - 87.
Abstract.
We consider the category P of Petri nets with capacities (place/transition net) and also a category A of automata with a collection of binary concurrency relations indicating when two events, in a particular state of the automaton, commute. We construct an adjunction between the categories P and A. This generalizes a recent result of Winskel and Nielsen for condition/event-nets and asynchronous transition systems.


Universal domains and the amalgamation property
(with R. Göbel), Mathem. Structures in Comp. Science 3 (1993), 137 - 159.
Abstract.
In the theory of denotational semantics of programming languages, several authors have constructed various kinds of universal domains. We present here a categorical generalization of a well-known result in model theory, which we use to characterize large classes of reasonable categories that contain universal homogeneous objects. The existence uf such objects is characterized by the condition that the finite objects in the category satisfy the amalgamation property. We derive from this the existence and uniqueness of universal homogeneous domains for several categories of bifinite domains, with embedding-projection-pairs as morphisms. We also obtain universal homogeneous objects for various categories of stable bifinite domains. In contrast, several categories of event domains and concrete domains and the category of all coherent Scott-domains do not contain universal homogeneous objects. Finally, we show that all our constructions can be performed effectively.


Concurrent automata and domains
Intern. Journal of Foundations of Comp. Science 3 (1992), 389 - 418.
Abstract.
We introduce 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 symmetric binary relations which describe when two events at a particular state of A commute. This model generalizes the recent concept of Stark's trace automata. A permutation equivalence for computation sequences of A arises canonically, and we obtain a natural domain (D(A),<), comprising the induced equivalence classes. We give a complete order-theoretic characterization of all such partial orders (D(A),<), which turn out to be particular finitary domains. The arising domains (D(A),<) are particularly pleasant Scott-domains, if A is asumed to be concurrent, i.e. if the concurrency relations of A depend (in a natural way) locally on each other, but not necessarily globally. We show that both event domains and dI-domains arise, up to isomorphism, as domains (D(A),<) with well-behaved such concurrent automata A.  We introduce a subautomaton relationship for concurrent automata and show that, given two concurrency domains (D,<), (D',<), there exists a nice stable embedding-projection pair  from D to D' iff D, D' can be generated by concurrent automata A, A' such that A is a subautomaton of A'. Finally, we introduce the concept of locally finite concurrent automata and show that there exists a universal homogeneous locally finite concurrent automaton, which is unique up to isomorphism.


Finite axiomatizations for universal domains
J. of Logic and Computation 2 (1992), 119 - 131
Abstract.
In the theory of denotional semantics of programming languages, several authors established the existence of particular kinds of universal domains. Here we consider the categories of all $\omega$-bifinite domains, all $\omega$-bifinite L-domains, all $\omega$-Scott-domains, and all $\omega$-algebraic lattices, respectively, in each case with embedding-projection pairs as morphisms. It has been shown that each of these categories contains a universal homogeneous, or saturated, object, which is unique up to isomorphism. Here we introduce for each of these four categories C a set of finite axioms $S_C$, formulated in a first-order language of predicate calculus for posets, and show that an arbitrary domain $(D,\leq)\in C$ is the universal homogeneous object in C if and only if its subset of compact elements satisfies all axioms in $S_C$.


Universal information systems
(with R. Göbel), Intern. J. of Foundations of Comp. Science 1(1991). 413 - 424.
Abstract.
In the theory of denotional semantics of programming languages, several authors proved the existence of particular kinds of universal domains. D. Scott constructed universal information systems, which are, however, not unique up to isomorphism. Here, we use a model-theoretic technique to establish the existence and uniqueness of a universal homogeneous information system. Similar results are also obtained for canonical and for stable information systems, respectively.


Universal homogeneous event structures and domains
Information and Computation 94 (1991), 48 - 61.
Abstract.
In the theory of denotional 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.


Concurrency, automata and domains
in: Automata, Languages and Programming (17th ICALP, Warwick),
Lecture Notes in Comp. Science 443, Springer, 1990, 195 - 208.
Abstract.
We introduce 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 symmetric binary relations which describe when two events at a particular state of A commute; we assume that these concurrency relations depend (in a natural way) locally on each other, but not globally. This model generalizes the recent concept of Stark's trace automata. A permutation equivalence for computation sequences of A arises canonically, and we obtain a natural domain (D(A),<), comprising the induced equivalence classes. We give a complete order-theoretic characterization of all such concurrency domains (D(A),<), which turn out to be particular finitary Scott-domains. We also show that dI-domains arise, up to isomorphism, as domains (D(A),<) with
particularly well-behaved concurrent automata A.


Non-deterministic information systems and their domains
(with R. Göbel), Theoret. Comp. Sci. 75 (1990), 289 - 309.
Abstract.
In the theory of denotional 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.


Recursive domain equations for concrete data structures
Information and Computation 82 (1989), 65 - 80.
Abstract.
In the theory of denotional 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.


Event structures and domains
Theoret. Comp. Sci. 68 (1989), 37 - 47.
Abstract.
In the theory of denotional 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.



last modified February 4, 2003, Gudrun Seidel