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


Weighted automata
(with D. Kuske), chapter 4 (invited) in Handbook: "Automata: from Mathematics to Applications" (J.-E. Pin, ed.), European Mathematical Society, to appear.
Abstract.
Weighted automata are classical finite automata in which the transitions carry weights. These weights may model quantitative properties like the amount of resources needed for executing a transition or the probability or reliability of its successful execution. Using weighted automata, we may also count the number of successful paths labeled by a given word.
As an introduction into this field, we present selected classical and recent results concentrating on the expressive power of weighted automata.


Weighted tree automata over valuation monoids and their characterizations by weighted logics
(with D. Götze, S. Märcker, I. Meinecke), in: Algebraic Foundations in Computer Science (eds. W. Kuich, G. Rahonis), Lecture Notes in Computer Sciences, vol. 7020, Springer, 2011, pp. 30-55.
Abstract.
Quantitative aspects of systems can be modeled by weighted automata. Here, we deal with such automata running on finite trees. Usually, transitions are weighted with elements of a semiring and the behavior of the automaton is obtained by multiplying the weights along a run. We turn to a more general cost model: the weight of a run is now determined by a global valuation function. An example of such a valuation function is the average of the weights. We establish a characterization of the behaviors of these weighted finite tree automata by fragments of weighted monadic second-order logic. For bi-locally finite bimonoids, we show that weighted tree automata capture the expressive power of several semantics of full weighted MSO logic. Decision procedures follow as consequences.


A Cascade Decomposition of Weighted Finite Transition Systems
(with I. Meinecke, B. Seselja, A. Tepavcevic), Coverings and decompositions of semiring-weighted finite transition systems, in: Fuzzy emirings with Applications to Automata Theory (by J. Ahsan, J. Mordeson, M. Shabir), chapter 11 (invited), Springer, 2012
Abstract.
We consider weighted finite transition systems (wts) with weights from commutative naturally ordered semirings. Such semirings comprise distributive lattices as well as the natural numbers with ordinary addition and multiplication, and the max-plus-semiring. For these systems we explore the concepts of covering and cascade product. We show a cascade decomposition result for such wts using special partitions of the state set of the system. This extends a classical result of automata theory to the weighted setting.


Weighted Finite Automata over Strong Bimonoids
(with T.Stüber, H.Vogler), Information Sciences, Information Sciences 180 (2010), 156-166.
Abstract.
We investigate weighted finite automata over strings and strong bimonoids. Such algebraic structures satisfy the same laws as semirings except that no distributivity laws need to hold. We define two different behaviors and prove precise characterizations for them if the underlying strong bimonoid satisfies local finiteness conditions. Moreover, we show that in this case the given weighted automata can be determinized.


A Kleene-Schützenberger Theorem for Weighted Timed Automata
(with K.Quaas), in: 11th Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS), Lecture Notes in Comp. Science vol. 4962, Springer 2008, pp. 142-156.
Abstract.
During the last years, weighted timed automata (WTA) 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 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 possible behaviours of WTA by rational power series. We define WTA with weights taken in an arbitrary semiring, resulting in a model that subsumes several WTA 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 WTA investigated before, e.g., for weighted finite automata, timed automata and timed automata with stopwatch observers.


Random event structures
(with G.-Q. Zhang), International Journal of Software and Informatics 2 (2008), 77-88.

Abstract.
In a line of recent development, probabilistic constructions of universal, homogeneous objects have been provided in various categories of ordered structures, such as causal sets [11], bifinite domains [12], and countable partial orders [9]. These constructions have been shown to produce objects with the desired properties with probability 1 in an appropriately defined measure space. A common strategy for these constructions is successive point-wise extension of an existing finite structure, with decisions on the relationships between the newly added point and the existing structure made according to well-specified probabilistic choices. This strategy is a departure from (and understandably so due to the increased complexity) the original one for random graphs [15] where a universal homogeneous countable graph is constructed with probability 1 in a single step (i.e., a single round of countably many probabilistic choices made independently). It would be interesting to see which of the categories studied more recently may admit such "one-step" constructions. The main focus of this paper is a new strategy, consisting of a single round of countably many probabilistic choices made independently, for the construction of a universal, homogeneous prime event structure. Such a construction not only simplifies the process (and the associated proofs), but also may reveal additional insights on the properties about universal homogeneous random prime event structures, including causal sets and the corresponding dI-domains.


Multi-valued MSO logics over words and trees
(with W.Kuich, G.Rahonis), Fundamenta Informaticae 84 (2008), 305-327.

Abstract.
We introduce multi-valued Büchi and Muller automata over distributive lattices and a multi-valued MSO logic for infinite words. For this logic, we prove the expressive equivalence of ω-recognizable and MSO-definable infinitary formal Power series over distributive lattices with negation function. Then we consider multi-valued Muller tree automata and a multi-valued MSO logics for trees over distributive lattices. For this logic, we establish a version of Rabin's theorem for infinitary tree series.


Almost every domain universal
(with D.Kuske)
MFPS 2007, Electronic Notes in Theoretical Computer Science vol. 173, 103-119 (2007).
Abstract.
We endow the collection of ω-bifinite domains with the structure of a probability space, and we will show that in this space the collection of all universal domains has measure 1. For this, we present a probabilistic way to extend a finite partial order by one element. Applying this procedure iteratively, we obtain an infinite partial order. We show that, with probability~1, the cpo-completion of this infinite partial order is the universal homogeneous ω-bifinite domain. By alternating the probabilistic one-point extension with completion procedures we obtain almost surely the universal and homogeneous ω-algebraic lattice, ω-Scott domain, and ω-bifinite L-domain, respectively. We also show that in the projective topology, the set of universal and homogeneous ω-bifinite domains is residual (i.e., comeagre), and we present an explicit number-theoretic construction of such a domain.


