Skew and infinitary formal
power series.
(with D. Kuske), in: Automata Languages and Programming
(30th ICALP, Eindhoven)
Lecture Notes in Computer Science 2719, 2003, pp. 426 - 438
.
Abstract.
We investigate finite-state systems with costs. Departing
from the classical theory, in this paper the cost of an action does not only
depend on the state of the system, but also on the time when it is executed;
this reflects the usual human evaluation practices in which later events
are considered less urgent and carry less weight than close events. We first
characterize the terminating behaviors of such systems in terms of rational
formal power series. This generalizes a classical result of Schützenberger.
Secondly, we deal with nonterminating behaviors and
their costs. This includes an extension of the Büchi-acceptance condition
from finite automata to weighted automata and provides a characterization
of these nonterminating behaviors in terms of $/omega$-rational formal
power series. This generalizes a classical theorem of Büchi.
Automata with concurrency
relations - a survey.
(with D. Kuske), in:
Advances in Logic, Artificial Intelligence and Robotics,
(eds. J. Abe, J. da Silva
Filho), IOS Press, 2002, pp. 152 - 172; invited survey.
Abstract:
Automata with concurrency relations, which occured
in the verification methods of concurrent programs, are labeled transition
systems with state-dependent concurrency relations on the actions. They
generalize the asynchronous transition systems and trace alphabets. Here
we survey results obtained on such automata with connections to domain theory,
Petri nets, graph-theoretic representations and algebraic and logical definability
of languages.
A Kleene theorem for weighted
tree automata.
(with H. Vogler), Theory of Computing Systems, to appear.
Abstract.
In this paper we prove Kleene's result for tree series
over a commutative and idempotent semiring A (which is not necessarily
complete or continuous), i.e., the class of recognizable tree series over
A and the class of rational tree series over A are equal. We
show the result by direct automata-theoretic constructions and prove their
correctness.
Rational transformations
of formal power series
(with G.-Q. Zhang), in:
Automata, Languages and Programming (28th ICALP, Crete),
Lecture Notes in Computer
Science 2076, Springer 2001, 555 - 566.
Abstract.
Formal power series are an extension of formal languages.
Recognizable formal power series can be captured by the so-called weighted
finite automata, generalizing finite state machines. In this paper, motivated
by codings of formal languages, we introduce and investigate two types of
transformations for formal power series. We characterize when these transformations
preserve rationality, generalizing the recent results of Zhang [15] to the
formal power series setting. We show, for example, that the "square-root"
operation, while preserving regularity for formal languages, preserves rationality
for formal power series when the underlying semiring is commutative or locally
finite, but not in general.
Continuous Petri nets and
transition systems
(with R.M. Shortt), in:"Unifying
Petri Nets" , (H. Ehrig, G. Juhas, J. Padberg, G. Rozenberg, eds.)
Lecture Notes in Computer
Science 2128, Springer 2001, pp. 457 - 484; invited contribution.
Abstract.
In many systems, the values of finitely many parameters
can be influenced in a continuous way by controls acting with possibly
varying strength over intervals of time. For this, we present general models
of continuous Petri nets and of continuous transition systems with situation-dependent
concurrency. With a suitable concept of morphisms, we obtain a categorial
adjunction between these two models, and often even a coreflection. This
shows that the concept of regions is also applicable in this continuous setting.
Finally, we prove that our categories of continuous Petri nets and of continuous
automata with concurrency have products and conditional coproducts.
Recognizable languages in
divisibility monoids
(with D. Kuske),
Mathem. Structures in Comp. Science 11 (2001), pp. 743 - 770.
Abstract.
We define the class of divisibility monoids which
arise as quotients of the free monoid $\sum*$ modulo certain equations of
the form ab=cd. These form a much larger class than free partially
commutative monoids, and we show, under certain assumptions, that the recognizable
languages in these divisibility monoids coincide with c-rational languages.
The proofs rely on Ramsey's theorem, distributive lattice theory and on
Hashigushi's rank function generalized to these monoids. We obtain Ochmañski's
theorem on recognizable languages in free partially commutative monoids as
a consequence.
From Petri nets to automata
with concurrency
(with R.M. Shortt),
Applied Categorical Structures 10 (2002), 173 - 191.
Abstract.
Automata with concurency relations are labelled transition
systems with a collection of state-dependent binary independence relations
for the actions. We show how to associate with each Petri net (place/transition
net) such an automaton having the same dynamic behaviour. We characterize
the automata arising in this way, and with suitable notions of morphisms
for Petri nets and for automata with concurrency relations we extend this
correspondence to a coreflection between the associated categories. As a consequence,
we derive, that these categories have products and conditional oproducts.
Universal homogeneous graph-like
structures and domains
(with P. Boldi and F.
Cardone), Mathem. Structures in Comp. Science 12 (2002), 91 - 109.
Abstract.
We present explicit constructions of universal homogeneous
objects in categories of domains with stable embedding-projection pairs as
arrows. These results make use of a representation of such domains through
graph-like structures and apply a generalization of Rado's result on the
existence of the universal homogeneous countable graph. In particular, we
build universal homogeneous objects in the categories of coherence spaces
and qualitative domains, introduced by (Girard 1987; Girard 1986), and two
categories of hypercoherences recently studied by (Ehrhard 1993). Our constructions
reply upon basic numerical notions. We also show that a suitable random construction
of Rado's graph and its generalizations produces with probability 1 the universal
homogeneous structures presented here.
On aperiodic and star-free
formal power series in partially commuting variables
(with P. Gastin), in:
Formal Power Series and Algebraic Combinatorics (D. Krob, A.A. Mikhalev,
A.V. Mikhalev, eds.),
12th Int. Conf., Moscow, Springer 2000, pp. 158 - 169.
Abstract.
Formal power series over non-commuting variables
have been investigated as representations of the behaviour of automata with
multiplicities. Here we introduce and investigate the concepts of aperiodic
and of star-free formal power series over semirings and partially commuting
variables. We prove that if the semiring K is idempotent and commutative,
or if K is idempotent and the variables are non-commuting, then the
product of any two aperiodic series is again aperiodic. We also show that
if K is idempotent and the matrix monoids over K have a Burnside
property (satisfied, e.g. by tropical semiring), then the aperiodic and the
star-free series coincide.
Asynchronous cellular automata
for pomsets
(with
P. Gastin and D. Kuske), Theoret. Comp. Science 247 (2000), 1 - 38
(fundamental study).
Abstract.
This paper extends to pomsets without auto-concurrency
the fundamental notion of asynchronous automata (ACA) which was originally
introduced for traces by Zielonka. We generalize to pomsets the notion
of asynchronous mapping introduced by Cori, Métivier and Zielonka
and we show how to construct a deterministic ACA from an asynchronous mapping.
Then we investigate the relation between the expressiveness of monadic
second-order logic, nondeterministic ACAs and deterministic ACAs. We can
generalize Büchi's theorem for finite words to a class of pomsets without
auto-
concurrency which satisfy a natural axiom. This axiom
ensures that an asynchronous cellular automaton works on the pomset as a
concurrent read and exclusive owner write machine. More precisely, in this
class nondeterministic ACAs, deterministic ACAs and monadic second-order logic
have the same expressive power. Then we consider a class where deterministic
ACAs are strictly weaker than nondeterministic ones. But in this class nondeterministic
ACAs still capture monadic second-order logic. Finally, it is shown that even
this equivalence does not hold in the class of pomsets since there the class
of recognizable pomset languages is not closed under complementation.
On recognizable languages
in divisibility monoids
(with
D. Kuske), in: 12th Int. Symp. on Fundamentals of Computation Theory
(FCT, Iasi)
Lecture Notes in Comp.
Science, Springer 1684, 1999, pp. 246 - 257.
Abstract.
Kleene's theorem on recognizable languages in free monoids is considered to be of eminent importance in theoretical computer
science. It has been generalized into various directions, including trace
and rational monoids. Here, we investigate divisibility monoids which are
defined by and capture algebraic properties sufficient to obtain a characterization
of the recognizable languages by certain rational expressions as known from
trace theory. The proofs rely on Ramsey's theorem, distributive lattice theory
and on Hashigushi's rank function generalized to our divisibility monoids.
We obtain chmañski's theorem on recognizable languages in free partially
commutative monoids as a consequence.
The Kleene-Schützenberger
theorem for formal power series in partially commuting variables
(with P. Gastin), Information
and Computation 153 (1999), 47 - 80.
Abstract.
Kleene's theorem on the coincidence of regular and
rational languages in free monoids has been generalized by Schützenberger
to a description of the recognizable formal power series in noncommuting
variables over arbitrary semirings and by Ochmañski to a characterization
of the recognizable languages in trace monoids. We will describe the recognizable
formal power series over
arbitrary semirings and in partially commuting variables,
i.e. over trace monoids. We prove that the recognizable series are certain
rational power series, which can be constructed from the polynomials by using
the operations sum, product, and a restricted star which is applied only
to series for which the elements in the support all have the same connected
alphabet. The converse is true if the underlying semiring is commutative.
Moreover, if in addition the semiring is idempotent then the same result holds
with a star restricted to series for which the elements in the support have
connected (possibly different) alphabets. It is shown that these assumptions
over the semiring are necessary. This provides a joint
generalization of Kleene's, Schützenberger's
and Ochmañski's theorems.
On recognizable and rational
formal power series in partially commuting variables
(with P. Gastin), in:
Automata, Languages and Programming (24th ICALP, Bologna).
Abstract.
We will describe the recognizable formal power
series over arbitrary semirings and in partially commuting variables, i.e.
over trace monoids. We prove that the recognizable series are certain rational
power series, which can be constructed from the polynomials by using the
operations sum, product, and a restricted star which is applied only to series
for which the elements in the support all have the same connected alphabet.
The converse is true if the underlying semiring is commutative. Moreover,
if in addition the semiring is idempotent then the same result holds with
a star restricted to series for which the elements in the support have connected
(possibly different) alphabets. It is shown that these
assumptions over the semiring are necessary. This
provides a joint generalization of Kleene's, Schützenberger's and Ochmañski's
theorems.
Recognizable and logically
definable languages of finite computations in concurrent automata
(with D. Kuske),
Intern. J. of Foundations of Comp. Sc. 9 (1998), 295 - 313.
Abstract.
Automata with concurrency relations A, which
occured in formal verification methods of concurrent programs, are labeled
transition systems with a collection of binary relations describing when
two actions in a given state of the automaton can happen independently of
each other. The concurrency monoid M(A) comprises all finite computation
sequences of A, modulo a canonical congruence induced by the concurrency
relations, with composition as monoid operation. Then $M^{\infty}(A)$
denotes the set of all infinite products in M(A); its elements can
be represented by labeled partially ordered sets. Under suitable assumptions
on A, we show that a language L in $M^{\infty}(A)$ is
recognizable iff it is definable by a formula of monadic second order logic,
and that it is recognizable iff it can be constructed from recognizable languages
in M(A) using co-rational expressions. This generalizes various recent
results in trace theory.
Representation of computations
in concurrent automata by dependence orders
(with
F. Bracho and D. Kuske), Theoret. Comp. Science 174 (1997), 67 - 96.
Abstract.
An automaton with concurrency relations A
is a labelled transition system with a collection of binary relations indicating
when two actions in a given state of the automaton can occur independently
of each other. The concurrency relations induce a natural equivalence relation
for finite computation sequences. We investigate two graph-theoretic representations
of the equivalence classes of
computation sequences and obtain that under suitable
assumptions on A they are isomorphic. Furthermore, the graphs are
shown to carry a monoid operation reflecting precisely the composition of
computations. This generalizes fundamental graph-theoretical representation
results due to Mazurkiewicz in trace theory.
Asynchronous cellular automata
for pomsets without auto-concurrency
(with P. Gastin), in:
7th Int. Conf. on Concurrency Theory (CONCUR, Pisa),
Lecture Notes in Comp.
Science 1119, Springer, 1996, pp. 627 - 638.
Abstract.
This paper extends to pomsets without auto-concurrency
the fundamental notion of asynchronous cellular automata (ACA) which was
originally introduced for traces by Zielonka. We generalize to pomsets the
notion of asynchronous mapping introduced by Zielonka and we show how to
construct a
deterministic ACA from an asynchronous mapping. Our
main result generalizes Büchi's theorem for a class of pomsets without
auto-concurrency which satisfy a natural axiom. This axiom ensures that an
asynchronous cellular automaton works on the pomset as a concurrent read
owner write machine. More precisely, we prove the equivalence between non
deterministic ACA, deterministic ACA and
monadic second order logic for this class of pomsets.
Trace languages definable
with modular quantifiers
(with D. Kuske), in:
Developments in Language Theory, 2nd int. Conf., Magdeburg,
World Scientific Publ.,
1996, pp. 386 - 395.
Abstract.
We study an extension of first-order logic obtained
by adjoining quantifiers that count with respect to an integer modulus.
It is shown that the trace languages definable in the framework are precisely
the regular trace languages whose syntactic monoids contain only solvable
groups. Also, we consider the languages that are definable by sentences
that contain only these modular quantifiers. Our results generalize corresponding
results of Straubing, Thérien and Thomas on words.
Aperiodic languages in concurrency
monoids
Information and Computation
126 (1996), 105 - 113.
Abstract.
Automata with concurrency relations A are
labeled transition systems with a collection of binary relations indicating
when two events, in a given state of the automaton, are concurrent.We investigate
concurrency monoids M(A) comprising all finite computation sequences
of A, modulo a canonical congruence induced by the concurrency relations,
with composition as monoid operation. Under suitable assumptions on A,
we obtain a characterization of the star-free languages of M(A).
This generalizes a classical result of G. Guaiana, A. Restivo and S. Salemi
in trace theory.
Languages and logical definability
in concurrency monoids
(with D. Kuske), in "Computer
Science Logic", Paderborn 1995,
Lecture Notes in Computer
Science 1092, Springer, 1996, pp. 233 - 251.
Abstract.
Automata with concurrency relations A are
labeled transition systems with a collection of binary relations describing
when two actions in a given state of the automaton can occur independently
of each other. The concurrency monoid M(A) comprises all finite computation
sequences of A, modulo a canonical congruence induced by the concurrency
relations, with composition as monoid operation; its elements can be represented
ba labelled partially ordered sets. Under suitable assumptions on A,
we show that a language L in M(A) is recorgnizable iff it is
definable ba a formula of monadic second order logic. We also investigate
the relationship between aperiodic and first-order definable languages in
M(A). This generalizes various recent results in trace theory.
Dependence orders for computations
of concurrent automata
(with F. Bracho and D.
Kuske), in: STACS '95, Lecture Notes in Comp. Science 900,
Springer, 1995, pp. 467
- 478.
Abstract.
An automaton with concurrency relations A
is a labeled transition systems with a collection of binary relations indicating
when two events in a given state of the automaton can happen independently
from each other. The concurrency relations induce a natural equivalence
relation for finite computation sequences. We investigate two graph-theoretic
representations of the equivalence classes of computation sequences and obtain
that under suitable assumptions on A they are isomorphic. Furthermore,
the graphs are shown to carry a monoid operation reflecting precisely the
composition of computations. This generalizes fundamental graph theoretical
representation results due to Mazurkiewicz in trace theory.
Recognizable languages in
concurrency monoids
Theoret. Comp. Science
150, 1995, 77 - 108.
Abstract.
Automata with concurrency relations A are
labelled transition systems with a collection of binary relations indicating
when two actions, in a given state of the automaton, are concurrent. We investigate
concurrency monoids M(A) comprising all finite computation sequences
of A, modulo a canonical congruence induced by the concurrency relations,
with composition as monoid operation. Under suitable assumptions on A,
we obtain a Kleene-type characterization of the recognizable languages of
M(A). This generalizes results of Cori, Métivier, Perrin and
Ochmanski in trace theory.
A Kleene theorem for recognizable
languages over Concurrency monoids
in: Automata, Languages
and Programming (21st ICALP, Jerusalem),
Lecture Notes in Comp.
Science 820, Springer, 1994, pp. 388 - 399.
Abstract.
Automata with concurrency relations A are
labelled transition systems with a collection of binary relations indicating
when two events, in a given state of the automaton, are concurrent. We investigate
concurrency monoids M(A) comprising all finite computation sequences
of A, modulo a canonical congruence induced by the concurrency relations,
with composition as monoid operation. Under suitable assumptions on A,
we obtain a Kleene-type characterization of the recognizable languages of
M(A). This generalizes results of Cori, Métivier, Perrin and
Ochmanski in trace theory.
Labelled domains and automata
with concurrency
(with F. Bracho), Theoret.
Comp. Science 135 (1994), 289 - 318.
Abstract.
We investigate an operational model of concurrent
systems, called automata with concurrency relations. These are labelled transition
systems A in which the event set is endowed with a collection of
binary concurrency relations which indicate when two events, in a particular
state of the automaton, commute. This model generalizes asynchronous transition
systems, and in trace theory we obtain, through a permutation equivalence
for computation sequences of A, an induced domain (D(A),<).
Here we construct a categorical equivalence between a large category of
("cancellative") automata with concurrency relations and the associated domains.
We show that each cancellative automaton can be reduced to a minimal cancellative
automaton generating, up to isomorphism, the same domain. Furthermore, when
fixing the event set, this minimal automaton is unique.
Petri nets and automata with
concurrency relations - an adjunction
(with R. Shortt), in:
"Semantics of programming Languages and Model Theory"
(M.
Droste, Y. Gurevich, eds.), Gordon and Breach Science Publ., OPA (Amsterdam),
1993, 69 - 87.
Abstract.
We consider the category P of Petri
nets with capacities (place/transition net) and also a category A
of automata with a collection of binary concurrency relations indicating
when two events, in a particular state of the automaton, commute. We construct
an adjunction between the categories P and A. This generalizes
a recent result of Winskel and Nielsen for condition/event-nets and asynchronous
transition systems.
Universal domains and the
amalgamation property
(with R. Göbel),
Mathem. Structures in Comp. Science 3 (1993), 137 - 159.
Abstract.
In the theory of denotational semantics of programming
languages, several authors have constructed various kinds of universal
domains. We present here a categorical generalization of a well-known result
in model theory, which we use to characterize large classes of reasonable
categories that contain universal homogeneous objects. The existence uf
such objects is characterized by the condition that the finite objects in
the category satisfy the amalgamation property. We derive from this the
existence and uniqueness of universal homogeneous domains for several categories
of bifinite domains, with embedding-projection-pairs as morphisms. We also
obtain universal homogeneous objects for various categories of stable bifinite
domains. In contrast, several categories of event domains and concrete domains
and the category of all coherent Scott-domains do not contain universal homogeneous
objects. Finally, we show that all our constructions can be performed effectively.
Concurrent automata and domains
Intern. Journal of
Foundations of Comp. Science 3 (1992), 389 - 418.
Abstract.
We introduce an operational model of concurrent systems,
called automata with concurrency relations. These are labelled transition
systems A in which the event set is endowed with a collection of symmetric
binary relations which describe when two events at a particular state of
A commute. This model generalizes the recent concept of Stark's trace
automata. A permutation equivalence for computation sequences of A arises
canonically, and we obtain a natural domain (D(A),<), comprising
the induced equivalence classes. We give a complete order-theoretic characterization
of all such partial orders (D(A),<), which turn out to
be particular finitary domains. The arising domains (D(A),<)
are particularly pleasant Scott-domains, if A is asumed to be concurrent,
i.e. if the concurrency relations of A depend (in a natural way)
locally on each other, but not necessarily globally. We show that both event
domains and dI-domains arise, up to isomorphism, as domains (D(A),<)
with well-behaved such concurrent automata A. We introduce
a subautomaton relationship for concurrent automata and show that, given
two concurrency domains (D,<), (D',<), there exists a
nice stable embedding-projection pair from D to D' iff
D, D' can be generated by concurrent automata A, A' such that
A is a subautomaton of A'. Finally, we introduce the concept of locally
finite concurrent automata and show that there exists a universal homogeneous
locally finite concurrent automaton, which is unique up to isomorphism.
Finite axiomatizations for
universal domains
J. of Logic and Computation
2 (1992), 119 - 131
Abstract.
In the theory of denotional semantics of programming
languages, several authors established the existence of particular kinds
of universal domains. Here we consider the categories of all $\omega$-bifinite
domains, all $\omega$-bifinite L-domains, all $\omega$-Scott-domains,
and all $\omega$-algebraic lattices, respectively, in each case with embedding-projection
pairs as morphisms. It has been shown that each of these categories contains
a universal homogeneous, or saturated, object, which is unique up to isomorphism.
Here we introduce for each of these four categories C a set of finite
axioms $S_C$, formulated in a first-order language of predicate
calculus for posets, and show that an arbitrary domain $(D,\leq)\in
C$ is the universal homogeneous object in C if and only if
its subset of compact elements satisfies all axioms in $S_C$.
Universal information systems
(with R. Göbel),
Intern. J. of Foundations of Comp. Science 1(1991). 413 - 424.
Abstract.
In the theory of denotional semantics of programming
languages, several authors proved the existence of particular kinds of
universal domains. D. Scott constructed universal information systems, which
are, however, not unique up to isomorphism. Here, we use a model-theoretic
technique to establish the existence and uniqueness of a universal homogeneous
information system. Similar results are also obtained for canonical and
for stable information systems, respectively.
Universal homogeneous event
structures and domains
Information and Computation
94 (1991), 48 - 61.
Abstract.
In the theory of denotional semantics of programming
languages, several authors established the existence of particular kinds
of "universal" domains. Here, we use a general model-theoretic result
to show that there
exists a unique countable universal homogeneous event
structure. From this, we deduce that the category of all event domains, with
stable embedding-projection pairs as morphisms, contains a universal object.
Similarly, we also obtain a universal dI.domain. We also show that the category
of all event domains is closed under inverse limits. Similar results are
derived for Kahn and Plotkin's concrete data structures and concrete domains.
Concurrency, automata and
domains
in: Automata, Languages
and Programming (17th ICALP, Warwick),
Lecture Notes in Comp.
Science 443, Springer, 1990, 195 - 208.
Abstract.
We introduce an operational model of concurrent systems,
called automata with concurrency relations. These are labelled transition
systems A in which the event set is endowed with a collection of symmetric
binary relations which describe when two events at a particular state of
A commute; we assume that these concurrency relations depend (in a
natural way) locally on each other, but not globally. This model generalizes
the recent concept of Stark's trace automata. A permutation equivalence for
computation sequences of A arises canonically, and we obtain a natural
domain (D(A),<), comprising the induced equivalence classes.
We give a complete order-theoretic characterization of all such concurrency
domains (D(A),<), which turn out to be particular finitary
Scott-domains. We also show that dI-domains arise, up to isomorphism, as domains
(D(A),<) with
particularly well-behaved concurrent automata A.
Non-deterministic information
systems and their domains
(with R. Göbel),
Theoret. Comp. Sci. 75 (1990), 289 - 309.
Abstract.
In the theory of denotional semantics of programming
languages Dedekind-complete, algebraic partial orders (domains) frequently
have been considered since Scott's and Strachey's fundamental work in 1971
(Stoy, 1977). As Scott (1982) showed, these domains can be represented
canonically by (deterministic) information systems. However, recently, more
complicated constructions (such as power domains) have led to more general
domains (Plotkin, 1976; Smyth and Plotkin, 1977; Smyth, 1983). We introduce
non-deterministic information systems and establish the representation theorem
similar to Scott (1982) for these more general domains. This result will
be the basis for solving recursive domain equations.
Recursive domain equations
for concrete data structures
Information and Computation
82 (1989), 65 - 80.
Abstract.
In the theory of denotional semantics of programming
languages, we study event structures which combine features of Scott's
information systems and Kahn and Plotkin's concrete data structures and
model computational processes. We show that a simple approximation concept
for event structures allows us to obtain straightforward solutions of recursive
domain equations for event domains. From this, we derive a generalization
of corresponding theorems of Kahn and Plotkin respectively Berry and Curien
for concrete data structures and concrete domains.
Event structures and domains
Theoret. Comp. Sci.
68 (1989), 37 - 47.
Abstract.
In the theory of denotional semantics, we study event
structures which generalize Kahn and Plotkin's concrete data structures and
which model computational processes. With each event structure we associate
canonically an event domain (a particular algebraic complete partial order),
and conversely we derive a representation result for event domains. For
a particular class of event structures, the canonical event structures, we
obtain that any two canonical event structures are isomorphic iff they have
order-isomorphic canonical domains.