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

**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