Author name cluster

Stefan Milius

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

24 papers

2 author rows

I&C Journal 2023 Journal Article

Eilenberg's variety theorem without Boolean operations

Fabian Birkmann
Stefan Milius
Henning Urbat

Eilenberg's variety theorem marked a milestone in the algebraic theory of regular languages by establishing a formal correspondence between properties of regular languages and properties of finite monoids recognizing them. Motivated by classes of languages accepted by quantum finite automata, we introduce basic varieties of regular languages, a weakening of Eilenberg's original concept that does not require closure under any boolean operations, and prove a variety theorem for them. To do so, we investigate the algebraic recognition of languages by lattice bimodules, generalizing Klíma and Polák's lattice algebras, and we utilize the duality between algebraic completely distributive lattices and posets.

MFCS Conference 2023 Conference Paper

Positive Data Languages

Florian Frank 0002
Stefan Milius
Henning Urbat

Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.

FSCD Conference 2022 Conference Paper

Stateful Structural Operational Semantics

Sergey Goncharov 0001
Stefan Milius
Lutz Schröder
Stelios Tsampas 0001
Henning Urbat

Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.

MFCS Conference 2021 Conference Paper

A Linear-Time Nominal μ-Calculus with Name Allocation

Daniel Hausmann 0001
Stefan Milius
Lutz Schröder

Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as {regular nondeterministic nominal automata (RNNAs)} have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-μTL} for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-μTL} allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-μTL} over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.

FSCD Conference 2021 Conference Paper

Coalgebra Encoding for Efficient Minimization

Hans-Peter Deifel
Stefan Milius
Thorsten Wißmann

Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.

I&C Journal 2020 Journal Article

A new foundation for finitary corecursion and iterative algebras

Stefan Milius
Dirk Pattinson
Thorsten Wißmann

This paper contributes to a generic theory of behaviour of “finite-state” systems. Systems are coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to the locally finite fixpoint (LFF), a new fixpoint of the endofunctor. The LFF exists provided that the endofunctor is finitary and preserves monomorphisms, is a subcoalgebra of the final coalgebra, i. e. it is fully abstract w. r. t. behavioural equivalence, and it is characterized by two universal properties: as the final locally finitely generated coalgebra, and as the initial fg-iterative algebra. Instances of the LFF are: regular languages, rational streams, rational formal power-series, regular trees etc. Moreover, we obtain e. g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten), and the monad of Courcelle's algebraic trees.

TCS Journal 2019 Journal Article

On functors preserving coproducts and algebras with iterativity

Jiří Adámek
Stefan Milius

An algebra for a functor H is called completely iterative (cia, for short) if every flat recursive equation in it has a unique solution. Every cia is corecursive, i. e. , it admits a unique coalgebra-to-algebra morphism from every coalgebra. If the converse also holds, H is called a cia functor. We prove that whenever the base category is hyper-extensive (i. e. countable coproducts are ‘well-behaved’) and H preserves countable coproducts, then H is a cia functor. Surprisingly few cia functors exist among standard finitary set functors: in fact, the only ones are those preserving coproducts; they are given by X ↦ W × ( − ) + Y for some sets W and Y.

MFCS Conference 2017 Conference Paper

Eilenberg Theorems for Free

Henning Urbat
Jirí Adámek
Liang-Ting Chen 0001
Stefan Milius

Eilenberg-type correspondences, relating varieties of languages (e. g. , of finite words, infinite words, or trees) to pseudovarieties of finite algebras, form the backbone of algebraic language theory. We show that they all arise from the same recipe: one models languages and the algebras recognizing them by monads on an algebraic category, and applies a Stone-type duality. Our main contribution is a variety theorem that covers e. g. Wilke's and Pin's work on infinity-languages, the variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two categorical approaches of Bojanczyk and of Adamek et al. In addition we derive new results, such as an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.

TCS Journal 2015 Journal Article

Coalgebraic constructions of canonical nondeterministic automata

Robert S.R. Myers
Jiří Adámek
Stefan Milius
Henning Urbat

For each regular language L we describe a family of canonical nondeterministic acceptors (nfas). Their construction follows a uniform recipe: build the minimal dfa for L in a locally finite variety V, and apply an equivalence between the category of finite V -algebras and a suitable category of finite structured sets and relations. By instantiating this to different varieties, we recover three well-studied canonical nfas: V = boolean algebras yields the átomaton of Brzozowski and Tamm, V = semilattices yields the jiromaton of Denis, Lemay and Terlutte, and V = Z 2 -vector spaces yields the minimal xor automaton of Vuillemin and Gama. Moreover, we obtain a new canonical nfa called the distromaton by taking V = distributive lattices. Each of these nfas is shown to be minimal relative to a suitable measure, and we derive sufficient conditions for their state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties of the canonical nfas.

