inducing various notions of process equivalence, ranging from

linear-time semantics such as trace equivalence to branching-time

semantics such as strong bisimilarity. Many of these generalize to

system types beyond standard transition systems, featuring, for

example, weighted, probabilistic, or game-based transitions; this

motivates the search for suitable coalgebraic abstractions of

process equivalence that cover these orthogonal dimensions of

generality, i.e.~are generic both in the system type and in the

notion of system equivalence. In recent joint work with Kurz, we

have proposed a parametrization of system equivalence over an

embedding of the coalgebraic type functor into a monad. In the

present paper, we refine this abstraction to use graded

monads, which come with a notion of depth that corresponds, e.g.,

to trace length or bisimulation depth. We introduce a notion of

graded algebras and show how they play the role of formulas in trace

logics.

}, address = {Dagstuhl}, author = {Milius, Stefan and Pattinson, Dirk and Schröder, Lutz}, booktitle = {6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015}, date = {2015-06-24/2015-06-26}, doi = {10.4230/LIPIcs.CALCO.2015.253}, faupublication = {yes}, keywords = {Graded monad; traces; concurrent systems; bisimilarity; graded algebra; trace logic;}, pages = {253--269}, peerreviewed = {Yes}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Generic} {Trace} {Semantics} and {Graded} {Monads}}, venue = {Nijmegen}, year = {2015} } @inproceedings{faucris.223100924, 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.}, author = {Urbat, Henning and Milius, Stefan}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2019-07-09/2019-07-12}, doi = {10.4230/LIPIcs.ICALP.2019.130}, editor = {Ioannis Chatzigiannakis, Christel Baier, Stefano Leonardi, Paola Flocchini}, faupublication = {yes}, isbn = {9783959771092}, keywords = {Algebraic language theory; Data languages; Nominal sets; Stone duality}, note = {CRIS-Team Scopus Importer:2019-07-26}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Varieties} of data languages}, venue = {Patras}, volume = {132}, year = {2019} } @inproceedings{faucris.119800384, 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 [16]. Finally, the initial iterative algebra consists of all finite well-pointed coalgebras. Numerous examples are discussed e.g. automata, graphs, and labeled transition systems. © 2012 Springer-Verlag Berlin Heidelberg.}, address = {Berlin/Heidelberg}, author = {Adámek, Jiří and Milius, Stefan and Moss, Lawrence and Sousa, Lurdes}, booktitle = {Foundations of Software Science and Computational Structures}, date = {2012-03-24/2012-04-01}, doi = {10.1007/978-3-642-28729-9_6}, faupublication = {no}, isbn = {978-3-642-28728-2}, note = {UnivIS-Import:2015-04-16:Pub.2012.tech.IMMD.profes_1.wellpo_2}, pages = {89-103}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, title = {{Well}-{Pointed} {Coalgebras} ({Extended} {Abstract})}, venue = {Tallinn, Estonia}, volume = {7213}, year = {2012} } @incollection{faucris.117722704, 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 lineartime/ 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.}, address = {Berlin}, author = {Kurz, Alexander and Milius, Stefan and Pattinson, Dirk and Schröder, Lutz}, booktitle = {Software, Services, and Systems}, doi = {10.1007/978-3-319-15545-6_8}, faupublication = {yes}, keywords = {Trace semantics; monads; coalgebra}, note = {UnivIS-Import:2015-03-09:Pub.2015.tech.IMMD.profes_1.simpli}, pages = {75-90}, peerreviewed = {unknown}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{Simplified} {Coalgebraic} {Trace} {Equivalence}}, url = {https://www8.cs.fau.de/publications}, volume = {8950}, year = {2015} } @inproceedings{faucris.217155885, 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.}, author = {Milius, Stefan and Urbat, Henning}, booktitle = {22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019)}, doi = {10.1007/978-3-030-17127-8_23}, editor = {Mikolaj Bojanczyk, Alex Simpson}, faupublication = {yes}, note = {CRIS-Team Scopus Importer:2019-05-09}, pages = {400-417}, peerreviewed = {unknown}, publisher = {Springer Verlag}, title = {{Equational} {Axiomatization} of {Algebras} with {Structure}}, volume = {11425 LNCS}, year = {2019} } @inproceedings{faucris.118582904, 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. © 2012 IFIP International Federation for Information Processing.}, address = {Berlin Heidelberg}, author = {Adámek, Jiří and Milius, Stefan and Moss, Lawrence}, booktitle = {Coalgebraic Methods in Computer Science}, date = {2012-03-31/2012-04-01}, doi = {10.1007/978-3-642-32784-1_4}, faupublication = {no}, isbn = {978-3-642-32783-4}, keywords = {Finitary functors; Hausdorff functor; presentation of functors}, note = {UnivIS-Import:2015-04-16:Pub.2012.tech.IMMD.profes_1.onfini}, pages = {51-70}, publisher = {Springer-verlag}, series = {Lecture Notes in Computer Science}, title = {{On} {Finitary} {Functors} and {Their} {Presentations}}, url = {http://link.springer.com/chapter/10.1007%2F978-3-642-32784-1_4}, venue = {Tallin, Estonia}, volume = {7399}, year = {2012} } @inproceedings{faucris.123827704, author = {Schröder, Lutz and Kozen, Dexter and Milius, Stefan and Wißmann, Thorsten}, booktitle = {Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)}, date = {2017-04-22/2017-04-29}, editor = {Esparza Javier, Murawski Andrzej}, faupublication = {yes}, keywords = {Nominal sets; automata over infinite alphabets; inclusion checking; coalgebra}, peerreviewed = {Yes}, publisher = {Springer}, series = {Lecture Notes Comput.~Sci. (ARCoSS)}, title = {{Nominal} {Automata} with {Name} binding}, venue = {Uppsala}, year = {2017} } @inproceedings{faucris.118780684, abstract = {We propose an abstract framework for modeling state-based systems with internal behavior 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. © 2014 IFIP International Federation for Information Processing.}, address = {Berlin/Heidelberg}, author = {Bonchi, Filippo and Milius, Stefan and Silva, Alexandra and Zanasi, Fabio}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'14)}, date = {2014-04-05/2014-04-06}, doi = {10.1007/978-3-662-44124-4_4}, faupublication = {yes}, isbn = {978-3-662-44124-4}, note = {UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.howtok}, pages = {53-74}, publisher = {Springer}, title = {{How} to {Kill} {Epsilons} with a {Dagger}: {A} {Coalgebraic} {Take} on {Systems} with {Algebraic} {Label} {Structure}}, url = {http://www8.cs.fau.de/publications}, venue = {Grenoble, France}, volume = {8446}, year = {2014} } @article{faucris.109775644, author = {Adámek, Jiří and Milius, Stefan and Moss, Lawrence}, faupublication = {yes}, journal = {Journal of Logical and Algebraic Methods in Programming}, pages = {41--81}, peerreviewed = {Yes}, title = {{Fixed} {Points} of {Functors}}, volume = {95}, year = {2018} } @article{faucris.107011344, author = {Adámek, Jiří and Milius, Stefan and Velebil, Jiří}, faupublication = {yes}, journal = {Theory and Applications of Categories}, pages = {682--718}, peerreviewed = {Yes}, title = {{A} {Presentation} of {Bases} for {Parametrized} {Iterativity}}, volume = {32}, year = {2017} } @article{faucris.203758070, author = {Adámek, Jiří and Milius, Stefan and Urbat, Henning}, doi = {10.23638/LMCS-14(2:9)2018}, faupublication = {yes}, journal = {Logical Methods in Computer Science}, pages = {34 pp.}, peerreviewed = {Yes}, title = {{A} {Categorical} {Approach} to {Syntactic} {Monoids}}, url = {https://arxiv.org/pdf/1804.03011v2.pdf}, volume = {14}, year = {2018} } @inproceedings{faucris.203758665, author = {Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz and Wißmann, Thorsten}, booktitle = {Proc.~Coalgebraic Methods in Computer Science (CMCS'18)}, editor = {Corina Cîrstea}, faupublication = {yes}, peerreviewed = {Yes}, publisher = {Springer}, title = {{Predicate} {Liftings} and {Functor} {Presentations} in {Coalgebraic} {Expression} {Languages}}, venue = {Thessaloniki}, year = {2018} } @article{faucris.214173580, 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 exist among standard finitary set functors: in fact, the only ones are those preserving coproducts; they are given by X bar right arrow W x (-) + Y for some sets W and Y. (C) 2019 Elsevier B.V. All rights reserved.}, author = {Adamek, Jiri and Milius, Stefan}, doi = {10.1016/j.tcs.2019.01.018}, faupublication = {yes}, journal = {Theoretical Computer Science}, note = {CRIS-Team WoS Importer:2019-03-22}, pages = {66-87}, peerreviewed = {Yes}, title = {{On} functors preserving coproducts and algebras with iterativity}, volume = {763}, year = {2019} }