Skew and infinitary formal power series
(with D.Kuske)

Theoretical Computer Science 366 (2006), 199-227.
Abstract.
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 ωomega-rational formal power series. This generalizes a classical theorem of Büchi.


Weighted automata and weighted logics with discounting
(with G.Rahonis)

12th Int. Conf. on Implementation and Application of Automata (CIAA), Lecture Notes in Comp. Science vol. 4783, 2007, pp. 73-84.
Abstract.
We introduce a weighted logic with discounting and we etablish Büchi's and Elgot's 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.


Weighted automata and weighted logics on infinite words
(with G.Rahonis)

Izvestiya VUZ. Matematika 54 (2010), 26-45.
Abstract.
We introduce weighted automata over infinite words with Muller acceptance condition and we show that their behaviors coincide with the semantics of weigthed restrict MSO-sentences. Furthermore, we establish an equivalence property of weighted Muller and weighted Büchi automata over certain semirings.


Bifinite Chu spaces
(with Guo-Quiang Zhang)
in: 2nd Conf. on Algebra and Coalgebra in Computer Science (CALCO), Lecture Notes in Comp. Science vol. 4624, Springer, 2007, pp. 179-193.
Abstract.
This paper studies colimits of sequences of finite Chu spaces and their ramifications. We consider three bases categories of Chu spaces: the generic Chuspaces (C), the extensional Ch spaces (E), and the biextensional Chu spaces (B). The main results are: (1) a characterization of monics in each of the three categories; (2) existence (or the lack thereof) of colimits and a characterization of finite objects in each of the corresponding categories using monomorphisms/injections (denoted as iC, iE, and iB, respectively); (3) a formulation of bifinite Chu spaces with respect of iC; (4) the existence of universal, homogeneous Chu spaces in this category. Unanticipated results driving this development include the fact that: (a) in C, a morphism (f,g) is monic iff f is injective (but g is not necessarily surjective); (b) while colimits always exist in iE, it is not the case for iC and iB; (c) not all finite Chu spaces (considered set-theoretically) are finite objects in their categories. This study opens up opportunities for further investigations into recursively defined Chu spaces, as well as constructive models of linear logic.


Weighted logics for XML.
(
with H. Vogler), 2006  
Abstract.
We define a weighted monadic second order logic for XML-documents (weighted uMSO-logic), viewed as unranked trees. Such a logic allows us to pose quantitative queries to XML-databases. Also we define the concept of unranked weighted tree automata and prove that, for every commutative semiring K, they have the same expresive power as (1) restricted weighted uMSO-logic, (2) almost existential weighted uMSO-logic whenever the additive monoid of K is locally finite , (3) (unrestricted) weighted uMSO-logic whenever K is locally finite. Moreover, if K is a computable field, then the equivalence of any two sentences of restricted weighted uMSO-logic is decidable and there is an effective procedure to construct the automaton from the sentence.


On weighted Büchi automata with order-complete weights.
(
with U. Püschmann), Intern. J. of Algebra and Computation, 17 (2007), 235-260.  
Abstract.
We investigate Büchi automata with weights for the transitions. Assuming that the weights are taken in a suitable ordered semiring, we show how to define the behaviours of these automata on infinite words. Our main result shows that the formal power series arising in this way are precisely the ones which can be constructed using !-rational operations. This extends the classical Kleene-Schützenberger result for weighted finite automata to the case of infinite words and generalizes Büchi s theorem on languages of infinite words. We also derive versions of our main result for non-complete semirings and for other automata models.


Weighted automata and weighted logics on infinite words.
(
with G.Rahonis), 10th Int. Conf. on Developments in Language Theory (DLT), Lecture Notes in Computer Science vol. 4036, Springer, 2006, pp. 49-58
Abstract.
We introduce weighted automata over infinite words with Muller acceptance condition and we show that their behaviors coincide with the semantics of weighted restricted MSO-sentences. Furthermore, we establish an equivalence property of weighted Muller and weighted Büchi automata over certain semirings.


On aperiodic and star-free formal power series in partially commuting variables.
(
with P. Gastin), Theory of Computing Systems 42 (2008), 608-631.
Abstract.
Formal power series over non-commuting variables have been investigated as representations of the behavior 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 the tropical semiring), then the aperiodic and the star-free series coincide. This generalizes a classical result of Schützenberger (1961) for aperiodic regular languages and subsumes a result of Guaiana, Restivo and Salemi (1992) on aperiodic trace languages.


Weighted tree automata and weighted logics.
(
with H.Vogler), 366 (2006), 228-247
Abstract.
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 wich 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 [M.Droste and P.Gastin: Weighted automata and weighted logics, 2005] from formal power series on words to formal tree series.


Weighted automata and weighted logics.
(
with P.Gastin), in: Automata Languages and Programming (32th ICALP, Lissabon) 2005,
Lecture Notes in Computer Science vol. 3580, Springer, 2005, pp. 513-525, Theoretical Computer Science vol. 380, pp. 69-86, Full version: pdf ps
Abstract.
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 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.
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.


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, 38 (2005), 1-38
.
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), Lecture Notes in Comp. Science 1256, Springer, 1997, pp. 682-692.
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 if they have order-isomorphic canonical domains.



last modified December 19, 2012