TCS Journal 2015 Journal Article

Killing epsilons with a dagger: A coalgebraic study of systems with algebraic label structure

Filippo Bonchi
Stefan Milius
Alexandra Silva
Fabio Zanasi

We propose an abstract framework for modelling state-based systems with internal behaviour as e. g. given by silent or ϵ-transitions. Our approach employs monads with a parametrized fixpoint operator † to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems and non-deterministic transducers.

TCS Journal 2014 Journal Article

Base modules for parametrized iterativity

Jiří Adámek
Stefan Milius
Jiří Velebil

The concept of a base, that is a parametrized finitary monad, which we introduced earlier, followed the footsteps of Tarmo Uustalu in his attempt to formalize parametrized recursion. We proved that for every base free iterative algebras exist, and we called the corresponding monad the rational monad of the base. Here we introduce modules for a base, and we prove that the rational monad of a base gives rise to a canonical module, that is characterized as the free iterative module on the given base. This generalizes the classical, nonparametric case of iterative Σ-algebras whose rational monad is the monad of rational Σ-trees and that was characterized by Calvin Elgot et al. as the free iterative monad on Σ. A basic parametrized example is the base assigning to every parameter set X the monad A ↦ X ⁎ × A whose rational monad is the monad of all right-wellfounded rational binary trees; the rational module for this base is the natural transformation ( X ⁎ × X ) × A → X ⁎ × A given by parametrized concatenation.

I&C Journal 2013 Journal Article

How iterative reflections of monads are constructed

Jiří Adámek
Stefan Milius
Jiří Velebil

Every ideal monad M on the category of sets is known to have a reflection M ˆ in the category of all iterative monads of Elgot. Here we describe the iterative reflection M ˆ as the monad of free iterative Eilenberg–Moore algebras for M. This yields numerous concrete examples: if M is the free-semigroup monad, then M ˆ is obtained by adding a single absorbing element; if M is the monad of finite trees then M ˆ is the monad of rational trees, etc.

TCS Journal 2011 Journal Article

On second-order iterative monads

Jiří Adámek
Stefan Milius
Jiří Velebil

B. Courcelle studied algebraic trees as precisely the solutions of all recursive program schemes for a given signature in Set. He proved that the corresponding monad is iterative. We generalize this to recursive program schemes over a given finitary endofunctor H of a “suitable” category. A monad is called second-order iterative if every guarded recursive program scheme has a unique solution in it. We construct two second-order iterative monads: one, called the second-order rational monad, S H, is proved to be the initial second-order iterative monad. The other one, called the context-free monad, C H, is a quotient of S H and in the original case of a polynomial endofunctor H of Set we prove that C H is the monad studied by B. Courcelle. The question whether these two monads are equal is left open.

CSL Conference 2011 Conference Paper

Power-Set Functors and Saturated Trees

Jirí Adámek
Stefan Milius
Lawrence S. Moss
Lurdes Sousa

We combine ideas coming from several fields, including modal logic, coalgebra, and set theory. Modally saturated trees were introduced by K. Fine in 1975. We give a new purely combinatorial formulation of modally saturated trees, and we prove that they form the limit of the final omega-op-chain of the finite power-set functor Pf. From that, we derive an alternative proof of J. Worrell's description of the final coalgebra as the coalgebra of all strongly extensional, finitely branching trees. In the other direction, we represent the final coalgebra for Pf in terms of certain maximal consistent sets in the modal logic K. We also generalize Worrell's result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor Mf studied by H. P. Gumm and T. Schröder. We introduce the concept of an i-saturated tree for all ordinals i, and then prove that the i-th step in the final chain of the power set functor consists of all i-saturated trees. This leads to a new description of the final coalgebra for the restricted power-set functors Plambda (of subsets of cardinality smaller than lambda).

I&C Journal 2010 Journal Article

Equational properties of iterative monads

Jiří Adámek
Stefan Milius
Jiří Velebil

Iterative monads of Calvin Elgot were introduced to treat the semantics of recursive equations purely algebraically. They are Lawvere theories with the property that all ideal systems of recursive equations have unique solutions. We prove that the unique solutions in iterative monads satisfy all the equational properties of iteration monads of Stephen Bloom and Zoltán Ésik, whenever the base category is hyper-extensive and locally finitely presentable. This result is a step towards proving that functorial iteration monads form a monadic category over sets in context. This shows that functoriality is an equational property when considered w. r. t. sets in context.

I&C Journal 2008 Journal Article

Bases for parametrized iterativity

Jiří Adámek
Stefan Milius
Jiří Velebil

