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 ()
Jump to year:20242023202220212020201920182017201620152014201320122011201020092008200720062005200420032002

2024

Fabian Birkmann, Stefan Milius and Henning Urbat
Monoidal Extended Stone Duality
In: Proc. 26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024),
Lecture Notes Comput. Sci. (ARCoSS), vol. ??, pp. ??, to appear.

Abstract

Extensions of Stone-type dualities have a long history in algebraic logic and have also been instrumental for proving results in algebraic language theory. We show how to extend abstract categorical dualities via monoidal adjunctions, subsuming various incarnations of classical extended Stone and Priestley duality as a special case. Guided by these categorical foundations, we investigate residuation algebras, which are algebraic models of language derivatives, and show its subcategory of boolean derivation algebras to be dually equivalent to the category of profinite monoids. We further extend this duality to capture relational morphisms of profinite monoids, which dualize to natural morphisms of residuation algebras.

Download

Bibtex

@inproceedings{bmu24,
author = {Fabian Birkmann and Stefan Milius and Henning Urbat},
title = {Monoidal Extended Stone Duality},
booktitle = {Proc. 26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024)},
year = {2024},
series = {Lecture Notes Comput. Sci. (ARCoSS)},
volume = {??},
pages = {??},
}

2023

Jiří Adámek, Stefan Milius and Lawrence S. Moss
On Kripke, Vietoris and Hausdorff Polynomial Functors
In: Proc. 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 270, pp. 21:1-21:20.

Abstract

The Vietoris space of compact subsets of a given Hausdorff space yields an endofunctor V on the category of Hausdorff spaces. Vietoris polynomial endofunctors on that category are built from V, the identity and constant functors by forming products, coproducts and compositions. These functors are known to have terminal coalgebras and we deduce that they also have initial algebras. We present an analogous class of endofunctors on the category of extended metric spaces, using in lieu of V the Hausdorff functor H. We prove that the ensuing Hausdorff polynomial functors have terminal coalgebras and initial algebras. Whereas the canonical constructions of terminal coalgebras for Vietoris polynomial functors takes ω steps, one needs ω + ω steps in general for Hausdorff ones. We also give a new proof that the closed set functor on metric spaces has no fixed points.

Download

Bibtex

@inproceedings{amm23,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss},
title = {On Kripke, Vietoris and Hausdorff Polynomial Functors},
booktitle = {Proc. 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
year = {2023},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {270},
pages = {21:1--21:20},
}
Florian Frank, Stefan Milius and Henning Urbat
Positive Data Languages
In: Proc. 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 272, pp. 48:1-48:15.

Abstract

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

Download

Bibtex

