# Publications of Stefan Milius

You may also want to check my DBLP page.

Click on titles to see abstracts and pdf's.

Filter by publication type: All () Journal () Conference () Edited () Other ()

## 2016

Regular Behaviours with Names: On Rational Fixpoints of Endofunctors on Nominal Sets
Appl. Categ. Structures, vol. 24 (5), pp. 663-701, 2016.

## Abstract

Nominal sets provide a framework to study key notions of syntax and semantics such as fresh names, variable binding and $\alpha$-equivalence on a conveniently abstract categorical level. Coalgebras for endofunctors on nominal sets model, e.g., various forms of automata with names as well as infinite terms with variable binding operators (such as $\lambda$-abstraction). Here, we first study the behaviour of orbit-finite coalgebras for functors $\bar F$ on nominal sets that lift some finitary set functor $F$. We provide sufficient conditions under which the rational fixpoint of~$\bar F$, i.e.~the collection of all behaviours of orbit-finite $\bar F$-coalgebras, is the lifting of the rational fixpoint of~$F$. Second, we describe the rational fixpoint of the quotient functors: we introduce the notion of a sub-strength of an endofunctor on nominal sets, and we prove that for a functor $G$ with a sub-strength the rational fixpoint of each quotient of $G$ is a canonical quotient of the rational fixpoint of $G$. As applications, we obtain a concrete description of the rational fixpoint for functors arising from so-called binding signatures with exponentiation, such as those arising in coalgebraic models of infinitary $\lambda$-terms and various flavours of automata.

## Bibtex

@article{msw16, author = {Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann}, title = {Regular Behaviours with Names: On Rational Fixpoints of Endofunctors on Nominal Sets}, journal = {Appl. Categ. Structures}, year = {2016}, volume = {24}, number = {5}, pages = {663--701}, }
A New Foundation for Finitary Corecursion: The Locally Finite Fixpoint and its Properties
In: Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16),
Lecture Notes Comput. Sci. (ARCoSS), vol. 9634, pp. 107-125.

## Abstract

This paper contributes to a theory of the behaviour of "finite-state" systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint} (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius and Velebil). Moreover, we show that the LFF is characterized by two universal properties: 1. as the final locally finitely generated coalgebra, and 2. as the initial fg-iterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal power-series, regular trees etc. And we obtain a number of new examples, e.g.~(realtime deterministic resp.~non-deterministic) context-free languages, constructively $S$-algebraic formal power-series (and any other instance of the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten) and the monad of Courcelle's algebraic trees.

## Bibtex

@inproceedings{mpw16, author = {Stefan Milius and Dirk Pattinson and Thorsten Wißmann}, title = {A New Foundation for Finitary Corecursion: The Locally Finite Fixpoint and its Properties}, booktitle = {Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16)}, year = {2016}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {9634}, pages = {107--125}, }
Profinite Monads, Profinite Equationa and Reitermann's Theorem
In: Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16),
Lecture Notes Comput. Sci. (ARCoSS), vol. 9634, pp. 531-547.

## Abstract

Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman's theorem states that they precisely specify pseudovarieties, i.e. classes of finite algebras closed under finite products, subalgebras and quotients. In this paper Reiterman's theorem is generalised to finite Eilenberg-Moore algebras for a monad T on a variety D of (ordered) algebras: a class of finite T-algebras is a pseudovariety iff it is presentable by profinite (in-)equations. As an application, quasivarieties of finite algebras are shown to be presentable by profinite implications. Other examples include finite ordered algebras, finite categories, finite $\infty$-monoids, etc.

## Bibtex

@inproceedings{acmu16, author = {Liang-Ting Chen and Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat}, title = {Profinite Monads, Profinite Equationa and Reitermann's Theorem}, booktitle = {Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16)}, year = {2016}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {9634}, pages = {531--547}, }

## 2015

Rob Myers, Jiří Adámek, Stefan Milius and Henning Urbat
Coalgebraic Constructions of Canonical Nondeterministic Automata
Theoret. Comput. Sci., vol. 604, pp. 81-101, 2015. Journal version of CMCS'14 conference paper below.

## Abstract

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₂-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.

## Bibtex

@article{mamu15, author = {Rob Myers and Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat}, title = {Coalgebraic Constructions of Canonical Nondeterministic Automata}, journal = {Theoret. Comput. Sci.}, year = {2015}, volume = {604}, pages = {81--101}, }
Killing Epsilons with a Dagger: A Coalgebraic Study of Systems with Algebraic Label Structure
Theoret. Comput. Sci., vol. 604, pp. 102-126, 2015. Journal version of CMCS'14 conference paper below.

## Abstract

We propose an abstract framework for modeling 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.

## Bibtex

@article{bmsz15, author = {Filippo Bonchi and Stefan Milius and Alexandra Silva and Fabio Zanasi}, title = {Killing Epsilons with a Dagger: A Coalgebraic Study of Systems with Algebraic Label Structure}, journal = {Theoret. Comput. Sci.}, year = {2015}, volume = {604}, pages = {102--126}, }
Syntactic Monoids in a Category
In: Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 35, pp. 1-16.

## Abstract

The syntactic monoid of a language is generalized to the level of a symmetric monoidal closed category D. This allows for a uniform treatment of several notions of syntactic algebras known in the literature, including the syntactic monoids of Rabin and Scott (D = sets), the syntactic semirings of Pol\'ak (D = semilattices), and the syntactic associative algebras of Reutenauer (D = vector spaces). Assuming that D is a commutative variety of algebras, we prove that the syntactic D-monoid of a language L can be constructed as a quotient of a free D-monoid modulo the syntactic congruence of L, and that it is isomorphic to the transition D-monoid of the minimal automaton for L in D. Furthermore, in the case where the variety D is locally finite, we characterize the regular languages as precisely the languages with finite syntactic D-monoids.

## Bibtex

@inproceedings{amu15, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat}, title = {Syntactic Monoids in a Category}, booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)}, year = {2015}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {35}, pages = {1--16}, }
Finitary Corecursion for the Infinitary Lambda Calculus
In: Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 35, pp. 336-351.

## Abstract

Kurz et al. have recently shown that infinite λ-trees with finitely many free variables modulo α-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational λ-trees, i.e. those λ-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational λ-trees.

## Bibtex

@inproceedings{mw15, author = {Stefan Milius and Thorsten Wißmann}, title = {Finitary Corecursion for the Infinitary Lambda Calculus}, booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)}, year = {2015}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {35}, pages = {336--351}, }
In: Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 35, pp. 253-269.

## Bibtex