Parametrized iterativity of an algebra means the existence of unique solutions of all finitary recursive systems of equations where recursion is allowed to use only some variables (chosen as a parameter). We show how such algebras can be introduced in an arbitrary category A by employing a base, i. e. , an operation interpreting objects of A as monads on A. For every base we prove that free base algebras and free iterative base algebras exist. The main result is a coalgebraic construction of the latter: all equation morphisms form a diagram whose colimit is proved to be a free iterative base algebra.

TCS Journal 2008 Journal Article

Corrigendum to: “The category theoretic solution of recursive program schemes” [Theoret. Comput. Sci. 366 (2006) 3–59]

Stefan Milius
Lawrence S. Moss

This is a corrigendum for our paper [S. Milius, L. S. Moss, The category theoretic solution of recursive program schemes, Theoret. Comput. Sci. 366 (2006) 3–59]. The main results are correct, but we offer some changes to the definitions and proofs concerning interpreted recursive program schemes.

TCS Journal 2007 Journal Article

Algebras with parametrized iterativity

Jiří Adámek
Stefan Milius
Jiří Velebil

Iterative algebras, as studied by Nelson and Tiuryn, are generalized to algebras whose iterativity is parametrized in the sense that only some variables can be used for iteration. For example, in the case of one binary operation, the free iterative algebra is the algebra of all rational binary trees; if only the left-hand variable is allowed to be iterated, then the free iterative algebra is the algebra of all right-well-founded rational binary trees. In order to express such parametrized iterativity, we work with parametrized endofunctors of Set, i. e. finitary endofunctors H: Set × Set → Set, and introduce the concept of iterativity for algebras for the endofunctor X ↦ H ( X, X ). We then describe free iterative H -algebras.

MFCS Conference 2007 Conference Paper

What Are Iteration Theories?

Jirí Adámek
Stefan Milius
Jirí Velebil

Abstract We prove that iteration theories can be introduced as algebras for the monad on the category of signatures assigning to every signature the rational- -tree signature. This supports the result that iteration theories axiomatize precisely the equational properties of least fixed points in domain theory: is the monad of free rational theories and every free rational theory has a continuous completion.

I&C Journal 2006 Journal Article

Terminal coalgebras and free iterative theories

Jiřı´ Adámek
Stefan Milius

Every finitary endofunctor H of Set can be represented via a finitary signature Σ and a collection of equations called “basic”. We describe a terminal coalgebra for H as the terminal Σ-coalgebra (of all Σ-trees) modulo the congruence of applying the basic equations potentially infinitely often. As an application we describe a free iterative theory on H (in the sense of Calvin Elgot) as the theory of all rational Σ-trees modulo the analogous congruence. This yields a number of new examples of iterative theories, e. g. , the theory of all strongly extensional, rational, finitely branching trees, free on the finite power-set functor, or the theory of all binary, rational unordered trees, free on one commutative binary operation.

TCS Journal 2006 Journal Article

The category-theoretic solution of recursive program schemes

Stefan Milius
Lawrence S. Moss

This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with “enough final coalgebras” we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme.

I&C Journal 2005 Journal Article

Completely iterative algebras and completely iterative monads

Stefan Milius

Completely iterative theories of Calvin Elgot formalize (potentially infinite) computations as solutions of recursive equations. One of the main results of Elgot and his coauthors is that infinite trees form a free completely iterative theory. Their algebraic proof of this result is extremely complicated. We present completely iterative algebras as a new approach to the description of free completely iterative theories. Examples of completely iterative algebras include algebras on complete metric spaces. It is shown that a functor admits an initial completely iterative algebra iff it has a final coalgebra. The monad given by free completely iterative algebras is proved to be the free completely iterative monad on the given endofunctor. This simplifies substantially all previous descriptions of these monads. Moreover, the new approach is much more general than the classical one of Elgot et al. A necessary and sufficient condition for the existence of a free completely iterative monad is proved.

TCS Journal 2004 Journal Article

On coalgebra based on classes

Jiřı́ Adámek
Stefan Milius
Jiřı́ Velebil

The category Class of classes and functions is proved to have a number of properties suitable for algebra and coalgebra: every endofunctor is set-based, it has an initial algebra and a terminal coalgebra, the categories of algebras and coalgebras are complete and cocomplete, and every endofunctor generates a free completely iterative monad. A description of a terminal coalgebra for the power-set functor is provided.

TCS Journal 2003 Journal Article

Infinite trees and completely iterative theories: a coalgebraic view

Peter Aczel
Jiřı́ Adámek
Stefan Milius
Jiřı́ Velebil

Infinite trees form a free completely iterative theory over any given signature—this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(_)+X, then those coalgebras, TX, form a monad. This monad is completely iterative, i. e. , every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees. This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H⊗_+I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.