@inproceedings{fmu23,
author = {Florian Frank and Stefan Milius and Henning Urbat},
title = {Positive Data Languages},
booktitle = {Proc. 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
year = {2023},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {272},
pages = {48:1--48:15},
}
Fabian Birkmann, Stefan Milius and Henning Urbat
Nominal Topology for Data Languages
In: Proc. 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 261, pp. 114:1--114:21.

Abstract

We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite nominal topological spaces. Assuming globally bounded support sizes, they coincide with nominal Stone spaces and are shown to be dually equivalent to a subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of pro-orbit-finite words. In addition, we explore the expressive power of pro-orbit-finite equations by establishing a nominal version of Reiterman's pseudovariety theorem.

Download

Bibtex

@inproceedings{bmu23,
author = {Fabian Birkmann and Stefan Milius and Henning Urbat},
title = {Nominal Topology for Data Languages},
booktitle = {Proc. 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
year = {2023},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {261},
pages = {114:1----114:21},
}
Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius and Lutz Schröder
Weak similarity in higher-order mathematical operational semantics
In: Proc. 38th Annual Symposium on Logic in Computer Science (LICS 2023).

Abstract

Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the lambda-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method.

Download

Bibtex

@inproceedings{utgms23,
author = {Henning Urbat and Stelios Tsampas and Sergey Goncharov and Stefan Milius and Lutz Schr\"oder},
title = {Weak similarity in higher-order mathematical operational semantics},
booktitle = {Proc. 38th Annual Symposium on Logic in Computer Science (LICS 2023)},
year = {2023},
pages = {},
}
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas and Henning Urbat
Towards a Higher-Order Mathematical Operational Semantics
In: Proc. 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023),
Proceedings of the ACM on Programming Languages, vol. 7, Issue POPL, pp. 632-658.

Abstract

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the 𝜆-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.

Download

Bibtex

@inproceedings{gmstu23,
author = {Sergey Goncharov and Stefan Milius and Lutz Schr\"oder and Stelios Tsampas and Henning Urbat},
title = {Towards a Higher-Order Mathematical Operational Semantics},
booktitle = {Proc. 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)},
year = {2023},
series = {Proceedings of the ACM on Programming Languages},
volume = {7, Issue POPL},
pages = {632--658},
}

2022

Thorsten Wißmann, Stefan Milius and Lutz Schröder
Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence
Log. Methods Comput. Sci., vol. 18 (4), pp. 6:1-6:48, 2022. Journal version of CONCUR 2021 conference paper below.

Abstract

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time O((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was O(mn).

Download

Bibtex

@article{wms22,
author = {Thorsten Wißmann and Stefan Milius and Lutz Schr\"oder},
title = {Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence},
journal = {Log. Methods Comput. Sci.},
year = {2022},
volume = {18},
number = {4},
pages = {6:1--6:48},
}
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas and Henning Urbat
Stateful Structural Operational Semantics
In: Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 30:1-30:19.

Abstract

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

Download

Bibtex

@inproceedings{gmstu22,
author = {Sergey Goncharov and Stefan Milius and Lutz Schr\"oder and Stelios Tsampas and Henning Urbat},
title = {Stateful Structural Operational Semantics},
booktitle = {Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
year = {2022},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {228},
pages = {30:1--30:19},
}
Chase Ford, Harsh Beohar, Barbara König, Stefan Milius and Lutz Schröder
Graded Monads and Behavioural Equivalence Games
In: Proc. 37th Annual Symposium on Logic in Computer Science (LICS 2022).

Abstract

The framework of graded semanticsuses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.

Download

Bibtex

@inproceedings{fbkms22,
author = {Chase Ford and Harsh Beohar and Barbara K\"onig and Stefan Milius and Lutz Schr\"oder},
title = {Graded Monads and Behavioural Equivalence Games},
booktitle = {Proc. 37th Annual Symposium on Logic in Computer Science (LICS 2022)},
year = {2022},
pages = {},
}
Fabian Birkmann, Hans-Peter Deifel and Stefan Milius
Distributed Coalgebraic Partition Refinement
In: Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022),
Lecture Notes Comput. Sci. (ARCoSS), vol. 13244, pp. 159-177.

Abstract

Partition refinement is a method for minimizing automata and transition systems of various types. Recently we have developed a partition refinement algorithm and the tool CoPaR that is generic in the transition type of the input system and matches the theoretical run time of the best known algorithms for many concrete system types. Genericity is achieved by modelling transition types as functors on sets and systems as coalgebras. Experimentation has shown that memory consumption is a bottleneck for handling systems with a large state space, while running times are fast. We have therefore extended an algorithm due to Blom and Orzan, which is suitable for a distributed implementation to the coalgebraic level of genericity, and implemented it in CoPaR. Experiments show that this allows to handle much larger state spaces. Running times are low in most experiments, but there is a significant penalty for some.

Download

Bibtex

@inproceedings{bdm22,
author = {Fabian Birkmann and Hans-Peter Deifel and Stefan Milius},
title = {Distributed Coalgebraic Partition Refinement},
booktitle = {Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022)},
year = {2022},
series = {Lecture Notes Comput. Sci. (ARCoSS)},
volume = {13244},
pages = {159--177},
}
Florian Frank, Stefan Milius and Henning Urbat
Coalgebraic Semantics for Nominal Automata
In: Proc. Fifteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022),
Lecture Notes Comput. Sci., vol. 13225, pp. 45-66.

Abstract

This paper provides a coalgebraic approach to the language semantics of two types of non-deterministic automata over nominal sets: non-deterministic orbit-finite automata (NOFAs) and regular nominal non-deterministic automata (RNNAs), which were introduced in previous work. While NOFAs are a straightforward nominal version of non-deterministic automata, RNNAs feature ordinary as well as name binding transitions. Correspondingly, words accepted by RNNAs are strings formed by ordinary letters and name binding letters. Bar languages are sets of such words modulo α-equivalence, and to every state of an RNNA one associates its accepted bar language. We show that the semantics of NOFAs and RNNAs, respectively, arise both as an instance of the Kleisli-style coalgebraic trace semantics as well as an instance of the coalgebraic language semantics obtained via generalized determinization. On the way we revisit coalgebraic trace semantics in general and give a new compact proof for the main result in that theory stating that an initial algebra for a functor yields the terminal coalgebra for the Kleisli extension of the functor. Our proof requires fewer assumptions on the functor than all previous ones.

Download

Bibtex

@inproceedings{fmu22,
author = {Florian Frank and Stefan Milius and Henning Urbat},
title = {Coalgebraic Semantics for Nominal Automata},
booktitle = {Proc. Fifteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022)},
year = {2022},
series = {Lecture Notes Comput. Sci.},
volume = {13225},
pages = {45--66},
}

2021

Jiří Adámek, Chase Ford, Stefan Milius and Lutz Schröder
Finitary Monads on the Category of Posets
Math. Structures Comput. Sci., vol. 31 (Special Issue in honor of John Power), pp. 799-821, 2021.

Abstract

Finitary monads on Pos are characterized as precisely the free-algebra monads of varieties of algebras. These are classes of ordered algebras specified by inequations in context. Analogously, finitary enriched monads on Pos are characterized: here we work with varieties of coherent algebras which means that their operations are monotone.

Download

Bibtex

@article{afms21,
author = {Ji\v{r}\'i Ad\'amek and Chase Ford and Stefan Milius and Lutz Schr\"oder},
title = {Finitary Monads on the Category of Posets},
journal = {Math. Structures Comput. Sci.},
year = {2021},
volume = {31},
number = {Special Issue in honor of John Power},
pages = {799--821},
}
Chase Ford, Stefan Milius and Lutz Schröder
Monads on Categories of Relational Structures
In: Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 211, pp. 14:1-14:17.

Abstract

We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity λ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders (λ = ω) or metric spaces (λ = ω₁). We establish a bijective correspondence between λ-accessible enriched monads on the given category of relational structures and a notion of λ-ary algebraic theories (i.e. with operations of arity < λ), with the syntax of algebraic theories induced by the relational signature (e.g. inequations or equations-up-to-ε). We provide a generic sound and complete derivation system for such relational algebraic theories, thus in particular recovering (extensions of) recent systems of this type for monads on partial orders and metric spaces by instantiation. In particular, we present an ω₁-ary algebraic theory of metric completion. The theory-to-monad direction of our correspondence remains true for the case of κ-ary algebraic theories and κ-accessible monads for κ < λ, e.g. for finitary theories over metric spaces.

Download

Bibtex

@inproceedings{fms21-2,
author = {Chase Ford and Stefan Milius and Lutz Schr\"oder},
title = {Monads on Categories of Relational Structures},
booktitle = {Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
year = {2021},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {211},
pages = {14:1--14:17},
}
Jiří Adámek, Stefan Milius and Lawrence S. Moss
Initial algebras without iteration
In: Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 211, pp. 5:1-5:20.

Abstract

The Initial Algebra Theorem by Trnková et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point A of the functor, it uses Pataraia’s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of A. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.

Download

Bibtex

@inproceedings{amm21,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss},
title = {Initial algebras without iteration},
booktitle = {Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
year = {2021},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {211},
pages = {5:1--5:20},
}
Jiří Adámek, Stefan Milius and Henning Urbat
On the behaviour of coalgebras with side effects and algebras with effectful iteration
J. Logic Comput., vol. 31 (6), pp. 1429-1481, 2021. Journal version of CMCS 2018 paper below.

Abstract

For every finitary monad T on sets and every endofunctor F on the category of T-algebras we introduce the concept of an ffg-Elgot algebra for F, that is, an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad T. The goal is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point φF, i.e. the colimit of all F-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of T-algebras.

Download

Bibtex

@article{amu21,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},
title = {On the behaviour of coalgebras with side effects and algebras with effectful iteration},
journal = {J. Logic Comput.},
year = {2021},
volume = {31},
number = {6},
pages = {1429--1481},
}
Thorsten Wißmann, Stefan Milius and Lutz Schröder
Explaining Behavioural Inequivalence Generically in Quasilinear Time
In: Proc. 32nd International Conference on Concurrency Theory (CONCUR 2021),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 203, pp. 32:1-32:18.

Abstract

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically derived from the functor. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time O((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was O(mn).

Download

Bibtex

@inproceedings{wms21,
author = {Thorsten Wißmann and Stefan Milius and Lutz Schr\"oder},
title = {Explaining Behavioural Inequivalence Generically in Quasilinear Time},
booktitle = {Proc. 32nd International Conference on Concurrency Theory (CONCUR 2021)},
year = {2021},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {203},
pages = {32:1--32:18},
}
Henning Urbat, Daniel Hausmann, Stefan Milius and Lutz Schröder
Nominal Büchi Automata with Name Allocation
In: Proc. 32nd International Conference on Concurrency Theory (CONCUR 2021),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 203, pp. 4:1-4:16.

Abstract

Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e.~infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e.~resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.

Download

Bibtex

@inproceedings{uhms21,
author = {Henning Urbat and Daniel Hausmann and Stefan Milius and Lutz Schr\"oder},
title = {Nominal Büchi Automata with Name Allocation},
booktitle = {Proc. 32nd International Conference on Concurrency Theory (CONCUR 2021)},
year = {2021},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {203},
pages = {4:1--4:16},
}
Daniel Hausmann, Stefan Milius and Lutz Schröder
A Linear-Time Nominal mu-Calculus with Name Allocation
In: Proc. 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 202, pp. 58:1-58:18.

Abstract

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

Download

Bibtex

@inproceedings{hms21,
author = {Daniel Hausmann and Stefan Milius and Lutz Schr\"oder},
title = {A Linear-Time Nominal mu-Calculus with Name Allocation},
booktitle = {Proc. 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
year = {2021},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {202},
pages = {58:1--58:18},
}
Jiří Adámek, Liang-Ting Chen, Stefan Milius and Henning Urbat
Reiterman's Theorem on Finite Algebras for a Monad
ACM Trans. Comput. Log., vol. 22 (4:23), pp. 1-48, 2021.

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 generalized to finite Eilenberg-Moore algebras for a monad T on a category D: we prove that a class of finite T-algebras is a pseudovariety iff it is presentable by profinite equations. As a key technical tool, we introduce the concept of a profinite monad \hat{T} associated to the monad T, which gives a categorical view of the construction of the space of profinite terms.

Download

Bibtex

@article{acmu21,
author = {Ji\v{r}\'i Ad\'amek and Liang-Ting Chen and Stefan Milius and Henning Urbat},
title = {Reiterman's Theorem on Finite Algebras for a Monad},
journal = {ACM Trans. Comput. Log.},
year = {2021},
volume = {22},
number = {4:23},
pages = {1--48},
}
Chase Ford, Stefan Milius and Lutz Schröder
Behavioural Preorders via Graded Monads
In: Proc. 36th Annual Symposium on Logic in Computer Science (LICS 2021).

Abstract

Like notions of process equivalence, behavioural preorders on processes come in many flavours, ranging from fine-grained comparisons such as ready simulation to coarse-grained ones such as trace inclusion. Often, such behavioural preorders are characterized in terms of theory inclusion in dedicated characteristic logics; e.g. simulation is characterized by theory inclusion in the positive fragment of Hennessy-Milner logic. We introduce a unified semantic framework for behavioural preorders and their characteristic logics in which we parametrize the system type in the coalgebraic paradigm while behavioural preorders are captured as graded monads on the category Pos of partially ordered sets, in generalization of a previous approach to notions of process equivalence. We show that graded monads on Pos are induced by inequational theories in a form of graded ordered algebra that we introduce here. Moreover, we provide a general notion of modal logic compatible with a given graded behavioural preorder, along with a criterion for expressiveness.

Download

Bibtex

@inproceedings{fms21,
author = {Chase Ford and Stefan Milius and Lutz Schr\"oder},
title = {Behavioural Preorders via Graded Monads},
booktitle = {Proc. 36th Annual Symposium on Logic in Computer Science (LICS 2021)},
year = {2021},
pages = {},
}
Hans-Peter Deifel, Stefan Milius and Thorsten Wißmann
Coalgebra Encoding for Efficient Minimization
In: Proc. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 195, pp. 28:1-28:19.

Abstract

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

Download

Bibtex

@inproceedings{dmw21,
author = {Hans-Peter Deifel and Stefan Milius and Thorsten Wißmann},
title = {Coalgebra Encoding for Efficient Minimization},
booktitle = {Proc. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
year = {2021},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {195},
pages = {28:1--28:19},
}
Thorsten Wißmann, Hans-Peter Deifel, Stefan Milius and Lutz Schröder
From Generic Partition Refinement to Weighted Tree Automata Minimization
Form. Asp. Comput., vol. 30, pp. 695-727, 2021. Journal version of FM 2019 conference paper below.

Abstract

Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.

Download

Bibtex

@article{wdms21,
author = {Thorsten Wißmann and Hans-Peter Deifel and Stefan Milius and Lutz Schr\"oder},
title = {From Generic Partition Refinement to Weighted Tree Automata Minimization},
journal = {Form. Asp. Comput.},
year = {2021},
volume = {30},
pages = {695--727},
}
Rob Myers, Stefan Milius and Henning Urbat
Nondeterministic Syntactic Complexity
In: Proc. 24th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2021),
Lecture Notes Comput. Sci. (ARCoSS), vol. 12650, pp. 448--468.

Abstract

We introduce a new measure on regular languages: their nondeterministic syntactic complexity. It is the least degree of any extension of the `canonical boolean representation' of the syntactic monoid. Equivalently, it is the least number of states of any subatomic nondeterministic acceptor. It turns out that essentially all previous structural work on nondeterministic state-minimality computes this measure. Our approach rests on an algebraic interpretation of nondeterministic finite automata as deterministic finite automata endowed with semilattice structure. Crucially, the latter form a self-dual category.

Download

Bibtex

@inproceedings{mmu21,
author = {Rob Myers and Stefan Milius and Henning Urbat},
title = {Nondeterministic Syntactic Complexity},
booktitle = {Proc. 24th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2021)},
year = {2021},
series = {Lecture Notes Comput. Sci. (ARCoSS)},
volume = {12650},
pages = {448----468},
}
Fabian Birkmann, Stefan Milius and Henning Urbat
On Language Varieties Without Boolean Operations
In: Proc. 15th International Conference on Language and Automata Theory and Applications (LATA 2021),
Lecture Notes Comput. Sci., vol. 12638, pp. 3--15.

Abstract

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

Download

Bibtex

@inproceedings{bmu21,
author = {Fabian Birkmann and Stefan Milius and Henning Urbat},
title = {On Language Varieties Without Boolean Operations},
booktitle = {Proc. 15th International Conference on Language and Automata Theory and Applications (LATA 2021)},
year = {2021},
series = {Lecture Notes Comput. Sci.},
volume = {12638},
pages = {3----15},
}

2020

Janine Schneider, Hans-Peter Deifel, Stefan Milius and Felix Freiling
Unifying Metadata-Based Storage Reconstruction and Carving with LAYR
In: Proc. 20th Annual DFRWS USA (DFRWS 2020 USA),
Forensic Science International: Digital Investigation, vol. 33, article 301006.

Abstract

Storage resources are usually organized in abstraction layers in computing systems where higher level storage (e.g. files or file systems) are constructed from lower level storage (e.g. disk volumes). Many forensic storage reconstruction techniques exist that gather data at lower layers and interpret this data to reconstruct higher layers. On the one hand, there are metadata-based reconstruction techniques that interpret metadata structures to precisely reconstruct upper layer content. On the other hand, there are pattern-based techniques (carving) that focus mainly on deleted files that cannot be reconstructed by other methods. Instances resembling the former approach are Carrier's The Sleuth Kit (TSK) as well as many commercial tools, while the latter approach is used by file carvers like Foremost and Scalpel. Based on a formalization of storage abstraction layers, we show that all these techniques can be unified within a modular reconstruction framework. We define composition operators that allow to precisely express complex reconstruction tasks that involve both metadata-based and pattern-based techniques and allow to combine their respective strengths seamlessly in forensic analysis. We present LAYR, an implementation of our approach and show that it can automatically and reliably combine different reconstruction approaches.

Download

Bibtex

@inproceedings{sdmf20,
author = {Janine Schneider and Hans-Peter Deifel and Stefan Milius and Felix Freiling},
title = {Unifying Metadata-Based Storage Reconstruction and Carving with LAYR},
booktitle = {Proc. 20th Annual DFRWS USA (DFRWS 2020 USA)},
year = {2020},
series = {Forensic Science International: Digital Investigation},
volume = {33},
pages = {},
}
Thorsten Wißmann, Ulrich Dorsch, Stefan Milius and Lutz Schröder
Efficient and Modular Coalgebraic Partition Refinement
Log. Methods Comput. Sci., vol. 16 (1), pp. 8:1-8:63, 2020. Journal version of CONCUR 2017 conference paper below.

Abstract

We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in system analysis and verification. Coalgebraic generality allows us to cover not only classical relational systems but also, e.g. various forms of weighted systems and furthermore to flexibly combine existing system types. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log(n)) where n and m are the numbers of nodes and edges, respectively. The generic complexity result and the possibility of combining system types yields a toolbox for efficient partition refinement algorithms. Instances of our generic algorithm match the run-time of the best known algorithms for unlabelled transition systems, Markov chains, deterministic automata (with fixed alphabets), Segala systems, and for color refinement.

Download

Bibtex

@article{wdms20,
author = {Thorsten Wißmann and Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder},
title = {Efficient and Modular Coalgebraic Partition Refinement},
journal = {Log. Methods Comput. Sci.},
year = {2020},
volume = {16},
number = {1},
pages = {8:1--8:63},
}
Stefan Milius, Dirk Pattinson and Thorsten Wißmann
A New Foundation for Finitary Corecursion and Iterative Algebras
Inform. and Comput., vol. 271, pp. 104456, 2020. Journal version of FoSSaCS 2016 conference paper below.

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 is finitary and preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adamek et al.). 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. Moreover, we obtain a number of new examples, e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by Silva et al., and the monad of Courcelle's algebraic trees.

Download

Bibtex

@article{mpw19,
author = {Stefan Milius and Dirk Pattinson and Thorsten Wißmann},
title = {A New Foundation for Finitary Corecursion and Iterative Algebras},
journal = {Inform. and Comput.},
year = {2020},
volume = {271},
pages = {104456},
}
Jiří Adámek, Stefan Milius and Lawrence S. Moss
On Well-Founded and Recursive Coalgebras
In: Proc. 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020),
Lecture Notes Comput. Sci. (ARCoSS), vol. 12077, pp. 17-36.

Abstract

This paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving endofunctors on complete and well-powered categories every coalgebra has a well-founded part, and we provide a new, shorter proof that this is the coreflection in the category of all well-founded coalgebras. We present a new more general proof of Taylor's General Recursion Theorem that every well-founded coalgebra is recursive, and we study under which hypothesis the converse holds. In addition, we present a new equivalent characterization of well-foundedness: a coalgebra is well-founded iff it admits a coalgebra-to-algebra morphism to the initial algebra.

Download

Bibtex

@inproceedings{amm20,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss},
title = {On Well-Founded and Recursive Coalgebras},
booktitle = {Proc. 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020)},
year = {2020},
series = {Lecture Notes Comput. Sci. (ARCoSS)},
volume = {12077},
pages = {17--36},
}
Sergey Goncharov, Stefan Milius and Alexandra Silva
Towards a Uniform Theory of Effectful State Machines
ACM Trans. Comput. Log., vol. 21 (3:23), pp. 63, 2020. Journal version of TCS 2014 paper below.

Abstract

Using recent developments on coalgebraic and monad-based semantics, we present a uniform study of various notions of machines, e.g. finite state machines, multi-stack machines, Turing machines, valence automata, and weighted automata. They are instances of Jacobs' notion of a T-automaton}, where T is a monad. We show that the generic language semantics for T-automata correctly instantiates the usual language semantics for a number of known classes of machines/languages, including~regular, context-free, recursively-enumerable and various subclasses of context free languages (e.g. deterministic and real-time ones). Moreover, our approach provides new generic techniques for studying the expressivity power of various machine-based models.

Download

Bibtex

@article{gms20,
author = {Sergey Goncharov and Stefan Milius and Alexandra Silva},
title = {Towards a Uniform Theory of Effectful State Machines},
journal = {ACM Trans. Comput. Log.},
year = {2020},
volume = {21},
number = {3:23},
pages = {63},
}

2019

Thorsten Wißmann, Stefan Milius, Jérémy Dubut and Shin-ya Katsumata
A Coalgebraic View on Reachability
Comment. Math. Univ. Carolin., vol. 60 (4), pp. 605-638, 2019.

Abstract

Coalgebras for an endofunctor provide a category-theoretic framework for modeling a wide range of state-based systems of various types. We provide an iterative construction of the reachable part of a given pointed coalgebra that is inspired by and resembles the standard breadth-first search procedure to compute the reachable part of a graph. We also study coalgebras in Kleisli categories: for a functor extending a functor on the base category, we show that the reachable part of a given pointed coalgebra can be computed in that base category.

Download

Bibtex

@article{wmkd19,
author = {Thorsten Wißmann and Stefan Milius and J\'er\'emy Dubut and Shin-ya Katsumata},
title = {A Coalgebraic View on Reachability},
journal = {Comment. Math. Univ. Carolin.},
year = {2019},
volume = {60},
number = {4},
pages = {605--638},
}
Jiří Adámek, Stefan Milius, Lurdes Sousa and Thorsten Wißmann
Finitely Presentable Algebras For Finitary Monads
Theory Appl. Categ., vol. 34, pp. 1179-1195, 2019.

Abstract

For finitary regular monads $\T$ on locally finitely presentable categories we characterize the finitely presentable objects in the category of $\T$-algebras in the style known from general algebra: they are precisely the algebras presentable by finitely many generators and finitely many relations.

Download

Bibtex

@article{amsw19_2,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lurdes Sousa and Thorsten Wißmann},
title = {Finitely Presentable Algebras For Finitary Monads},
journal = {Theory Appl. Categ.},
year = {2019},
volume = {34},
pages = {1179--1195},
}
Jiří Adámek, Stefan Milius, Lurdes Sousa and Thorsten Wißmann
On Finitary Functors
Theory Appl. Categ., vol. 34, pp. 1134-1164, 2019.

Abstract

A simple criterion for a functor to be finitary is presented: we call $F$ finitely bounded if for all objects $X$ every finitely generated subobject of $FX$ factorizes through the $F$-image of a finitely generated subobject of $X$. This is equivalent to $F$ being finitary for all functors between `reasonable' locally finitely presentable categories, provided that $F$ preserves monomorphisms. We also discuss the question when that last assumption can be dropped.

All this generalizes to locally $\lambda$-presentable categories, $\lambda$-accessible functors and $\lambda$-presentable algebras. As an application we obtain an easy proof that the Hausdorff functor on the category of complete metric spaces is $\aleph_1$-accessible.

Download

Bibtex

@article{amsw19_1,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lurdes Sousa and Thorsten Wißmann},
title = {On Finitary Functors},
journal = {Theory Appl. Categ.},
year = {2019},
volume = {34},
pages = {1134--1164},
}
Hans-Peter Deifel, Stefan Milius, Lutz Schröder and Thorsten Wißmann
Generic Partition Refinement and Weighted Tree Automata
In: Proc. International Symposium on Formal Methods (FM 2019),
Lecture Notes Comput. Sci., vol. 11800, pp. 280-297.

Abstract

Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g.~deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.

Download

Bibtex

@inproceedings{dmsw19,
author = {Hans-Peter Deifel and Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann},
title = {Generic Partition Refinement and Weighted Tree Automata},
booktitle = {Proc. International Symposium on Formal Methods (FM 2019)},
year = {2019},
series = {Lecture Notes Comput. Sci.},
volume = {11800},
pages = {280--297},
}
Ulrich Dorsch, Stefan Milius and Lutz Schröder
Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum
In: Proc. 30th International Conference on Concurrency Theory (CONCUR 2019),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 140, pp. 36:1-36:16.

Abstract

State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time - branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplary proofs of their expressiveness based on our generic criterion.

Download

Bibtex

@inproceedings{dms19,
author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder},
title = {Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum},
booktitle = {Proc. 30th International Conference on Concurrency Theory (CONCUR 2019)},
year = {2019},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {140},
pages = {36:1--36:16},
}
Stefan Milius and Joël Ouaknine (editors)
Special Issue with Selected Papers of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Logical Methods in Computer Science, 2019.
Special issue with selected papers of the conference LICS 2017.

Download

Bibtex

@proceedings{mo19,
editor = {Stefan Milius and Joël Ouaknine},
title = {Special Issue with Selected Papers of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)},
publisher = {},
series = {Logical Methods in Computer Science},
year = {2019},
volume = {},
number = {},
pages = {},
}
Stefan Milius and Henning Urbat
Varieties of Data Languages
In: Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 132, pp. 130:1--130:14.

Abstract

We establish an Eilenberg-type correspondence for data languages, i.e.~languages over an infinite alphabet. More precisely, we prove that there is a bijective correspondence between varieties of languages recognized by orbit-finite nominal monoids and pseudovarieties of such monoids. This is the first result of this kind for data languages. Our approach makes use of nominal Stone duality and a recent category theoretic generalization of Birkhoff-type theorems that we instantiate here for the category of nominal sets. In addition, we prove an axiomatic characterization of weak pseudovarieties as those classes of orbit-finite monoids that can be specified by sequences of nominal equations, which provides a nominal version of a classical theorem of Eilenberg and Schützenberger.

Download

Bibtex

@inproceedings{um19,
author = {Stefan Milius and Henning Urbat},
title = {Varieties of Data Languages},
booktitle = {Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
year = {2019},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {132},
pages = {130:1----130:14},
}
Stefan Milius and Henning Urbat
Equational Axiomatization of Algebras with Structure
In: Proc. 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019),
Lecture Notes Comput. Sci. (ARCoSS), vol. 11425, pp. 400-417.

Abstract

This paper proposes a new category theoretic account of equationally axiomatizable classes of algebras. Our approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. Our main contributions are a generic HSP theorem and a sound and complete equational logic, which are shown to encompass numerous flavors of equational axiomizations studied in the literature.

Download

Bibtex

@inproceedings{mu19,
author = {Stefan Milius and Henning Urbat},
title = {Equational Axiomatization of Algebras with Structure},
booktitle = {Proc. 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019)},
year = {2019},
series = {Lecture Notes Comput. Sci. (ARCoSS)},
volume = {11425},
pages = {400--417},
}
Jiří Adámek and Stefan Milius
On functors preserving coproducts and algebras with iterativity
Theoret. Comput. Sci., vol. 763, pp. 66-87, 2019. Journal version of CALCO 2017 conference paper below.

Abstract

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

Download

Bibtex

@article{am19,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius},
title = {On functors preserving coproducts and algebras with iterativity},
journal = {Theoret. Comput. Sci.},
year = {2019},
volume = {763},
pages = {66--87},
}
Jiří Adámek, Stefan Milius, Rob Myers and Henning Urbat
Generalized Eilenberg theorem: Varieties of languages in a category
ACM Trans. Comput. Log., vol. 20 (1), pp. 3:1-3:47, 2019.

Abstract

For finite automata as coalgebras in a category $\C$ we study languages they accept, and varieties of such languages. This generalizes Eilenberg's concept of a variety of languages which corresponds to choosing as $\Cat$ the category of boolean algebras. Eilenberg established a bijective correspondence between pseudovarieties of monoids and varieties of regular languages. In our generalization we work with a pair $\C/\D$ of locally finite varieties of algebras that are predual, i.e. dualize on the level of finite algebras, and we prove that pseudovarieties of $\D$-monoids bijectively correspond to varieties of regular languages in $\C$. As one instance, Eilenberg's result is recovered by choosing $\D=$ sets and $\Cat=$ boolean algebras. Another instance, Pin's result on pseudovarieties of ordered monoids, is covered by taking $\D=$ posets and $\C=$ distributive lattices. By choosing as $\C=\D$ the self-predual category of join-semilattices we obtain Polák's result on pseudovarieties of idempotent semirings. Similar, using the self-preduality of vector spaces over a finite field $K$, our result covers that of Reutenauer on pseudovarieties of $K$-algebras. Several new variants of Eilenberg's theorem arise by taking other predualities, e.g. between the categories of non-unital boolean rings and of pointed sets. In each of these cases we also prove a local variant of the bijection, where a fixed alphabet is assumed and one considers local varieties of regular languages over that alphabet in the category $\C$.

Download

Bibtex

@article{ammu19,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat},
title = {Generalized Eilenberg theorem: Varieties of languages in a category},
journal = {ACM Trans. Comput. Log.},
year = {2019},
volume = {20},
number = {1},
pages = {3:1--3:47},
}

2018

Stefan Milius and Lawrence S. Moss (editors)
Special Issue in Honor of Jiří Adámek
Logical Methods in Computer Science, 2018.
Special Festschrift Issue celebrating Jiří Adámek's 70th birthday.

Download

Bibtex

@proceedings{mm18,
editor = {Stefan Milius and Lawrence S. Moss},
title = {Special Issue in Honor of Jiří Adámek},
publisher = {},
series = {Logical Methods in Computer Science},
year = {2018},
volume = {},
number = {},
pages = {},
}
Stefan Milius
Proper Functors and Fixed Points for Finite Behaviour
Log. Methods Comput. Sci., vol. 14 (3:22), 32 pp., 2018. Journal version of CALCO'17 conference paper below.

Abstract

The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be fully abstract, i.e.~a subcoalgebra of the final coalgebra. Inspired by Ésik and Maletti's notion of a proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g.~for weighted automata.

Download

Bibtex

@article{milius18,
author = {Stefan Milius},
title = {Proper Functors and Fixed Points for Finite Behaviour},
journal = {Log. Methods Comput. Sci.},
year = {2018},
volume = {14},
number = {3:22},
pages = {32 pp.},
}
Ulrich Dorsch, Stefan Milius, Lutz Schröder and Thorsten Wißmann
Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages
In: Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18),
Lecture Notes Comput. Sci., vol. 11202, pp. 56-77.

Abstract

We introduce a generic expression language describing behaviours of finite coalgebras over sets; besides relational systems, this covers, e.g., weighted, probabilistic, and neighbourhood-based system types. We prove a generic Kleene-type theorem establishing a correspondence between our expressions and finite systems. Our expression language is similar to one introduced in previous work by Myers but has a semantics defined in terms of a particular form of predicate liftings as used in coalgebraic modal logic; in fact, our expressions can be regarded as a particular type of modal fixed point formulas. The predicate liftings in question are required to satisfy a natural preservation property; we show that this property holds in particular for the Moss liftings introduced by Marti and Venema in work on lax extensions.

Download

Bibtex

@inproceedings{dmst18,
author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann},
title = {Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages},
booktitle = {Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18)},
year = {2018},
series = {Lecture Notes Comput. Sci.},
volume = {11202},
pages = {56--77},
}
Jiří Adámek, Stefan Milius and Henning Urbat
On Algebras with Effectful Iteration
In: Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18),
Lecture Notes Comput. Sci., vol. 11202, pp. 144-166.

Abstract

For every finitary monad T on sets and every endofunctor F on the category of T-algebras we introduce the concept of an ffg-Elgot algebra for F, that is, an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad T. The goal of this paper is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point $\phi F$, the colimit of all F-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of T-algebras.

Download

Bibtex

@inproceedings{amu18_cmcs,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},
title = {On Algebras with Effectful Iteration},
booktitle = {Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18)},
year = {2018},
series = {Lecture Notes Comput. Sci.},
volume = {11202},
pages = {144--166},
}
Jiří Adámek, Stefan Milius and Henning Urbat
A Categorical Approach to Syntactic Monoids
Log. Methods Comput. Sci., vol. 14 (2:9), 34 pp., 2018. Journal version of CALCO'15 conference paper below.

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 ordered monoids of Pin (D = posets), the syntactic semirings of Polák (D = semilattices), and the syntactic associative algebras of Reutenauer (D = vector spaces). Assuming that D is a commutative variety of algebras or ordered 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.

Download

Bibtex

@article{amu18,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},
title = {A Categorical Approach to Syntactic Monoids},
journal = {Log. Methods Comput. Sci.},
year = {2018},
volume = {14},
number = {2:9},
pages = {34 pp.},
}
Jiří Adámek, Lawrence S. Moss and Stefan Milius
Fixed Points of Functors
J. Log. Algebr. Methods Program., vol. 95, pp. 41-81, 2018. doi: 10.1016/j.jlamp.2017.11.003.

Abstract

This is a survey on fixed points of endofunctors, including initial algebras and terminal coalgebras. We also consider the rational fixed point, a canonical domain of behavior for finitely presentable systems. In addition to the basic existence theorems for fixed points, several new results are presented. For example, the Smyth-Plotkin theorem that locally continuous endofunctors of DCPO have terminal coalgebras is derived from a new result stating that every locally monotone endofunctor with a fixed point has a terminal coalgebra. We introduce bounded endofunctors on abstract categories and prove that they have terminal coalgebras. We study well-founded coalgebras and prove that for set functors, the largest well-founded coalgebra of every fixed point is the initial algebra. Another new result concerns mixed fixed points: initial algebras and terminal coalgebras of a parametrized accessible functor always form accessible functors.

Download

Bibtex

@article{amm18,
author = {Ji\v{r}\'i Ad\'amek and Lawrence S. Moss and Stefan Milius},
title = {Fixed Points of Functors},
journal = {J. Log. Algebr. Methods Program.},
year = {2018},
volume = {95},
pages = {41--81},
}

2017

Hans-Peter Deifel, Christian Dietrich, Merlin Göttlinger, Daniel Lohmann, Stefan Milius and Lutz Schröder
Automatic Verification of Application-Tailored OSEK Kernels
In: Proc. Formal Methods in Computer Aided Design (FMCAD'17), pp. 196-203.

Abstract

Download

Bibtex

@inproceedings{ddglms17,
author = {Hans-Peter Deifel and Christian Dietrich and Merlin G\"ottlinger and Daniel Lohmann and Stefan Milius and Lutz Schr\"oder},
title = {Automatic Verification of Application-Tailored OSEK Kernels},
booktitle = {Proc. Formal Methods in Computer Aided Design (FMCAD'17)},
year = {2017},
pages = {196--203},
}
Ulrich Dorsch, Stefan Milius, Lutz Schröder and Thorsten Wißmann
Efficient coalgebraic partition refinement
In: Proc. 28th International Conference on Concurrency Theory (CONCUR 2017),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 85, pp. 28:1-28:16.

Abstract

We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log n) where n and m are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.

Download

Bibtex

@inproceedings{dmsw17,
author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann},
title = {Efficient coalgebraic partition refinement},
booktitle = {Proc. 28th International Conference on Concurrency Theory (CONCUR 2017)},
year = {2017},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {85},
pages = {28:1--28:16},
}
Henning Urbat, Jiří Adámek, Liang-Ting Chen and Stefan Milius
Eilenberg Theorems For Free
In: Proc. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS'17),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 83, pp. 43:1-43:15, EATCS Best Paper Award.

Abstract

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

Download

Bibtex

@inproceedings{amu17,
author = {Henning Urbat and Ji\v{r}\'i Ad\'amek and Liang-Ting Chen and Stefan Milius},
title = {Eilenberg Theorems For Free},
booktitle = {Proc. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS'17)},
year = {2017},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {83},
pages = {43:1--43:15},
}
Stefan Milius
Proper Functors and their Rational Fixed Point
In: Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 72, pp. 18:1-18:15.

Abstract

The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be a subcoalgebra of the final coalgebra. Inspired by Ésik and Maletti's notion of proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.

Download

Bibtex

@inproceedings{milius17,
author = {Stefan Milius},
title = {Proper Functors and their Rational Fixed Point},
booktitle = {Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
year = {2017},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {72},
pages = {18:1--18:15},
}
Jiří Adámek and Stefan Milius
On Corecursive Algebras for Functors Preserving Coproducts
In: Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 72, pp. 3:1-3:15.

Abstract

For an endofunctor H on a hyper-extensive category preserving countable coproducts we describe the free corecursive algebra on Y as the coproduct of the terminal coalgebra for H and the free H-algebra on Y. As a consequence, we derive that H is a cia functor, i.e., its corecursive algebras are precisely the cias (completely iterative algebras). Also all functors H(-) + Y are then cia functors. For finitary set functors we prove that, conversely, if H is a cia functor, then it has the form H = W \times (-) + Y for some sets W and Y.

Download

Bibtex

@inproceedings{am17,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius},
title = {On Corecursive Algebras for Functors Preserving Coproducts},
booktitle = {Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17)},
year = {2017},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {72},
pages = {3:1--3:15},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
A presentation of bases for parametrized iterativity
Theory Appl. Categ., vol. 32 (19), pp. 682-718, 2017.

Abstract

Finitary monads on a locally finitely presentable category A are well-known to possess a presentation by signatures and equations. Here we prove that, analogously, bases on A, i.e., finitary functors from A to the category of finitary monads on A, possess a presentation by parametrized signatures and equations.

Download

Bibtex

@article{amv17,
author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil},
title = {A presentation of bases for parametrized iterativity},
journal = {Theory Appl. Categ.},
year = {2017},
volume = {32},
number = {19},
pages = {682--718},
}
Lutz Schröder, Dexter Kozen, Stefan Milius and Thorsten Wißmann
Nominal automata with name binding
In: Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17),
Lecture Notes Comput. Sci. (ARCoSS), vol. 10203, pp. 124-142.

Abstract

Nominal sets are a convenient setting for languages over infinite alphabets, i.e. data languages. We introduce an automaton model over nominal sets, regular nondeterministic nominal automata (RNNA), which have a natural coalgebraic definition using abstraction sets to capture transitions that read a fresh letter from the input word. We prove a Kleene theorem for RNNAs w.r.t. a simple expression language that extends nominal Kleene algebra (NKA) with unscoped name binding, thus remedying the known failure of the expected Kleene theorem for NKA itself. We analyse RNNAs under two notions of freshness: global and local. Under global freshness, RNNAs turn out to be equivalent to session automata, and as such have a decidable inclusion problem. Under local freshness, RNNAs retain a decidable inclusion problem, and translate into register automata. We thus obtain decidability of inclusion for a reasonably expressive class of nondeterministic register automata, with no bound on the number of registers.

Download

Bibtex

@inproceedings{skmw17,
author = {Lutz Schr\"oder and Dexter Kozen and Stefan Milius and Thorsten Wißmann},
title = {Nominal automata with name binding},
booktitle = {Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17)},
year = {2017},
series = {Lecture Notes Comput. Sci. (ARCoSS)},
volume = {10203},
pages = {124--142},
}
Stefan Milius and Tadeusz Litak
Guard your daggers and traces: Properties of guarded (co-)recursion
Fund. Inform., vol. 150 (3-4), pp. 407-449, 2017. Journal version of FICS'13 conference paper below.

Abstract

Motivated by the recent interest in models of guarded (co-)recursion, we study their equational properties. 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, hopefully, towards future description of classifying theories for guarded recursion.

Download

Bibtex

@article{ml17,
author = {Stefan Milius and Tadeusz Litak},
title = {Guard your daggers and traces: Properties of guarded (co-)recursion},
journal = {Fund. Inform.},
year = {2017},
volume = {150},
number = {3-4},
pages = {407--449},
}

2016

Kristof Teichel, Dieter Sibold and Stefan Milius
An attack possibility on time synchronization protocols secured with TESLA-like mechanisms
In: Proc. International Conference on Information Systems Security (ICISS'16),
Lecture Notes Comput. Sci., vol. 10063, pp. 3-22.

Abstract

In network-based broadcast time synchronization, an important security goal is integrity protection linked with source authentication. One technique frequently used to achieve this goal is to secure the communication by means of the TESLA protocol or one of its variants. This paper presents an attack vector usable for time synchronization protocols that protect their broadcast or multicast messages in this manner. The underlying vulnerability results from interactions between timing and security that occur specifically for such protocols. We propose possible countermeasures and evaluate their respective advantages. Furthermore, we discuss our use of the UPPAAL model checker for security analysis and quantification with regard to the attack and countermeasures described, and report on the results obtained. Lastly, we review the susceptibility of three existing cryptographically protected time synchronization protocols to the attack vector discovered.

Download

Bibtex

@inproceedings{tsm16,
author = {Kristof Teichel and Dieter Sibold and Stefan Milius},
title = { An attack possibility on time synchronization protocols secured with TESLA-like mechanisms},
booktitle = {Proc. International Conference on Information Systems Security (ICISS'16)},
year = {2016},
series = {Lecture Notes Comput. Sci.},
volume = {10063},
pages = {3--22},
}
Sergey Goncharov, Stefan Milius and Christoph Rauch
Complete Elgot monads and coalgebraic resumptions
In: Proc. 32nd Conference on Mathematical Foundations of Programming Science (MFPS XXXII),
Electron. Notes Theor. Comput. Sci., vol. 325, pp. 147-168.

Abstract

Monads are used to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. Complete Elgot monads are monads that are equipped with a (uniform) iteration operator satisfying a set of natural axioms, which allows to model iterative computations just as abstractly. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to generalized coalgebraic resumption monads, which were previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of complete Elgot monads and their relationship with generalized coalgebraic resumption monads. We give a characterization of the Eilenberg-Moore algebras of the latter. In fact, we work more generally with Uustalu's \emph{parametrized monads}; we introduce complete Elgot algebras for a parametrized monad and we prove that they form an Eilenberg-Moore category. This is further used for establishing a characterization of complete Elgot monads as those monads whose algebras are coherently equipped with the structure of complete Elgot algebras for the parametrized monads obtained from generalized coalgebraic resumption monads.

Download

Bibtex

@inproceedings{gmr16,
author = {Sergey Goncharov and Stefan Milius and Christoph Rauch},
title = {Complete Elgot monads and coalgebraic resumptions},
booktitle = {Proc. 32nd Conference on Mathematical Foundations of Programming Science (MFPS XXXII)},
year = {2016},
series = {Electron. Notes Theor. Comput. Sci.},
volume = {325},
pages = {147--168},
}
Stefan Milius, Lutz Schröder and Thorsten Wißmann
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.

Download

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},
}
Stefan Milius, Dirk Pattinson and Thorsten Wißmann
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.

Download

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},
}
Liang-Ting Chen, Jiří Adámek, Stefan Milius and Henning Urbat
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.

Download

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

Reiko Heckel and Stefan Milius (editors)
Special Issue with Selected Papers of the 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013
Logical Methods in Computer Science, 2015.
Special issue with selected papers of the conference CALCO'13.

Download

Bibtex

@proceedings{ah15,
editor = {Reiko Heckel and Stefan Milius},
title = {Special Issue with Selected Papers of the 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013},
publisher = {},
series = {Logical Methods in Computer Science},
year = {2015},
volume = {},
number = {},
pages = {},
}
Kristof Teichel, Dieter Sibold and Stefan Milius
First results of a formal analysis of the network time security specification
In: Proc. 2nd International Conference on Research in Security Standardization (SSR'15),
Lecture Notes Comput. Sci., vol. 9497, pp. 218-245.

Abstract

This paper presents a first formal analysis of parts of a draft version of the Network Time Security specification. It presents the protocol model on which we based our analysis, discusses the decision for using the model checker ProVerif and describes how it is applied to analyze the protocol model. The analysis uncovers two possible attacks on the protocol. We present those attacks and show measures that can be taken in order to mitigate them and that have meanwhile been incorporated in the current draft specification.

Download

Bibtex

@inproceedings{tsm15,
author = {Kristof Teichel and Dieter Sibold and Stefan Milius},
title = { First results of a formal analysis of the network time security specification},
booktitle = {Proc. 2nd International Conference on Research in Security Standardization (SSR'15)},
year = {2015},
series = {Lecture Notes Comput. Sci.},
volume = {9497},
pages = {218--245},
}
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.

Download

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},
}
Jiří Adámek, Paul B. Levy, Stefan Milius, Lawrence S. Moss and Lurdes Sousa
On Final Coalgebras of Power-Set Functors and Saturated Trees
Appl. Categ. Structures, vol. 23 (4), pp. 609-641, 2015. 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.

Download

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 = {2015},
volume = {23},
number = {4},
pages = {609--641},
}
Filippo Bonchi, Stefan Milius, Alexandra Silva and Fabio Zanasi
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Henning Urbat
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, CALCO Best Paper Award.

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.

Download

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},
}
Stefan Milius and Thorsten Wißmann
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.

Download

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},
}
Stefan Milius, Dirk Pattinson and Lutz Schröder
Generic Trace Semantics and Graded Monads
In: Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 35, pp. 253-269.

Abstract

Download

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

Download

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 2015)},
year = {2015},
pages = {414--425},
}
Alexander Kurz, Stefan Milius, Dirk Pattinson and Lutz Schröder
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.

