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.281406173, abstract = {The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found in 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 infnite variant of such games lead to a novel notion of infnite-depth graded semantics. Under reasonable restrictions, the infnite-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.}, author = {Ford, Matthew and Milius, Stefan and Schröder, Lutz and Beohar, Harsh and König, Barbara}, booktitle = {Proceedings - Symposium on Logic in Computer Science}, date = {2022-08-02/2022-08-05}, doi = {10.1145/3531130.3533374}, faupublication = {yes}, isbn = {9781450393515}, keywords = {Behavioural equivalence; Games; Graded monads; Lineartime/branching-time spectrum; Semantics}, note = {CRIS-Team Scopus Importer:2022-09-09}, peerreviewed = {unknown}, publisher = {Institute of Electrical and Electronics Engineers Inc.}, title = {{Graded} {Monads} and {Behavioural} {Equivalence} {Games}}, venue = {Haifa, ISR}, year = {2022} } @inproceedings{faucris.226669056, 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.}, author = {Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2019-08-27/2019-08-30}, doi = {10.4230/LIPIcs.CONCUR.2019.36}, editor = {Wan Fokkink, Rob van Glabbeek}, faupublication = {yes}, isbn = {9783959771214}, keywords = {Branching Time; Expressiveness; Linear Time; Modal Logics; Monads; System Equivalences}, note = {CRIS-Team Scopus Importer:2019-09-17}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Graded} monads and graded logics for the linear time – {Branching} time spectrum}, venue = {Amsterdam}, volume = {140}, year = {2019} } @inproceedings{faucris.118714904, address = {Cornell}, author = {Milius, Stefan and Litak, Tadeusz}, booktitle = {Proc. Fixed Points in Computer Science}, doi = {10.4204/EPTCS.126.6}, faupublication = {yes}, keywords = {Electron. Proc. Theoret. Comput. Sci.}, note = {UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes{\_}1.guardy}, pages = {72-86}, publisher = {Cornell University Library}, series = {Electronic Proceedings in Theoretical Computer Science}, title = {{Guard} {Your} {Daggers} and {Traces}: {On} {The} {Equational} {Properties} of {Guarded} ({Co}-)recursion}, url = {https://www8.cs.fau.de/~milius/publications/files/ml{\_}fics13.pdf}, volume = {126}, year = {2013} } @article{faucris.108440464, author = {Milius, Stefan and Litak, Tadeusz}, doi = {10.3233/FI-2017-1475}, faupublication = {yes}, journal = {Fundamenta Informaticae}, keywords = {guarded fixpoint, guarded trace, iteration, equational properties}, note = {UnivIS-Import:2017-03-24:Pub.2017.tech.IMMD.profes{\_}1.guardy}, pages = {407-449}, peerreviewed = {Yes}, title = {{Guard} {Your} {Daggers} and {Traces}: {Properties} of {Guarded} ({Co}-)recursion}, url = {http://arxiv.org/abs/1603.05214}, year = {2017} } @inproceedings{faucris.311727087, abstract = {We present a higher-order extension of Turi and Plotkin's abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe's method is developed. It encompasses, for instance, Abramsky's classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.}, author = {Goncharov, Sergey and Milius, Stefan and Schröder, Lutz and Tsampas, Stylianos and Urbat, Henning}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2023-06-19/2023-06-21}, doi = {10.4230/LIPIcs.CALCO.2023.24}, editor = {Paolo Baldan, Valeria de Paiva}, faupublication = {yes}, isbn = {9783959772877}, keywords = {Abstract GSOS; applicative bisimilarity; bialgebra; lambda-calculus}, note = {CRIS-Team Scopus Importer:2023-10-06}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Higher}-{Order} {Mathematical} {Operational} {Semantics}}, venue = {Bloomington, IN, USA}, volume = {270}, year = {2023} } @article{faucris.109686544, author = {Adámek, Jiří and Milius, Stefan and Velebil, Jiří}, faupublication = {yes}, journal = {Information and Computation}, pages = {83--118}, peerreviewed = {Yes}, title = {{How} {Iterative} {Reflections} of {Monads} are {Constructed}}, volume = {225}, year = {2013} } @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} } @inproceedings{faucris.326406654, abstract = {The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra construction by Adámek (1974) starts with the initial object (e.g. the empty set) and successively applies the functor until a fixed point is reached, an idea inspired by Kleene's fixed point theorem. Depending on the functor of interest, this may require transfinitely many steps indexed by ordinal numbers until termination.We provide a new initial algebra construction which is not based on an ordinal-indexed chain. Instead, our construction is loosely inspired by Pataraia's fixed point theorem and forms the colimit of all finite recursive coalgebras. This is reminiscent of the construction of the rational fixed point of an endofunctor that forms the colimit of all finite coalgebras. For our main correctness theorem, we assume the given endofunctor is accessible on a (weak form of) locally presentable category. Our proofs are constructive and fully formalized in Agda.}, author = {Wißmann, Thorsten and Milius, Stefan}, booktitle = {Proceedings - Symposium on Logic in Computer Science}, date = {2024-07-08/2024-07-11}, doi = {10.1145/3661814.3662105}, faupublication = {yes}, isbn = {9798400706608}, keywords = {agda; initial algebra; presentable category; recursive coalgebra}, note = {CRIS-Team Scopus Importer:2024-07-26}, peerreviewed = {unknown}, publisher = {Institute of Electrical and Electronics Engineers Inc.}, title = {{Initial} {Algebras} {Unchained} - {A} {Novel} {Initial} {Algebra} {Construction} {Formalized} in {Agda}}, venue = {Tallinn, EST}, year = {2024} } @inproceedings{faucris.267484946, 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.}, author = {Adámek, Jiří and Milius, Stefan and Moss, Lawrence S.}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2021-08-31/2021-09-03}, doi = {10.4230/LIPIcs.CALCO.2021.5}, editor = {Fabio Gadducci, Alexandra Silva, Alexandra Silva}, faupublication = {yes}, isbn = {9783959772129}, keywords = {Initial algebra; Initial-algebra chain; Pataraia’s theorem; Recursive coalgebra}, note = {CRIS-Team Scopus Importer:2021-12-24}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Initial} algebras without iteration}, venue = {Virtual, Salzburg, AUT}, volume = {211}, year = {2021} } @article{faucris.123486924, abstract = {We propose an abstract framework for modelling state-based systems with internal behaviour as e.g. given by silent or ε-transitions. Our approach employs monads with a parametrized fixpoint operator † to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems and non-deterministic transducers.}, author = {Bonchi, Filippo and Milius, Stefan and Silva, Alexandra and Zanasi, Fabio}, doi = {10.1016/j.tcs.2015.03.024}, faupublication = {yes}, journal = {Theoretical Computer Science}, keywords = {Coalgebras on kleisli categories; Epsilon transitions; Mazurkiewicz traces; Non-deterministic transducers; Parametrized fixpoint operator; Trace semantics}, note = {UnivIS-Import:2016-06-01:Pub.2015.tech.IMMD.profes{\_}1.killin}, pages = {102-126}, peerreviewed = {Yes}, title = {{Killing} {Epsilons} with a {Dagger}: {A} {Coalgebraic} {Study} of {Systems} with {Algebraic} {Label} {Structure}}, volume = {604}, year = {2015} } @inproceedings{faucris.267485203, 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 (λ = ω1). 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 ω1-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.}, author = {Ford, Matthew and Milius, Stefan and Schröder, Lutz}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2021-08-31/2021-09-03}, doi = {10.4230/LIPIcs.CALCO.2021.14}, editor = {Fabio Gadducci, Alexandra Silva, Alexandra Silva}, faupublication = {yes}, isbn = {9783959772129}, keywords = {Horn theories; Monads; Relational logic; Relational structures}, note = {CRIS-Team Scopus Importer:2021-12-24}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Monads} on categories of relational structures}, venue = {Virtual, Salzburg, AUT}, volume = {211}, year = {2021} } @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.264571526, 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.}, author = {Urbat, Henning and Hausmann, Daniel and Milius, Stefan and Schröder, Lutz}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2021-08-24/2021-08-27}, doi = {10.4230/LIPIcs.CONCUR.2021.4}, editor = {Serge Haddad, Daniele Varacca}, faupublication = {yes}, isbn = {9783959772037}, keywords = {Data languages; Inclusion checking; Infinite words; Nominal sets}, note = {CRIS-Team Scopus Importer:2021-10-01}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Nominal} {Büchi} {Automata} with {Name} {Allocation}}, venue = {Virtual, Online}, volume = {203}, year = {2021} } @inproceedings{faucris.309432942, 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.}, author = {Birkmann, Fabian and Milius, Stefan and Urbat, Henning}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2023-07-10/2023-07-14}, doi = {10.4230/LIPIcs.ICALP.2023.114}, editor = {Kousha Etessami, Uriel Feige, Gabriele Puppis}, faupublication = {yes}, isbn = {9783959772785}, keywords = {Data languages; Nominal sets; Profinite space; Stone duality}, note = {CRIS-Team Scopus Importer:2023-08-18}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Nominal} {Topology} for {Data} {Languages}}, venue = {Paderborn}, volume = {261}, year = {2023} } @inproceedings{faucris.261334143, 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.}, author = {Myers, Robert S.R. and Milius, Stefan and Urbat, Henning}, booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, date = {2021-03-27/2021-04-01}, doi = {10.1007/978-3-030-71995-1{\_}23}, editor = {Stefan Kiefer, Christine Tasson}, faupublication = {yes}, isbn = {9783030719944}, note = {CRIS-Team Scopus Importer:2021-07-09}, pages = {448-468}, peerreviewed = {unknown}, publisher = {Springer Science and Business Media Deutschland GmbH}, title = {{Nondeterministic} syntactic complexity}, venue = {Online}, volume = {12650}, year = {2021} } @article{faucris.109785544, author = {Huhn, Michaela and Milius, Stefan}, faupublication = {yes}, journal = {Science of Computer Programming}, pages = {150--168}, peerreviewed = {Yes}, title = {{Observations} on formal safety analysis in practice}, volume = {80A}, year = {2014} } @inproceedings{faucris.203758915, address = {Heidelberg}, author = {Milius, Stefan and Adámek, Jiří and Urbat, Henning}, booktitle = {Proc.~Coalgebraic Methods in Computer Science (CMCS'18)}, editor = {Corina Cîrstea}, faupublication = {yes}, peerreviewed = {Yes}, publisher = {Springer}, series = {Lecture Notes Comput.~Sci.}, title = {{On} {Algebras} with {Effectful} {Iteration}}, venue = {Thessaloniki}, year = {2018} } @article{faucris.117709724, 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.}, author = {Adámek, Jiří and Milius, Stefan and Myers, Robert and Urbat, Henning and Urbat, Henning}, doi = {10.1016/j.entcs.2014.10.002}, faupublication = {yes}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {Canonical Nondeterministic Automata; Closure Spaces; Semilattices; State Minimality}, note = {UnivIS-Import:2015-03-09:Pub.2014.tech.IMMD.profes{\_}1.oncont}, pages = {3-23}, peerreviewed = {unknown}, title = {{On} {Continuous} {Nondeterminism} and {State} {Minimality}}, url = {http://www8.cs.fau.de/publications}, volume = {308}, year = {2014} } @inproceedings{faucris.109750784, author = {Adámek, Jiří and Milius, Stefan}, booktitle = {Proc.~7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17)}, editor = {Bonchi F, König B}, faupublication = {yes}, pages = {3:1--3:15}, peerreviewed = {Yes}, publisher = {Schloss Dagstuhl}, series = {LIPIcs}, title = {{On} {Corecursive} {Algebras} for {Functors} {Preserving} {Coproducts}}, volume = {72}, year = {2017} } @article{faucris.114029564, abstract = {The final coalgebra for the finite power-set functor was described by Worrell who also proved that the final chain converges in ω+ω steps. We describe the step ω 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

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