@inproceedings{mps15, author = {Stefan Milius and Dirk Pattinson and Lutz Schr\"oder}, title = {Generic Trace Semantics and Graded Monads}, booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)}, year = {2015}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {35}, pages = {253--269}, }
Jiří Adámek, Stefan Milius, Rob Myers and Henning Urbat
Varieties of Languages in a Category
In: Proc. 30th Annual Symposium on Logic in Computer Science (LICS'15), pp. 414-425.

## Abstract

Eilenberg's variety theorem, a centerpiece of algebraic automata theory, establishes a bijective correspondence between varieties of languages and pseudovarieties of monoids. In the present paper this result is generalized to an abstract pair of algebraic categories: we introduce varieties of languages in a category C, and prove that they correspond to pseudovarieties of monoids in a closed monoidal category D, provided that C and D are dual on the level of finite objects. By suitable choices of these categories our result uniformly covers Eilenberg's theorem and three variants due to Pin, Polák and Reutenauer, respectively, and yields new Eilenberg-type correspondences.

## Bibtex

@inproceedings{ammu15, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat}, title = {Varieties of Languages in a Category}, booktitle = {Proc. 30th Annual Symposium on Logic in Computer Science (LICS'15)}, year = {2015}, pages = {414--425}, }
Simplified Coalgebraic Trace Equivalence
In: Software, Services, and Systems: Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of Programming and Software Engineering,
Lecture Notes Comput. Sci., vol. 8950, pp. 75-90.

## Abstract

The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. labelled transition systems. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard and probabilistic labelled transition systems.

## Bibtex

@inproceedings{, author = {Alexander Kurz and Stefan Milius and Dirk Pattinson and Lutz Schr\"oder}, title = {Simplified Coalgebraic Trace Equivalence}, booktitle = {Software, Services, and Systems: Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of Programming and Software Engineering}, year = {2015}, series = {Lecture Notes Comput. Sci.}, volume = {8950}, pages = {75--90}, }
On Finitary Functors and Their Presentations
J. Comput. System Sci., vol. 81 (5), pp. 813-833, 2015. Journal version of CMCS'12 conference paper below.

## Abstract

Finitary endofunctors of locally presentable categories are proved to have equational presentations. Special attention is paid to the category of complete metric spaces and two endofunctors: the Hausdorff functor of all compact subsets and the Kantorovich functor of all tight measures.

## Bibtex

@article{ammu14, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss and Henning Urbat}, title = {On Finitary Functors and Their Presentations}, journal = {J. Comput. System Sci.}, year = {2015}, volume = {81}, number = {5}, pages = {813--833}, }

## 2014

Jiří Adámek, Stefan Milius, Rob Myers and Henning Urbat
On Continuous Nondeterminism and State Minimality
In: Proc. 30th Conference on Mathematical Foundations of Programming Science (MFPS XXX),
Electron. Notes Theor. Comput. Sci., vol. 308, pp. 3-23.

## Abstract

This paper is devoted to the study of nondeterministic closure automata, that is, nondeterministic finite automata (nfas) equipped with a strict closure operator on the set of states and continuous transition structure. We prove that for each regular language L there is a unique minimal nondeterministic closure automaton whose underlying nfa accepts L. Here minimality means no proper sub or quotient automata exist, just as it does in the case of minimal dfas. Moreover, in the important case where the closure operator of this machine is topological, its underlying nfa is shown to be state-minimal. The basis of these results is an equivalence between the categories of finite semilattices and finite strict closure spaces.

## Bibtex

@inproceedings{ammu14_2, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat}, title = {On Continuous Nondeterminism and State Minimality}, booktitle = {Proc. 30th Conference on Mathematical Foundations of Programming Science (MFPS XXX)}, year = {2014}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {308}, pages = {3--23}, }
Log. Methods Comput. Sci., vol. 10 (3:19), 51 pp., 2014.

## Abstract

An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it. We prove that free corecursive algebras are obtained as coproducts of the terminal coalgebra (considered as an algebra) and free algebras. The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.

## Bibtex

@article{ahm14, author = {Ji\v{r}\'i Ad\'amek and Mahdieh Haddadi and Stefan Milius}, title = {Corecursive Algebras, Corecursive Monads and Bloom Monads}, journal = {Log. Methods Comput. Sci.}, year = {2014}, volume = {10}, number = {3:19}, pages = {51 pp.}, }
On Final Coalgebras of Power-Set Functors and Saturated Trees
Appl. Categ. Structures, vol. ??? (???), 29 pp., 2014. doi: 10.1007/s10485-014-9372-9.

## Abstract

The final coalgebra for the finite power-set functor was described by Worrell who also proved that the final chain converges in omega + omega steps. We describe the step omega as the set of saturated trees, a concept equivalent to the modally saturated trees introduced by K. Fine in the 1970s in his study of modal logic. And for the bounded power-set functors P_lambda, where lambda is an infinite regular cardinal, we prove that the construction needs precisely lambda+omega steps. We also generalize Worrell's result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor M_f studied by H.-P. Gumm and T. Schröder. We describe the final chain of the power-set functor by introducing the concept of i-saturated tree for all ordinals i, and then prove that for i of cofinality omega, the i-th step in the final chain consists of all i-saturated, strongly extensional trees.

## Bibtex

@article{amms14, author = {Ji\v{r}\'i Ad\'amek and Paul B. Levy and Stefan Milius and Lawrence S. Moss and Lurdes Sousa}, title = {On Final Coalgebras of Power-Set Functors and Saturated Trees}, journal = {Appl. Categ. Structures}, year = {2014}, volume = {???}, number = {???}, pages = {29 pp.}, }
Towards a Coalgebraic Chomsky Hierarchy (Extended Abstract)
In: Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS'14),
Lecture Notes Comput. Sci., vol. 8705, pp. 265-280.

## Abstract

The Chomsky hierarchy plays a prominent role in the foundations of theoretical computer science relating classes of formal languages of primary importance. In this paper we use recent developments on coalgebraic and monad-based semantics to obtain a generic notion of a T-automaton, where T is a monad, which allows the uniform study of various notions of machines (e.g.~finite state machines, multi-stack machines, Turing machines, valence automata, weighted automata). We use the generalized powerset construction to define a generic (trace) semantics for $\BBT$-automata, and we show by numerous examples that it correctly instantiates for some known classes of machines/languages captured by the Chomsky hierarchy. Moreover, our approach provides new generic techniques for studying expressivity power of various machine-based models.

## Bibtex

@inproceedings{gms14, author = {Sergey Goncharov and Stefan Milius and Alexandra Silva}, title = {Towards a Coalgebraic Chomsky Hierarchy (Extended Abstract)}, booktitle = {Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS'14)}, year = {2014}, series = {Lecture Notes Comput. Sci.}, volume = {8705}, pages = {265--280}, }
An Open Alternative for SMT-based Verification of SCADE Models
In: Proc. 19th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'14),
Lecture Notes Comput. Sci., vol. 6959, pp. 124-139.

## Abstract

SCADE is an industrial strength synchronous language and tool suite for the development of the software of safety-critical systems. It supports formal verification using the so-called Design Verifier. Here we start developing a freely available alternative to the Design Verifier intended to support the academic study of verification techniques tailored for SCADE programs. Inspired by work of Hagen and Tinelli on the SMT-based verification of LUSTRE programs, we develop an SMT-based verification method for \SCADE programs. We introduce Lama as an intermediate language into which SCADE programs can be translated and which easily can be translated to SMT solver instances. We also present first experimental results of our approach using the SMT solver Z3.

## Bibtex

@inproceedings{bhmg14, author = {Henning Basold and Michaela Huhn and Stefan Milius and Henning G\"unther}, title = {An Open Alternative for SMT-based Verification of SCADE Models}, booktitle = {Proc. 19th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'14)}, year = {2014}, series = {Lecture Notes Comput. Sci.}, volume = {6959}, pages = {124--139}, }
Base modules for parametrized iterativity
Theoret. Comput. Sci., vol. 523, pp. 56-85, 2014. doi: 10.1016/j.tcs.2013.12.019.

## Abstract

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 $\Sigma$-algebras whose rational monad is the monad of rational $\Sigma$-trees and that was characterized by Calvin Elgot et al. as the free iterative monad on $\Sigma$. A basic parametrized example is the base assigning to every parameter set $X$ the monad $A\mapsto X^*\times 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^*\times X)\times A\to X^*\times A$ given by parametrized concatenation.

## Bibtex

@article{amv14, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Base modules for parametrized iterativity}, journal = {Theoret. Comput. Sci.}, year = {2014}, volume = {523}, pages = {56--85}, }
Rob Myers, Jiří Adámek, Stefan Milius and Henning Urbat
Canonical Nondeterministic Automata
In: Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science (CMCS'14),
Lecture Notes Comput. Sci., vol. 8446, pp. 189-210.

## Abstract

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 finite V-algebras and a category of finite structured sets and relations. By instantiating this to different varieties we recover three well-studied canonical nfas (the átomaton, the jiromaton and the minimal xor automaton) and obtain a new canonical nfa called the distromaton. We prove that each of these nfas is minimal relative to a suitable measure, and give conditions for state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties.

## Bibtex

@inproceedings{mamu14, author = {Rob Myers and Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat}, title = {Canonical Nondeterministic Automata}, booktitle = {Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science (CMCS'14)}, year = {2014}, series = {Lecture Notes Comput. Sci.}, volume = {8446}, pages = {189--210}, }
How to Kill Epsilons With a Dagger: A Coalgebraic Take on Systems with Algebraic Label Structure
In: Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science (CMCS'14),
Lecture Notes Comput. Sci., vol. 8446, pp. 53-74.

## Abstract

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or epsilon-transitions. Our approach employs monads with a parametrized fixpoint operator dagger 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.

## Bibtex

@inproceedings{bmsz14, author = {Filippo Bonchi and Stefan Milius and Alexandra Silva and Fabio Zanasi}, title = {How to Kill Epsilons With a Dagger: A Coalgebraic Take on Systems with Algebraic Label Structure}, booktitle = {Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science (CMCS'14)}, year = {2014}, series = {Lecture Notes Comput. Sci.}, volume = {8446}, pages = {53--74}, }
Jiří Adámek, Stefan Milius, Rob Myers and Henning Urbat
Generalized Eilenberg Theorem I: Local Varieties of Languages
In: Proc. Seventeenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14),
Lecture Notes Comput. Sci. (ARCoSS), vol. 8412, pp. 366-380.

## Abstract

We investigate the duality between algebraic and coalgebraic recognition of languages to derive a generalization of the local version of Eilenberg's theorem. This theorem states that the lattice of all boolean algebras of regular languages over an alphabet $\Sigma$ closed under derivatives is isomorphic to the lattice of all pseudovarieties of $\Sigma$-generated monoids. By applying our method to different categories, we obtain three related results: one, due to Gehrke, Grigorieff and Pin, weakens boolean algebras to distributive lattices, one due to Polák weakens them to join-semilattices, and the last one considers vector spaces over $Z_2$.

## Bibtex

@inproceedings{ammu14_3, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat}, title = {Generalized Eilenberg Theorem I: Local Varieties of Languages}, booktitle = {Proc. Seventeenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14)}, year = {2014}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {8412}, pages = {366--380}, }
Observations on Formal Safety Analysis in Industrial Practice
Sci. Comput. Programming, vol. 80A (Part A), pp. 150-168, 2014. doi: 10.1016/j.scico.2013.01.001.

## Abstract

We report on the application of formal verification in the safety analysis of two level crossing controllers that were industrially designed using SCADE Suite. Although the theoretical grounds for formalizing safety analysis have been developed in recent years, we faced numerous and intense complexity problems even with these medium size industrial case studies. The complexity problems constricted formal verification and even remained after employing different heuristics based on abstraction and introducing environmental models. In addition, we found that the modeling style has a significant impact on the complexity of the verification tasks. We finally succeeded to formally classify all relevant fault combinations as either critical or uncritical by identifying a crucial, design-specific liveness property.

## Bibtex

@article{hm14, author = {Michaela Huhn and Stefan Milius}, title = {Observations on Formal Safety Analysis in Industrial Practice}, journal = {Sci. Comput. Programming}, year = {2014}, volume = {80A}, number = {Part A}, pages = {150--168}, }

## 2013

Reiko Heckel and Stefan Milius (editors)
Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013 (Proceedings)
Lecture Notes in Computer Science, vol. 8089, 2013.

## Bibtex

@proceedings{calco13, editor = {Reiko Heckel and Stefan Milius}, title = {Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013 (Proceedings)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, year = {2013}, volume = {8089}, number = {}, pages = {}, }
Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion
In: Proc. Fixed Points in Computer Science (FICS'13),
Electron. Proc. Theoret. Comput. Sci., vol. 126, pp. 72-86.

## Abstract

Motivated by the recent interest in models of guarded recursion we study the equational properties of guarded fixpoint operators. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and \'Esik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading to the description of classifying theories for guarded recursion and hence completeness results involving our axioms of guarded fixpoint operators in future work.

## Bibtex

@inproceedings{ml13, author = {Stefan Milius and Tadeusz Litak}, title = {Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion}, booktitle = {Proc. Fixed Points in Computer Science (FICS'13)}, year = {2013}, series = {Electron. Proc. Theoret. Comput. Sci.}, volume = {126}, pages = {72--86}, }
Stefan Milius, Marcello Bonsangue, Rob Myers and Jurriaan Rot
Rational Operational Models
In: Proc. 29th Conference on Mathematical Foundations of Programming Science (MFPS XXIX),
Electron. Notes Theor. Comput. Sci., vol. 298, pp. 257-282.

## Abstract

GSOS is a specification format for well-behaved operations on transition systems. Aceto introduced a restriction of this format, called \emph{simple GSOS}, which guarantees that the associated transition system is locally finite, i.e. every state has only finitely many different successors. The theory of \emph{coalgebras} provides a framework for the uniform study of systems, including labelled transition systems but also, e.g. weighted transition systems and (non-)deterministic automata. In this context GSOS can be studied at the general level of distributive laws of syntax over behaviour. In the present paper we generalize Aceto's result to the setting of coalgebras by restricting abstract GSOS to \emph{bipointed specifications}. We show that the operational model of a bipointed specification is locally finite, even for specifications with infinitely many operations which have finite dependency. As an example, we derive a concrete format for operations on regular languages and obtain for free that regular expressions have finitely many derivatives modulo the equations of join semilattices.

## Bibtex

@inproceedings{mbmr13, author = {Stefan Milius and Marcello Bonsangue and Rob Myers and Jurriaan Rot}, title = {Rational Operational Models}, booktitle = {Proc. 29th Conference on Mathematical Foundations of Programming Science (MFPS XXIX)}, year = {2013}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {298}, pages = {257--282}, }
Abstract GSOS rules and a Modular Treatment of Recursive Definitions
Log. Methods Comput. Sci., vol. 9 (3:28), 52 pp., 2013.

## Abstract

Terminal coalgebras for a functor serve as semantic domains for state-based systems of various types. For example, behaviors of CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present a uniform account of the semantics of recursive definitions in terminal coalgebras by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial completely iterative algebras (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle modularity. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.\,g., a finite stream circuit defines a unique stream function.

## Bibtex

@article{mms13, author = {Stefan Milius and Lawrence S. Moss and Daniel Schwencke}, title = {Abstract GSOS rules and a Modular Treatment of Recursive Definitions}, journal = {Log. Methods Comput. Sci.}, year = {2013}, volume = {9}, number = {3:28}, pages = {52 pp.}, }
Well-pointed Coalgebras
Log. Methods Comput. Sci., vol. 9 (3:2), 51 pp., 2013.

## Abstract

For endofunctors of varieties preserving intersections, a new description of the final coalgebra and the initial algebra is presented: the former consists of all well-pointed coalgebras. These are the pointed coalgebras having no proper subobject and no proper quotient. The initial algebra consists of all well-pointed coalgebras that are well-founded in the sense of Osius and Taylor. And initial algebras are precisely the final well-founded coalgebras. Finally, the initial iterative algebra consists of all finite well-pointed coalgebras. Numerous examples are discussed e.g. automata, graphs, and labeled transition systems.

## Bibtex

@article{amms13, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss and Lurdes Sousa}, title = {Well-pointed Coalgebras}, journal = {Log. Methods Comput. Sci.}, year = {2013}, volume = {9}, number = {3:2}, pages = {51 pp.}, }
How iterative reflections of monads are constructed
Inform. and Comput., vol. 225, pp. 83-118, 2013. doi: 10.1016/j.ic.2013.02.003.

## Abstract

Every ideal monad M on the category of sets is known to have a reflection $\bar M$ in the category of all iterative monads of Elgot. Here we describe the iterative reflection $\bar 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 $\bar M$ is obtained by adding a single absorbing element; if M is the monad of finite trees then $\bar M$ is the monad of rational trees, etc.

## Bibtex

@article{amv_refl2_13, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {How iterative reflections of monads are constructed}, journal = {Inform. and Comput.}, year = {2013}, volume = {225}, pages = {83--118}, }
Sound and complete axiomatizations of coalgebraic language equivalence
ACM Trans. Comput. Log., vol. 14 (1:7), 52 pp., 2013.

## Abstract

Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalised powerset construction. We illustrate the framework with two examples: non-deterministic automata, for which we recover Rabinovich’s sound and complete calculus for language equivalence, and weighted automata, for which we present the first sound and complete calculus for weighted language equivalence.

## Bibtex

@article{bms13, author = {Marcello Bonsangue and Stefan Milius and Alexandra Silva}, title = {Sound and complete axiomatizations of coalgebraic language equivalence}, journal = {ACM Trans. Comput. Log.}, year = {2013}, volume = {14}, number = {1:7}, pages = {52 pp.}, }

## 2012

On the Formal Verification of Systems of Synchronous Software Components
In: Proc. 31st International Conference on Computer Safety, Reliability and Security (SafeComp'12),
Lecture Notes Comput. Sci., vol. 7612, pp. 291-304.

## Abstract

Large asynchronous systems composed from synchronous components (so called GALS—globally asynchronous, locally synchronous—systems) pose a challenge to formal verification. We present an approach which abstracts components with contracts capturing the behavior by a mixture of temporal logic formulas and non-deterministic state machines. Formal verification of global system properties is then done transforming a network of contracts to model checking tools such as PROMELA/SPIN or UPPAAL. Synchronous components are implemented in SCADE, and contract validation is done using the SCADE Design Verifier for formal verification. We also discuss first experiences from an ongoing industrial case study applying our approach.

## Bibtex

@inproceedings{gmm12, author = {Henning G\"unther and Stefan Milius and M. Oliver M\"oller}, title = {On the Formal Verification of Systems of Synchronous Software Components}, booktitle = {Proc. 31st International Conference on Computer Safety, Reliability and Security (SafeComp'12)}, year = {2012}, series = {Lecture Notes Comput. Sci.}, volume = {7612}, pages = {291--304}, }
On the specification of operations on the rational behaviour of systems
In: Proc. Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics (EXPRESS/SOS'12),
Electron. Proc. Theoret. Comput. Sci., vol. 89, pp. 3-18.

## Abstract

Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields specification formats for well-behaved algebraic operations on final coalgebras, which are a domain for the behaviour of all systems of a given type functor. We introduce a format for specification of algebraic operations that restrict to the rational fixpoint of a functor, which captures the behaviour of \emph{finite} systems. In other words, we show that rational behaviour is closed under operations specified in our format. As applications we consider operations on regular languages, regular processes and finite weighted transition systems.

## Bibtex

@inproceedings{bmr12, author = {Marcello Bonsangue and Stefan Milius and Jurriaan Rot}, title = {On the specification of operations on the rational behaviour of systems}, booktitle = {Proc. Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics (EXPRESS/SOS'12)}, year = {2012}, series = {Electron. Proc. Theoret. Comput. Sci.}, volume = {89}, pages = {3--18}, }
Jiří Adámek, Nathan Bowler, Paul B. Levy and Stefan Milius
In: Proc. 27th Annual Symposium on Logic in Computer Science (LICS'12), pp. 45-54.

## Abstract

Coproducts of monads on Set have arisen in both the study of computational effects and universal algebra. We describe coproducts of consistent monads on Set by an initial algebra formula, and prove also the converse: if the coproduct exists, so do the required initial algebras. That formula was, in the case of ideal monads, also used by Ghani and Uustalu. We deduce that coproduct embeddings of consistent monads are injective; and that a coproduct of injective monad morphisms is injective.
Two consistent monads have a coproduct iff either they have arbitrarily large common fixpoints, or one is an exception monad, possibly modified to preserve the empty set. Hence a consistent monad has a coproduct with every monad iff it is an exception monad, possibly modified to preserve the empty set. We also show other fixpoint results, including that a functor (not constant on nonempty sets) is finitary iff every sufficiently large cardinal is a fixpoint.

## Bibtex

@inproceedings{ablm12, author = {Ji\v{r}\'i Ad\'amek and Nathan Bowler and Paul B. Levy and Stefan Milius}, title = {Coproducts of Monads on Set}, booktitle = {Proc. 27th Annual Symposium on Logic in Computer Science (LICS'12)}, year = {2012}, pages = {45--54}, }
On Finitary Functors and Their Presentations
In: Proc. Eleventh International Workshop on Coalgebraic Methods in Computer Science (CMCS'12),
Lecture Notes Comput. Sci., vol. 7399, pp. 51-70.

## Abstract

Finitary endofunctors of locally presentable categories are proved to have equational presentations. Special attention is paid to the Hausdorff functor of non-empty compact subsets of a complete metric space.

## Bibtex

@inproceedings{amm12, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss}, title = {On Finitary Functors and Their Presentations}, booktitle = {Proc. Eleventh International Workshop on Coalgebraic Methods in Computer Science (CMCS'12)}, year = {2012}, series = {Lecture Notes Comput. Sci.}, volume = {7399}, pages = {51--70}, }
A coalgebraic perspective on minimization and determinization
In: Proc. Fifteenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'12),
Lecture Notes Comput. Sci. (ARCoSS), vol. 7213, pp. 58-73.

## Abstract

Coalgebra offers a unified theory of state based systems, including infinite streams, labelled transition systems and deterministic automata. In this paper, we use the coalgebraic view on systems to derive, in a uniform way, abstract procedures for checking behavioural equivalence in coalgebras, which perform (a combination of) minimization and determinization. First, we show that for coalgebras in categories equipped with factorization structures, there exists an abstract procedure for equivalence checking. Then, we consider coalgebras in categories without suitable factorization structures: under certain conditions, it is possible to apply the above procedure after transforming coalgebras with reflections. This transformation can be thought of as some kind of determinization. We will apply our theory to the following examples: conditional transition systems and (non-deterministic) automata.

## Bibtex

@inproceedings{ABHKMS12, author = {Ji\v{r}\'i Ad\'amek and Filippo Bonchi and Mathias H\"ulsbusch and Barbara K\"onig and Stefan Milius and Alexandra Silva}, title = {A coalgebraic perspective on minimization and determinization}, booktitle = {Proc. Fifteenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'12)}, year = {2012}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {7213}, pages = {58--73}, }
Well-pointed Coalgebras (Extended Abstract)
In: Proc. Fifteenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'12),
Lecture Notes Comput. Sci. (ARCoSS), vol. 7213, pp. 89-103.

## Abstract

For set functors preserving intersections, a new description of the final coalgebra and the initial algebra is presented: the former consists of all well-pointed coalgebras. These are the pointed coalgebras having no proper subobject and no proper quotient. And the initial algebra consists of all well-pointed coalgebras that are well-founded in the sense of Taylor. Finally, the initial iterative algebra consists of all finite well-pointed coalgebras. Numerous examples are discussed e.g. automata, graphs, and labeled transition systems.

## Bibtex

@inproceedings{amms12, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss and Lurdes Sousa}, title = {Well-pointed Coalgebras (Extended Abstract)}, booktitle = {Proc. Fifteenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'12)}, year = {2012}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {7213}, pages = {89--103}, }
Henning Günther, Ramin Hedayati, Helge Löding, Stefan Milius, M. Oliver Möller, Jan Peleska, Martin Sulzmann and Axel Zechner
A framework for formal verification of systems of synchronous components
In: Proc. Eighth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2012).

## Abstract

Large asynchronous systems composed from synchronous components (so called \GALS-globally asynchronous, locally synchronous-systems) pose a challenge to formal verification. We present an approach which abstracts components with contracts capturing the behavior in a rely-guarantee style logic. Formal verification of global system properties is then done transforming a network of contracts to PROMELA/SPIN. Synchronous components are implemented in SCADE, and contract validation is done by transforming the contracts into synchronous observers and using the \SCADE Design Verifier for formal verification. We also discuss first experiences from an ongoing industrial case study applying our approach.

## Bibtex

@inproceedings{g_etal_12, author = {Henning G\"unther and Ramin Hedayati and Helge L\"oding and Stefan Milius and M. Oliver M\"oller and Jan Peleska and Martin Sulzmann and Axel Zechner}, title = {A framework for formal verification of systems of synchronous components}, booktitle = {Proc. Eighth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2012)}, year = {2012}, pages = {}, }

## 2011

From Corecursive Algebras to Corecursive Monads
In: Proc. 4th Conference on Algebra and Coalgebra in Computer Science (CALCO'11),
Lecture Notes Comput. Sci., vol. 6859, pp. 55-69.

## Abstract

An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it. We prove that free corecursive algebras are obtained as a coproduct of the final coalgebra (considered as an algebra) and free algebras. The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.

## Bibtex

@inproceedings{ahm11, author = {Ji\v{r}\'i Ad\'amek and Mahdieh Haddadi and Stefan Milius}, title = {From Corecursive Algebras to Corecursive Monads}, booktitle = {Proc. 4th Conference on Algebra and Coalgebra in Computer Science (CALCO'11)}, year = {2011}, series = {Lecture Notes Comput. Sci.}, volume = {6859}, pages = {55--69}, }
Power-Set Functors and Saturated Trees
In: Proc. 20th Conference on Computer Science Logic (CSL'11),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 12, pp. 5-19.

## Abstract

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).

## Bibtex

@inproceedings{amms11, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss}, title = {Power-Set Functors and Saturated Trees}, booktitle = {Proc. 20th Conference on Computer Science Logic (CSL'11)}, year = {2011}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {12}, pages = {5--19}, }
Theoret. Comput. Sci., vol. 412 (38), pp. 4969-4988, 2011.

## Abstract

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.

## Bibtex

@article{amv_secalg, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {On second-order iterative monads}, journal = {Theoret. Comput. Sci.}, year = {2011}, volume = {412}, number = {38}, pages = {4969--4988}, }
Semantics of higher-order recursion schemes
Log. Methods Comput. Sci., vol. 7 (1:15), 43 pp., 2011.

## Abstract

Higher-order recursion schemes are recursive equations defining new operations from given ones called terminals''. Every such recursion scheme is proved to have a least interpreted semantics in every Scott's model of λ-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite λ-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Fiore et al showed how to capture the type of variable binding in λ-calculus by an endofunctor H_λ and they explained simultaneous substitution of λ-terms by proving that the presheaf of λ-terms is an initial H_λ-monoid. Here we work with the presheaf of rational infinite λ-terms and prove that this is an initial iterative H_λ-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in this monoid.

## Bibtex

@article{amv_highord, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Semantics of higher-order recursion schemes}, journal = {Log. Methods Comput. Sci.}, year = {2011}, volume = {7}, number = {1:15}, pages = {43 pp.}, }
Elgot theories: a new perspective of the equational properties of iteration
Math. Structures Comput. Sci., vol. 21 (2), pp. 417-480, 2011. © Cambridge University Press.

## Abstract

The concept of iteration theory of Bloom and Ésik summarizes all equational properties that iteration has in usual applications, e.g., in Domain Theory where to every system of recursive equations the least solution is assigned. This paper shows that in the more general coalgebraic approach to iteration the more suitable concept is that of a functorial iteration theory (called Elgot theory). These theories have a particularly simple axiomatization, and all well-known examples of iteration theories are functorial. Elgot theories are proved to be monadic over the category of sets in context (or, more generally, the category of finitary endofunctors of a locally finitely presentable category). This demonstrates that functoriality is an equational property from the perspective of sets in context. In contrast, Bloom and Ésik worked in the base category of signatures in lieu of sets in context, where iteration theories are monadic but Elgot theories are not. This explains why functoriality was not included into the definition of iteration theories.

## Bibtex

@article{amv_em2, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot theories: a new perspective of the equational properties of iteration}, journal = {Math. Structures Comput. Sci.}, year = {2011}, volume = {21}, number = {2}, pages = {417--480}, }
Ilyas Daskaya, Michaela Huhn and Stefan Milius
Formal Safety Analysis in Industrial Practice
In: Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'11),
Lecture Notes Comput. Sci., vol. 6959, pp. 68-84.

## Abstract

We report on a comparative study on formal verification of two level crossing controllers that were developed using SCADE by a rail automation manufacturer. Deductive Cause-Consequence Analysis of Ortmeier et al. is applied for formal safety analysis and in addition, safety requirements are proven. Even with these medium size industrial case studies we observed intense complexity problems that could not be overcome by employing different heuristics like abstraction and compositional verification. In particular, we failed to prove a crucial liveness property within the SCADE framework stating that an unsafe state will not be persistent. We finally succeeded to prove this property by combining abstraction and model transformation from SCADE to UPPAAL timed automata. In addition, we found that the modeling style has a significant impact on the complexity of the verification task.

## Bibtex

@inproceedings{dhm11, author = {Ilyas Daskaya and Michaela Huhn and Stefan Milius}, title = {Formal Safety Analysis in Industrial Practice}, booktitle = {Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'11)}, year = {2011}, series = {Lecture Notes Comput. Sci.}, volume = {6959}, pages = {68--84}, }

## 2010

Recursive Program Schemes and Context-Free Monads
In: Proc. Coalgebraic Methods in Computer Science (CMCS'10),
Electron. Notes Theor. Comput. Sci., vol. 264, pp. 3-23.

## Abstract

Solutions of recursive program schemes over a given signature Σ were characterized by Bruno Courcelle as precisely the context-free (or algebraic) Σ-trees. These are the finite and infinite Σ-trees yielding, via labelling of paths, context-free languages. Our aim is to generalize this to finitary endofunctors H of general categories: we construct a monad C^H “generated” by solutions of recursive program schemes of type H, and prove that this monad is ideal. In case of polynomial endofunctors of Set our construction precisely yields the monad of context-free Σ-trees of Courcelle. Our result builds on a result by N. Ghani et al on solutions of algebraic systems.

## Bibtex

@inproceedings{amv_algtrees, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Recursive Program Schemes and Context-Free Monads}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'10)}, year = {2010}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {264}, pages = {3--23}, }
Math. Structures Comput. Sci., vol. 20 (3), pp. 419-452, 2010. © Cambridge University Press.

## Abstract

Iterative monads were introduced by Calvin Elgot in the 1970’s and are those ideal monads in which every guarded system of recursive equations has a unique solution. We prove that every ideal monad M has an iterative reflection, that is, an embedding into an iterative monad with the expected universal property. We also introduce the concept of iterativity for algebras for the monad M, following in the footsteps of Evelyn Nelson and Jerzy Tiuryn, and prove that M is iterative if and only if all free algebras for M are iterative algebras.

## Bibtex

@article{amv_ref, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative reflections of monads}, journal = {Math. Structures Comput. Sci.}, year = {2010}, volume = {20}, number = {3}, pages = {419--452}, }
Inform. and Comput., vol. 208 (12), pp. 1306-1348, 2010.

## Abstract

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.

## Bibtex

@article{amv_em1, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Equational Properties of Iterative Monads}, journal = {Inform. and Comput.}, year = {2010}, volume = {208}, number = {12}, pages = {1306--1348}, }
Stefan Milius
A Sound and Complete Calculus for finite Stream Circuits
In: Proc. 25th Annual Symposium on Logic in Computer Science (LICS'10), pp. 449-458.

## Abstract

Stream circuits are a convenient graphical way to represent streams (or stream functions) computed by finite dimensional linear systems. We present a sound and complete expression calculus that allows us to reason about the semantic equivalence of finite closed stream circuits. For our proof of the soundness and completeness we build on recent ideas of Bonsangue, Rutten and Silva. They have provided a “Kleene theorem” and a sound and complete expression calculus for coalgebras for endofunctors of the category of sets. The key ingredient of the soundness and completeness proof is a syntactic characterization of the final locally finite coalgebra. In the present paper we extend this approach to the category of real vector spaces. We also prove that a final locally finite (dimensional) coalgebra is, equivalently, an initial iterative algebra. This makes the connection to existing work on the semantics of recursive specifications.

## Bibtex

@inproceedings{m_linexp, author = {Stefan Milius}, title = {A Sound and Complete Calculus for finite Stream Circuits}, booktitle = {Proc. 25th Annual Symposium on Logic in Computer Science (LICS'10)}, year = {2010}, pages = {449--458}, }
CIA Structures and the Semantics of Recursion
In: Proc. Foundations of Software Science and Computation Structures (FoSSaCS'10),
Lecture Notes Comput. Sci., vol. 6014, pp. 312-327.

## Abstract

Final coalgebras for a functor serve as semantic domains for state based systems of various types. For example, formal languages, streams, non-well-founded sets and behaviors of CCS processes form final coalgebras. We present a uniform account of the semantics of recursive definitions in final coalgebras by combining two ideas: (1) final coalgebras are also initial completely iterative algebras (cia); (2) additional algebraic operations on final coalgebras may be presented in terms of a distributive law λ. We first show that a distributive law leads to new extended cia structures on the final coalgebra. Then we formalize recursive function definitions involving operations given by λ as recursive program schemes for λ, and weprove that unique solutions exist in theextended cias. We illustrate our results by the four concrete final coalgebras mentioned above, e.g., a finite stream circuit defines a unique stream function and we show how to define new process combinators from given ones by sos rules involving recursion.

## Bibtex

@inproceedings{mms10, author = {Stefan Milius and Lawrence S. Moss and Daniel Schwencke}, title = {CIA Structures and the Semantics of Recursion}, booktitle = {Proc. Foundations of Software Science and Computation Structures (FoSSaCS'10)}, year = {2010}, series = {Lecture Notes Comput. Sci.}, volume = {6014}, pages = {312--327}, }

## 2009

A description of iterative reflections of monads (Extended Abstract)
In: Proc. Foundations of Software Science and Computation Structures (FoSSaCS'09),
Lecture Notes Comput. Sci., vol. 5504, pp. 152-166.

## Bibtex

@inproceedings{amv_refl2_09, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {A description of iterative reflections of monads (Extended Abstract)}, booktitle = {Proc. Foundations of Software Science and Computation Structures (FoSSaCS'09)}, year = {2009}, series = {Lecture Notes Comput. Sci.}, volume = {5504}, pages = {152--166}, }
Elgot theories: a new perspective on iteration theories
In: Proc. Mathematical Foundations of Programming Science (MFPS XXV),
Electron. Notes Theor. Comp. Sci., vol. 249, pp. 407-427.

## Abstract

The concept of iteration theory of Bloom and Ésik summarizes all equational properties that iteration has in usual applications, e.g., in Domain Theory where to every system of recursive equations the least solution is assigned. However, this assignment in Domain Theory is also functorial. Yet, functoriality is not included in the definition of iteration theory. Pity: functorial iteration theories have a particularly simple axiomatization, and most of examples of iteration theories are functorial. The reason for excluding functoriality was the view that this property cannot be called equational. This is true from the perspective of the category Sgn of signatures as the base category: whereas iteration theories are monadic (thus, equationally presentable) over Sgn, functorial iteration theories are not. In the present paper we propose to change the perspective and work, in lieu of Sgn, in the category of sets in context (the presheaf category of finite sets and functions). We prove that Elgot theories, which is our name for functorial iteration theories, are monadic over sets in context. Shortly: from the new perspective functoriality is equational.

## Bibtex

@inproceedings{amv_em2_mfps, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot theories: a new perspective on iteration theories}, booktitle = {Proc. Mathematical Foundations of Programming Science (MFPS XXV)}, year = {2009}, series = {Electron. Notes Theor. Comp. Sci.}, volume = {249}, pages = {407--427}, }
Semantics of Higher-Order Recursion Schemes
In: Proc. 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO'09),
Lecture Notes Comput. Sci., vol. 5728, pp. 49-63.

## Abstract

Higher-order recursion schemes are equations defining recursively new operations from given ones called “terminals”. Every such recursion scheme is proved to have a least interpreted semantics in every Scott’s model of λ-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite λ-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Whereas Fiore et al proved that the presheaf F_λ of λ-terms is an initial H_λ-monoid, we work with the presheaf R_λ of rational infinite λ-terms and prove that this is an initial iterative Hλ-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in R_λ.

## Bibtex

@inproceedings{amv_horps, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Semantics of Higher-Order Recursion Schemes}, booktitle = {Proc. 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO'09)}, year = {2009}, series = {Lecture Notes Comput. Sci.}, volume = {5728}, pages = {49--63}, }
Complete Iterativity for Algebras with Effects
In: Proc. Coalgebraic and Algebraic Methods in Computer Science (CALCO'09),
Lecture Notes Comput. Sci., vol. 5728, pp. 34-48.

## Abstract

Completely iterative algebras (cias) are those algebras in which recursive equations have unique solutions. In this paper we study complete iterativity for algebras with computational effects (described by a monad). First, we prove that for every analytic endofunctor on Set there exists a canonical distributive law over any commutative monad M, hence a lifting of that endofunctor to the Kleisli category of M. Then, for an arbitrary distributive law λ of an endofunctor H on Set over a monad M we introduce λ-cias. The cias for the corresponding lifting of H (called Kleisli-cias) form a full subcategory of the category of λ-cias. For various monads of interest we prove that free Kleisli-cias coincide with free λ-cias, and these free algebras are given by free algebras for H. Finally, for three concrete examples of monads we prove that Kleisli-cias and λ-cias coincide and give a characterisation of those algebras.

## Bibtex

@inproceedings{mps, author = {Stefan Milius and Thorsten Palm and Daniel Schwencke}, title = {Complete Iterativity for Algebras with Effects}, booktitle = {Proc. Coalgebraic and Algebraic Methods in Computer Science (CALCO'09)}, year = {2009}, series = {Lecture Notes Comput. Sci.}, volume = {5728}, pages = {34--48}, }
Heike Burghardt, Ralf Pinger and Stefan Milius
Modellbasierte Softwareentwicklung: Herausforderungen und Erfahrungen
Signal+Draht, vol. 101 (1+2), pp. 35-37, 2009.

## Abstract

Modellbasierte Entwicklung verspricht eine Steigerung der Effizienz in der Entwicklung. Gründe für die Effizienzsteigerung sind das frühe Aufdecken von Fehlern und die höhere Qualität der Software. Damit können Entwicklungsschleifen durch spät erkannte Fehler eingespart werden. Letztendlich wird erreicht, dass Produkte schnell und in hoher Qualität beim Kunden vorliegen.

## Bibtex

@article{bpm-sd, author = {Heike Burghardt and Ralf Pinger and Stefan Milius}, title = {Modellbasierte Softwareentwicklung: Herausforderungen und Erfahrungen}, journal = {Signal+Draht}, year = {2009}, volume = {101}, number = {1+2}, pages = {35--37}, }
Equational Properties of Recursive Program Scheme Solutions
Cah. Topol. Géom. Différ. Catég., vol. 50 (1), pp. 23-66, 2009.

## Abstract

In previous work, the authors proposed a general account of recursive program scheme solutions. This work generalized the time-honored approaches that using complete partial orders or metric spaces by offering an account using final coalgebras, Elgot algebras, and much of what is known about them. The account provided an existence and uniqueness result for the solution of a very general kind of uninterpreted recursive program scheme. In addition, it also provided a theory of interpreted solutions. This paper continues the development of the theory by deriving useful general principles which may be used to show that two recursive program schemes in our sense have the same (or related) uninterpreted solution, or that they have the same or related solutions in appropriately related interpretations.

## Bibtex

@article{mm_prop, author = {Stefan Milius and Lawrence S. Moss}, title = {Equational Properties of Recursive Program Scheme Solutions}, journal = {Cah. Topol. G\'{e}om. Diff\'{e}r. Cat\'{e}g.}, year = {2009}, volume = {50}, number = {1}, pages = {23--66}, }

## 2008

Heike Burghardt, Ralf Pinger and Stefan Milius
Modellbasierte Softwareentwicklung in der Bahntechnik
elektronik industrie, 8/9 2008.

## Abstract

Die moderne Bahntechnik weist heutzutage einen hohen Grad an Automatisierung auf. So wird mit nur sieben Betriebsleitzentralen der gesamte Bahnfernverkehr auf Deutschlands Hauptstrecken gesteuert und überwacht. Elek- tronische Stellwerke müssen daher höchsten Anforderungen an Sicherheit, Verfügbarkeit und Wartbarkeit genügen.

## Bibtex

@article{bmp08, author = {Heike Burghardt and Ralf Pinger and Stefan Milius}, title = {Modellbasierte Softwareentwicklung in der Bahntechnik}, journal = {elektronik industrie}, year = {2008}, month = {8/9}, pages = {24--26}, }
Iterative algebras: How iterative are they?
Theory Appl. Categ., vol. 19, pp. 61-92, 2008.

## Abstract

Iterative algebras, defined by the property that every guarded system of recursive equations has a unique solution, are proved to have a much stronger property: every system of recursive equations has a unique strict solution. Those systems that have a unique solution in every iterative algebra are characterized.

## Bibtex

@article{abmv_how, author = {Ji\v{r}\'i Ad\'amek and Reinhard B\"orger and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative algebras: How iterative are they?}, journal = {Theory Appl. Categ.}, year = {2008}, volume = {19}, pages = {61--92}, }
Corrigendum to: "The Category Theoretic Solution of Recursive Program Schemes"
Theoret. Comput. Sci., vol. 403 (2-3), pp. 409-415, 2008. Corrigendum of Theoret. Comput. Sci. 366 (2006), 3-59.

## Abstract

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.

## Bibtex

@article{mm_corr, author = {Stefan Milius and Lawrence S. Moss}, title = {Corrigendum to: "The Category Theoretic Solution of Recursive Program Schemes"}, journal = {Theoret. Comput. Sci.}, year = {2008}, volume = {403}, number = {2-3}, pages = {409--415}, }
On Algebras with Iteration
J. Logic. Comput., vol. 18 (6), pp. 1047-1085, 2008.

## Abstract

Several concepts of algebras with solutions of recursive equation systems are compared: CPO-enrichable algebras are proved to be iteration algebras of Z. Ésik, and iteration algebras are a special case of the recently introduced Elgot algebras (which are the monadic algebras for the free iterative monad). Another special case of iteration algebras are the iterative algebras of E. Nelson and J. Tiuryn, which are algebras with unique solutions of all guarded systems. For each of the above classes of algebras an example is provided showing that the inclusion in a wider class is proper.

## Bibtex

@article{abm_iteration, author = {Ji\v{r}\'i Ad\'amek and Stephen L. Bloom and Stefan Milius}, title = {On Algebras with Iteration}, journal = {J. Logic. Comput.}, year = {2008}, volume = {18}, number = {6}, pages = {1047--1085}, }
Stefan Milius and Uwe Steinke
Modelbasierte Softwarentwickung mit SCADE in der Eisenbahnautomatisierung
In: Proc. Fourth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2008), pp. 68-77.

## Abstract

Wir berichten in diesem Beitrag über ein momentan laufendes Pilotprojekt zur modellbasierten Entwicklung sicherheitsrelevanter Software bei Siemens Mobility im Bereich Eisenbahnautomatisierung. In der Pilotierung benutzen wir SCADE Version 6, ein Tool für die modellbasierte Entwicklung sicherheitsrelevanter Software von der Firma Esterel Technologies. Wir stellen kurz die wesentlichen Merkmale von SCADE vor, und wir berichten von den Erkenntnissen, die wir während unserer Pilotierungsphasen gewonnen haben.

## Bibtex

@inproceedings{ms_scade, author = {Stefan Milius and Uwe Steinke}, title = {Modelbasierte Softwarentwickung mit SCADE in der Eisenbahnautomatisierung}, booktitle = {Proc. Fourth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2008)}, year = {2008}, pages = {68--77}, }
Bases for parametrized iterativity
Inform. and Comput., vol. 206 (8), pp. 966-1002, 2008.

## Abstract

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.

## Bibtex

@article{amv_base2, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Bases for parametrized iterativity}, journal = {Inform. and Comput.}, year = {2008}, volume = {206}, number = {8}, pages = {966--1002}, }

## 2007

What are iteration theories?
In: Proc. 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2007),
Lecture Notes Comput. Sci., vol. 4708, pp. 240-252.

## Abstract

We prove that iteration theories can be introduced as algebras for the monad Rat 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: Rat is the monad of free rational theories and every free rational theory has a continuous completion.

## Bibtex

@inproceedings{amv_what, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {What are iteration theories?}, booktitle = {Proc. 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2007)}, year = {2007}, series = {Lecture Notes Comput. Sci.}, volume = {4708}, pages = {240--252}, }
Algebras with parametrized iterativity
Theoret. Comput. Sci., vol. 388, pp. 130-151, 2007.

## Abstract

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.

## Bibtex

@article{amv_base1, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Algebras with parametrized iterativity}, journal = {Theoret. Comput. Sci.}, year = {2007}, volume = {388}, pages = {130--151}, }
Jiří Adámek, Dominik Lücke and Stefan Milius
Recursive Coalgebras of Finitary Functors
Theor. Inform. Appl., vol. 41 (4), pp. 447-462, 2007.

## Abstract

For finitary set functors preserving inverse images, recursive coalgebras A of Paul Taylor are proved to be precisely those for which the system described by A always halts in finitely many steps.

## Bibtex

@article{alm_rec, author = {Ji\v{r}\'i Ad\'amek and Dominik L\"ucke and Stefan Milius}, title = {Recursive Coalgebras of Finitary Functors}, journal = {Theor. Inform. Appl.}, year = {2007}, volume = {41}, number = {4}, pages = {447--462}, }

## 2006

Jiří Adámek and Stefan Milius (editors)
Seventh Workshop on Coalgebraic Methods in Computer Science 2004
Information and Computation, vol. 204(4), pp. 435-678, 2006.
Special issue with selected papers of the workshop CMCS'04.

## Bibtex

@proceedings{AM_CMCS04, editor = {Ji\v{r}\'i Ad\'amek and Stefan Milius}, title = {Seventh Workshop on Coalgebraic Methods in Computer Science 2004}, publisher = {Elsevier}, series = {Information and Computation}, year = {2006}, volume = {204}, number = {4}, pages = {435--678}, }
Iterative Algebras at Work
Math. Structures Comput. Sci., vol. 16 (6), pp. 1085-1131, 2006. © Cambridge University Press.

## Abstract

Iterative theories, which were introduced by Calvin Elgot, formalise potentially infinite computations as unique solutions of recursive equations. One of the main results of Elgot and his coauthors is a description of a free iterative theory as the theory of all rational trees. Their algebraic proof of this fact is extremely complicated. In our paper we show that by starting with ‘iterative algebras’, that is, algebras admitting a unique solution of all systems of flat recursive equations, a free iterative theory is obtained as the theory of free iterative algebras. The (coalgebraic) proof we present is dramatically simpler than the original algebraic one. Despite this, our result is much more general: we describe a free iterative theory on any finitary endofunctor of every locally presentable category.

## Bibtex

@article{amv_atwork, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative Algebras at Work}, journal = {Math. Structures Comput. Sci.}, year = {2006}, volume = {16}, number = {6}, pages = {1085--1131}, }
Elgot Algebras
Log. Methods Comput. Sci., vol. 2 (5:4), 31 pp., 2006.

## Abstract

Denotational semantics can be based on algebras with additional structure (order, metric, etc.) which makes it possible to interpret recursive specifications. It was the idea of Elgot to base denotational semantics on iterative theories instead, i.e., theories in which abstract recursive specifications are required to have unique solutions. Later Bloom and Esik studied iteration theories and iteration algebras in which a specified solution has to obey certain axioms. We propose so-called Elgot algebras as a convenient structure for semantics in the present paper. An Elgot algebra is an algebra with a specified solution for every system of flat recursive equations. That specification satisfies two simple and well motivated axioms: functoriality (stating that solutions are stable under renaming of recursion variables) and compositionality (stating how to perform simultaneous recursion). These two axioms stem canonically from Elgot's iterative theories: We prove that the category of Elgot algebras is the Eilenberg-Moore category of the monad given by a free iterative theory.

## Bibtex

@article{amv_elgot, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot Algebras}, journal = {Log. Methods Comput. Sci.}, year = {2006}, volume = {2}, number = {5:4}, pages = {31 pp.}, }
Elgot Algebras (extended abstract)
In: Proc. Mathematical Foundations of Programming Science (MFPS XXI),
Electron. Notes Theor. Comput. Sci., vol. 155, pp. 87-109.

## Abstract

Iterative algebras, i. e., algebras A in which flat recursive equations e have unique solutions e†, are generalized to Elgot algebras, where a choice e→e† of solutions of all such equations e is specified. This specification satisfies two simple and well motivated axioms: functoriality (stating that solutions are “uniform”) and compositionality (stating how to perform simultaneous recursion). These two axioms stem canonically from Elgot's iterative theories: We prove that the category of Elgot algebras is the Eilenberg–Moore category of the free iterative monad.

## Bibtex

@inproceedings{amv_elgot_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot Algebras (extended abstract)}, booktitle = {Proc. Mathematical Foundations of Programming Science (MFPS XXI)}, year = {2006}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {155}, pages = {87--109}, }
Terminal Coalgebras and Free Iterative Theories
Inform. and Comput., vol. 204 (7), pp. 1139-1172, 2006.

## Abstract

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.

## Bibtex

@article{am_term, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius}, title = {Terminal Coalgebras and Free Iterative Theories}, journal = {Inform. and Comput.}, year = {2006}, volume = {204}, number = {7}, pages = {1139--1172}, }
How Iterative are Iterative Algebras
In: Proc. Coalgebraic Methods in Computer Science (CMCS'06),
Electron. Notes Theor. Comp. Sci., vol. 164, pp. 157-175.

## Abstract

Iterative algebras are defined by the property that every guarded system of recursive equations has a unique solution. We prove that they have a much stronger property: every system of recursive equations has a unique strict solution. And we characterize those systems that have a unique solution in every iterative algebra.

## Bibtex

@inproceedings{amv_how_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {How Iterative are Iterative Algebras}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'06)}, year = {2006}, series = {Electron. Notes Theor. Comp. Sci.}, volume = {164}, pages = {157--175}, }
The Category Theoretic Solution of Recursive Program Schemes
Theoret. Comput. Sci., vol. 366, pp. 3-59, 2006. Fundamental study; a corrigendum appeared in Theoret. Comput. Sci. 403 (2008), 409-415.

## Abstract

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.

## Bibtex

@article{mm, author = {Stefan Milius and Lawrence S. Moss}, title = {The Category Theoretic Solution of Recursive Program Schemes}, journal = {Theoret. Comput. Sci.}, year = {2006}, volume = {366}, pages = {3--59}, }

## 2005

Iterative Algebras for a Base
In: Proc. Category Theory and Computer Science (CTCS'04),
Electron. Notes Theor. Comput.Sci., vol. 122, pp. 147-170.

## Abstract

For algebras A whose type is given by an endofunctor, iterativity means that every flat equation morphism in A has a unique solution. In our previous work we proved that every object generates a free iterative algebra, and we provided a coalgebraic construction of those free algebras. Iterativity w.r.t. an endofunctor was generalized by Tarmo Uustalu to iterativity w.r.t. a “base”, i.e., a functor of two variables yielding finitary monads in one variable. In the current paper we introduce iterative algebras in this general setting, and provide again a coalgebraic construction of free iterative algebras.

## Bibtex

@inproceedings{amv_base_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative Algebras for a Base}, booktitle = {Proc. Category Theory and Computer Science (CTCS'04)}, year = {2005}, series = {Electron. Notes Theor. Comput.Sci.}, volume = {122}, pages = {147--170}, }
A General Final Coalgebra Theorem
Math. Structures Comput. Sci., vol. 15 (3), pp. 409-432, 2005. © Cambridge University Press.

## Abstract

By the Final Coalgebra Theorem of Aczel and Mendler, every endofunctor of the category of sets has a final coalgebra, which, however, may be a proper class. We generalise this to all ‘well-behaved’ categories K . The role of the category of classes is played by a free cocompletion K∞ of K under transfinite colimits, that is, colimits of ordinal-indexed chains. Every endofunctor F of K has a canonical extension to an endofunctor F∞ of K∞ which is proved to have a final coalgebra (and an initial algebra). Based on this, we prove a general solution theorem: for every endofunctor of a locally presentable category K all guarded equation-morphisms have unique solutions. The last result does not need the extension K∞: the solutions are always found within the category K .

## Bibtex

@article{amv_general, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {A General Final Coalgebra Theorem}, journal = {Math. Structures Comput. Sci.}, year = {2005}, volume = {15}, number = {3}, pages = {409--432}, }
Stefan Milius
Completely Iterative Algebras and Completely Iterative Monads
Inform. and Comput., vol. 196, pp. 1-41, 2005.

## Abstract

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.

## Bibtex

@article{m_cia, author = {Stefan Milius}, title = {Completely Iterative Algebras and Completely Iterative Monads}, journal = {Inform. and Comput.}, year = {2005}, volume = {196}, pages = {1--41}, }
The Category Theoretic Solution of Recursive Program Schemes
In: Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO'05),
Lecture Notes in Comput. Sci., vol. 3629, pp. 293-312.

## Abstract

This paper provides a general account of the notion of recursive program schemes, their uninterpreted and interpreted solutions, and related concepts. 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 recursion, e.g., 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 at all. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme. In this short version of our paper we can only sketch some proofs.

## Bibtex

@inproceedings{mm_abs, author = {Stefan Milius and Lawrence S. Moss}, title = {The Category Theoretic Solution of Recursive Program Schemes}, booktitle = {Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO'05)}, year = {2005}, series = {Lecture Notes in Comput. Sci.}, volume = {3629}, pages = {293--312}, }

## 2004

From Iterative Algebras to Iterative Theories
In: Proc. Coalgebraic Methods in Computer Science (CMCS'04),
Electron. Notes Theor. Comput. Sci., vol. 106, pp. 3-24.

## Abstract

Iterative theories introduced by Calvin Elgot formalize potentially infinite computations as solutions of recursive equations. One of the main results of Elgot and his coauthors is a description of a free iterative theory as the theory of all rational trees. Their algebraic proof of this fact is extremely complicated. In our paper we show that by starting with “iterative algebras”, i.e., algebras admitting a unique solution of all systems of flat recursive equations, a free iterative theory is obtained as the theory of free iterative algebras. The (coalgebraic) proof we present is dramatically simpler than the original algebraic one. And our result is, nevertheless, much more general: we describe a free iterative theory on any finitary endofunctor of every locally presentable category A. This allows us, e.g., to consider iterative algebras over any equationally specified class A of finitary algebras.

## Bibtex

@inproceedings{amv_mccoy_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {From Iterative Algebras to Iterative Theories}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'04)}, year = {2004}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {106}, pages = {3--24}, }
On coalgebra based on Classes
Theoret. Comput. Sci., vol. 316, pp. 3-23, 2004.

## Abstract

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.

## Bibtex

@article{, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {On coalgebra based on Classes}, journal = {Theoret. Comput. Sci.}, year = {2004}, volume = {316}, pages = {3--23}, }

## 2003

Infinite Trees and Completely Iterative Theories: A Coalgebraic View
Theoret. Comput. Sci., vol. 300, pp. 1-45, 2003. Fundamental study.

## Abstract

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 \tensor - + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.

## Bibtex

@article{aamv, author = {Peter Aczel and Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Infinite Trees and Completely Iterative Theories: A Coalgebraic View}, journal = {Theoret. Comput. Sci.}, year = {2003}, volume = {300}, pages = {1--45}, }
Some Remarks on Finitary and Iterative Monads
Appl. Categ. Structures, vol. 11 (6), pp. 521-541, 2003.

## Abstract

For every locally finitely presentable category A we introduce finitary Kleisli triples on A and show that they bijectively correspond to finitary monads on A. We illustrate this on free monads and free iterative monads.

## Bibtex

@article{amv_finkleisli, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Some Remarks on Finitary and Iterative Monads}, journal = {Appl. Categ. Structures}, year = {2003}, volume = {11}, number = {6}, pages = {521--541}, }
Free Iterative Theories: a coalgebraic view
Math. Structures Comput. Sci., vol. 13 (2), pp. 259-320, 2003. © Cambridge University Press.

## Abstract

Every finitary endofunctor of Set is proved to generate a free iterative theory in the sense of Elgot. This work is based on coalgebras, specifically on parametric corecursion, and the proof is presented for categories more general than just Set.

## Bibtex

@article{amv_62, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Free Iterative Theories: a coalgebraic view}, journal = {Math. Structures Comput. Sci.}, year = {2003}, volume = {13}, number = {2}, pages = {259--320}, }
Stefan Milius
On Colimits in Categories of Relations
Appl. Categ. Structures, vol. 11 (3), pp. 287-312, 2003.

## Abstract

We study (finite) coproducts and colimits of omega-chains in Rel(C), the 2-category of relations over a given category C. The former exist and are "the same" as in C provided that C is extensive. The latter do not exist for example in Rel(Set). However, the canonical construction of those colimits in the category of sets can be generalized to Rel(Set). The canonical cocone is shown to satisfy a 2-categorical universal property, namely that of an lax adjoint cooplimit. Sufficient conditions for any base category C to admit the construction are given. A necessary and sufficient condition for the construction to yield colimits of omega-chains in the category of maps of Rel(C) is also given.

## Bibtex

@article{m_rel, author = {Stefan Milius}, title = {On Colimits in Categories of Relations}, journal = {Appl. Categ. Structures}, year = {2003}, volume = {11}, number = {3}, pages = {287--312}, }

## 2002

On Rational Monads and Free Iterative Theories
In: Proc. Category Theory and Computer Science (CTCS'02),
Electron. Notes Theor. Comput. Sci., vol. 69, pp. 23-46.

## Abstract

For every finitary endofunctor H of Set a rational algebraic theory (or a rational finitary monad) R is defined by means of solving all finitary flat systems of recursive equations over H. This generalizes the result of Elgot and his coauthors, describing a free iterative theory of a polynomial endofunctor H as the theory R of all rational infinite trees. We present a coalgebraic proof that R is a free iterative theory on H for every finitary endofunctor H, which is substantially simpler than the previous proof by Elgot et al., as well as our previous proof. This result holds for more general categories than Set.

## Bibtex

@inproceedings{amv_62_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {On Rational Monads and Free Iterative Theories}, booktitle = {Proc. Category Theory and Computer Science (CTCS'02)}, year = {2002}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {69}, pages = {23--46}, }
Stefan Milius
On Iteratable Endofunctors
In: Proc. Category Theory and Computer Science (CTCS'02),
Electron. Notes Theor. Comput. Sci., vol. 69, pp. 287-304.

## Abstract

Completely iterative monads of Elgot et al. are the monads such that every guarded iterative equation has a unique solution. Free completely iterative monads are known to exist on every iteratable endofunctor H, i.e., one with final coalgebras of all functors H(-) + X. We show that conversely, if H generates a free completely iterative monad, then it is iteratable.

## Bibtex

@inproceedings{m_iter_abs, author = {Stefan Milius}, title = {On Iteratable Endofunctors}, booktitle = {Proc. Category Theory and Computer Science (CTCS'02)}, year = {2002}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {69}, pages = {287--304}, }
Final Coalgebras And a Solution Theorem for Arbitrary Endofunctors
In: Proc. Coalgebraic Methods in Computer Science (CMCS'02),
Electron. Notes Theor. Comput. Sci., vol. 65, pp. 1-28.

## Abstract

Every endofunctor F of Set has an initial algebra and a final coalgebra, but they are classes in general. Consequently, the endofunctor F∞ of the category of classes that F induces generates a completely iterative monad T. And solutions of arbitrary guarded systems of iterative equations w.r.t. F exist, and can be found in naturally defined subsets of the classes TY. More generally, starting from any category K, we can form a free cocompletion K∞ of K under small-filtered colimits (e.g., Set∞ is the category of classes), and we give sufficient conditions to obtain analogous results for arbitrary endofunctors of K.

@inproceedings{amv_general_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Final Coalgebras And a Solution Theorem for Arbitrary Endofunctors}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'02)}, year = {2002}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {65}, pages = {1--28}, }