Download

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},
}
Jiří Adámek, Stefan Milius, Lawrence S. Moss and Henning Urbat
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.

Download

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.

Download

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},
}
Jiří Adámek, Mahdieh Haddadi and Stefan Milius
Corecursive Algebras, Corecursive Monads and Bloom Monads
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.

Download

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.},
}
Sergey Goncharov, Stefan Milius and Alexandra Silva
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.

Download

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},
}
Henning Basold, Michaela Huhn, Stefan Milius and Henning Günther
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.

Download

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},
}
Filippo Bonchi, Stefan Milius, Alexandra Silva and Fabio Zanasi
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.

Download

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

Download

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},
}
Michaela Huhn and Stefan Milius
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.

Download

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.

Download

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 = {},
}
Stefan Milius and Tadeusz Litak
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.

Download

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.

Download

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},
}
Stefan Milius, Lawrence S. Moss and Daniel Schwencke
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.

Download

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.},
}
Jiří Adámek, Stefan Milius, Lawrence S. Moss and Lurdes Sousa
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.

Download

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.},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Marcello Bonsangue, Stefan Milius and Alexandra Silva
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.

Download

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

Henning Günther, Stefan Milius and M. Oliver Möller
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.

Download

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},
}
Marcello Bonsangue, Stefan Milius and Jurriaan Rot
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.

Download

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
Coproducts of Monads on Set
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Lawrence S. Moss
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.

Download

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},
}
Jiří Adámek, Filippo Bonchi, Mathias Hülsbusch, Barbara König, Stefan Milius and Alexandra Silva
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.

Download

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},
}
Jiří Adámek, Stefan Milius, Lawrence S. Moss and Lurdes Sousa
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.

Download

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.

Download

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

Jiří Adámek, Mahdieh Haddadi and Stefan Milius
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Lawrence S. Moss
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).

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
On second-order iterative monads
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.

Download

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

Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
Iterative reflections of monads
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
Equational Properties of Iterative Monads
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.

Download

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.

Download

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},
}
Stefan Milius, Lawrence S. Moss and Daniel Schwencke
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.

Download

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

Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Abstract

For ideal monads in Set (e.g. the finite list monad, the finite bag monad etc.) we have recently proved that every set generates a free iterative algebra. This gives rise to a new monad. We prove now that this monad is iterative in the sense of Calvin Elgot, in fact, this is the iterative reflection of the given ideal monad. This shows how to freely add unique solutions of recursive equations to a given algebraic theory. Examples: the monad of free commutative binary algebras has the monad of binary rational unordered trees as iterative reflection, and the finite list monad has the iterative reflection given by adding an absorbing element.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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_λ.

Download

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},
}
Stefan Milius, Thorsten Palm and Daniel Schwencke
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.

Download

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.

Download

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},
}
Stefan Milius and Lawrence S. Moss
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.

Download

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},
}
Jiří Adámek, Reinhard Börger, Stefan Milius and Jiří Velebil
Iterative algebras: How iterative are they?
Theory Appl. Categ., vol. 19 (5), 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.

Download

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},
number = {5},
pages = {61--92},
}
Stefan Milius and Lawrence S. Moss
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.

Download

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},
}
Jiří Adámek, Stephen L. Bloom and Stefan Milius
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.

Download

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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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

Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.

Download

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)
Special Issue: 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.

Download

Bibtex

@proceedings{AM_CMCS04,
editor = {Ji\v{r}\'i Ad\'amek and Stefan Milius},
title = {Special Issue: Seventh Workshop on Coalgebraic Methods in Computer Science 2004},
publisher = {Elsevier},
series = {Information and Computation},
year = {2006},
volume = {204},
number = {4},
pages = {435--678},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek and Stefan Milius
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Stefan Milius and Lawrence S. Moss
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.

Download

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

Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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 .

Download

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.

Download

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},
}
Stefan Milius and Lawrence S. Moss
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.

Download

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

Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

Bibtex

@article{amv_classes,
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

Peter Aczel, Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.

Download

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

Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

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.

Download

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},
}
Jiří Adámek, Stefan Milius and Jiří Velebil
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.

Download

Bibtex

@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},
}