A coalgebraic treatment of conditional transition systems with upgrades - Harsh, Beohar; König, Barbara; Küpper, Sebastian; Silva, Alexandra; Wißmann, Thorsten (Logical Methods in Computer Science, 2018)
Keywords: Computer Science - Logic in Computer Science

A coalgebraic view on reachability - Wißmann, Thorsten; Milius, Stefan; Katsumata, Shin-Ya; Dubut, Jeremy (Commentationes Mathematicae Universitatis Carolinae, 2019)
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.
CRIS-Team WoS Importer:2020-02-04

Action Codes - Vaandrager, Frits; Wißmann, Thorsten (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
We provide a new perspective on the problem how high-level state machine models with abstract actions can be related to low-level models in which these actions are refined by sequences of concrete actions. We describe the connection between high-level and low-level actions using action codes, a variation of the prefix codes known from coding theory. For each action code R, we introduce a contraction operator αR that turns a low-level model M into a high-level model, and a refinement operator ϱR that transforms a high-level model N into a low-level model. We establish a Galois connection ϱR(N) M N αR(M), where is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model M. To this end, we also introduce a concretization operator γR, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection αR(M) N M γR(N). Action codes may be used to construct adaptors that translate between concrete and abstract actions during learning and testing of Mealy machines. If Mealy machine M models a black-box system then αR(M) describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code R. Whenever αR(M) implements (or conforms to) N, we may conclude that M implements (or conforms to) γR(N). Almost all results, examples, and counter-examples are formalized in Coq.
CRIS-Team Scopus Importer:2023-08-18
Keywords: Action Codes; Action Contraction; Action Refinement; Automata; Galois Connection; LTS; Model Learning; Model-Based Testing; Models of Reactive Systems

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

A New Foundation for Finitary Corecursion - Milius, Stefan; Pattinson, Dirk; Wißmann, Thorsten (Foundations of Software Science and Computation Structures, 2016)
UnivIS-Import:2017-03-24:Pub.2016.tech.IMMD.profes_1.anewfo
Keywords: coalgebra; rational fixed point; corecursion; locally finite fixed point

Bisimilar States in Uncertain Structures - Rot, Jurriaan; Wißmann, Thorsten (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in automata learning algorithms, where one investigates whether two observed behaviours come from the same internal state of a black-box system that can not be transparently inspected. We model this uncertainty as a set functor equipped with a partial order which describes possible future developments of the learning game. On such a functor, we provide a lifting-based definition of uncertain bisimilarity and verify basic properties. Beside its applications to Mealy machines, a natural model for automata learning, our framework also instantiates to an existing compatibility relation on suspension automata, which are used in model-based testing. We show that uncertain bisimilarity is a necessary but not sufficient condition for two states being implementable by the same state in the black-box system. We remedy the lack of sufficiency by a characterization of uncertain bisimilarity in terms of coalgebraic simulations.
CRIS-Team Scopus Importer:2023-10-06
Keywords: Bisimilarity; Coalgebra; ioco; Mealy Machines; Relation Lifting

Coalgebra encoding for efficient minimization - Deifel, Hans-Peter; Milius, Stefan; Wißmann, Thorsten (Leibniz International Proceedings in Informatics, LIPIcs, 2021)
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.
CRIS-Team Scopus Importer:2021-10-01
Keywords: Coalgebra; Minimization; Partition refinement; Transition systems

COOL — A Generic Reasoner for Coalgebraic Hybrid Logics (System Description) - Gorin, Daniel; Pattinson, Dirk; Schröder, Lutz; Widmann, Florian; Wißmann, Thorsten (Automated Reasoning, 2014)
We describe the Coalgebraic Ontology Logic solver Cool, a generic reasoner that decides the satisfiability of modal (and, more generally, hybrid) formulas with respect to a set of global assumptions-in Description Logic parlance, we support a general TBox and internalize a Boolean ABox. The level of generality is that of coalgebraic logic, a logical framework covering a wide range of modal logics, beyond relational semantics. The core of Cool is an efficient unlabelled tableaux search procedure using global caching. Concrete logics are added by implemening the corresponding (one-step) tableaux rules. The logics covered at the moment include standard relational examples as well as graded modal logic and Pauly's Coalition Logic (the next-step fragment of Alternating-time Temporal Logic), plus every logic that arises as a fusion of the above. We compare the performance of Cool with state-of-the-art reasoners. © 2014 Springer International Publishing Switzerland.
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.coolag

Efficient and Modular Coalgebraic Partition Refinement - Wißmann, Thorsten; Dorsch, Ulrich; Milius, Stefan; Schröder, Lutz (Logical Methods in Computer Science, 2020)
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)" role="presentation">(𝑚⋅log𝑛) where n" role="presentation">𝑛 and m" role="presentation">𝑚 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.

Efficient Coalgebraic Partition Refinement - Dorsch, Ulrich; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (Proc. 28th International Conference on Concurrency Theory (CONCUR 2017), 2017)

Explaining Behavioural Inequivalence Generically in Quasilinear Time - Wißmann, Thorsten; Milius, Stefan; Schröder, Lutz (Leibniz International Proceedings in Informatics, LIPIcs, 2021)
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).
CRIS-Team Scopus Importer:2021-10-01
Keywords: Bisimulation; Coalgebra; Distinguishing formulae; Modal logic; Partition refinement

Fast Coalgebraic Bisimilarity Minimization - Jacobs, Jules; Wißmann, Thorsten (Proceedings of the ACM on Programming Languages, 2023)
Coalgebraic bisimilarity minimization generalizes classical automaton minimization to a large class of automata whose transition structure is specified by a functor, subsuming strong, weighted, and probabilistic bisimilarity. This offers the enticing possibility of turning bisimilarity minimization into an off-the-shelf technology, without having to develop a new algorithm for each new type of automaton. Unfortunately, there is no existing algorithm that is fully general, efficient, and able to handle large systems. We present a generic algorithm that minimizes coalgebras over an arbitrary functor in the category of sets as long as the action on morphisms is sufficiently computable. The functor makes at most O(m logn) calls to the functor-specific action, where n is the number of states and m is the number of transitions in the coalgebra. While more specialized algorithms can be asymptotically faster than our algorithm (usually by a factor of (m/n)), our algorithm is especially well suited to efficient implementation, and our tool often uses much less time and memory on existing benchmarks, and can handle larger automata, despite being more generic.
Created from Fastlane, Scopus look-up
Keywords: Coalgebra; Monotone Neighbourhoods; Partition Refinement

Finitary Corecursion for the Infinitary Lambda Calculus - Milius, Stefan; Wißmann, Thorsten (Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, 2015)
UnivIS-Import:2016-06-01:Pub.2015.tech.IMMD.profes_1.finita
Keywords: rational trees; infinitary lambda calculus; coinduction

Finitely presentable algebras for finitary monads - Adámek, J.; Milius, Stefan; Sousa, L.; Wißmann, Thorsten (Theory and Applications of Categories, 2019)
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.
CRIS-Team Scopus Importer:2019-11-29
Keywords: Finitary functor; Finitely generated object; Finitely presentable object; Regular monad

From generic partition refinement to weighted tree automata minimization - Wißmann, Thorsten; Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz (Formal Aspects of Computing, 2021)
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.
Created from Fastlane, WoS look-up

Generic Partition Refinement and Weighted Tree Automata - Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (Formal Methods – The Next 30 Years, 2019)
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.

Initial Algebras Unchained - A Novel Initial Algebra Construction Formalized in Agda - Wißmann, Thorsten; Milius, Stefan (Proceedings - Symposium on Logic in Computer Science, 2024)
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.
CRIS-Team Scopus Importer:2024-07-26
Keywords: agda; initial algebra; presentable category; recursive coalgebra

Nominal Automata with Name binding - Schröder, Lutz; Kozen, Dexter; Milius, Stefan; Wißmann, Thorsten (Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), 2017)
Keywords: Nominal sets; automata over infinite alphabets; inclusion checking; coalgebra

On Finitary Functors - Adámek, Jiří; Milius, Stefan; Sousa, Lourdes; Wißmann, Thorsten (Theory and Applications of Categories, 2019)

Path Category for Free: Open Morphisms from Coalgebras with Non-deterministic Branching - Wißmann, Thorsten; Dubut, Jérémy; Katsumata, Shin ya; Hasuo, Ichiro (22nd International Conference, FOSSACS 2019, 2019)
There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebra for a functor G, where a bisimulation is defined as a span of G-coalgebra homomorphism. Another one is in terms of path categories and open morphisms, where a bisimulation is defined as a span of open morphisms. This similarity is no coincidence: given a functor G, fulfilling certain conditions, we derive a path-category for pointed G-coalgebras and lax homomorphisms, such that the open morphisms turn out to be precisely the G-coalgebra homomorphisms. The above construction provides path-categories and trace semantics for free for different flavours of transition systems: (1) non-deterministic tree automata (2) regular nondeterministic nominal automata (RNNA), an expressive automata notion living in nominal sets (3) multisorted transition systems. This last instance relates to Lasota’s construction, which is in the converse direction.
CRIS-Team Scopus Importer:2019-05-09
Keywords: Categories; Coalgebra; Nominal sets; Open maps

Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages - Dorsch, Ulrich; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (Proc. Coalgebraic Methods in Computer Science (CMCS'18), 2018)

QUASILINEAR-TIME COMPUTATION OF GENERIC MODAL WITNESSES FOR BEHAVIOURAL INEQUIVALENCE - Wißmann, Thorsten; Milius, Stefan; Schröder, Lutz (Logical Methods in Computer Science, 2022)
We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nonde-terministic, 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).
CRIS-Team Scopus Importer:2022-11-25
Keywords: bisimulation; coalgebra; distinguishing formulae; modal logic; partition refinement

Reasoning with Bounded Self-reference Using Logical Interpreters - Gorin, Daniel; Schröder, Lutz; Wißmann, Thorsten (Proc. 26th International Workshop on Description Logics, DL 2013, 2013)
Self-referential concepts in description logic may formally be viewed as concepts that at some point mention an individual previously encountered in the evaluation; this corresponds to a restricted form of the down-arrow binder known from hybrid logic. Typical examples include being a narcissist, (someone who loves himself); a celebrity (someone who is known by everyone she meets) or a grant application reviewer (who can only review proposals of researchers with whom she did not collaborate in the past). While reasoning in ALC plus self-reference is known to be undecidable, it has recently been shown that one can often safely restrict self-reference to at most two indirections (allowing the definition of narcissists and celebrities, but not of grant reviewers). In particular, the extension of ALCQ with this construct has an expressive power roughly equivalent to ALCHIQ plus safe Boolean combinations of roles. Here, we discuss a translation-based approach to reasoning in this logic. The translation goes into ALCHIQ (without Boolean roles) and therefore can be used in combination with off-the-shelf reasoners for OWL. The translation strategy encodes the semantics of the source axiomatically in the target logic. We use an implementation of this type of translations to evaluate the feasibility of the whole approach.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.reason

Regular Behaviours with Names - On Rational Fixpoints of Endofunctors on Nominal Sets - Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (Applied Categorical Structures, 2016)
Keywords: Nominal sets; rational fixpoints; regular languages; coalgebra

Supported Sets – A New Foundation for Nominal Sets and Automata - Wißmann, Thorsten (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
The present work proposes and discusses the category of supported sets which provides a uniform foundation for nominal sets of various kinds, such as those for equality symmetry, for the order symmetry, and renaming sets. We show that all these differently flavoured categories of nominal sets are monadic over supported sets. Thus, supported sets provide a canonical finite way to represent nominal sets and the automata therein, e.g. register automata and coalgebras in general. Name binding in supported sets is modelled by a functor following the idea of de Bruijn indices. This functor lifts to the well-known abstraction functor in nominal sets. Together with the monadicity result, this gives rise to a transformation process from finite coalgebras in supported sets to orbit-finite coalgebras in nominal sets. One instance of this process transforms the finite representation of a register automaton in supported sets into its configuration automaton in nominal sets.
Created from Fastlane, Scopus look-up
Keywords: Coalgebra; LFP-Category; Monads; Nominal Sets; Supported Sets

Weighted and Branching Bisimilarities from Generalized Open Maps - Dubut, Jérémy; Wißmann, Thorsten (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2023)
In the open map approach to bisimilarity, the paths and their runs in a given state-based system are the first-class citizens, and bisimilarity becomes a derived notion. While open maps were successfully used to model bisimilarity in non-deterministic systems, the approach fails to describe quantitative system equivalences such as probabilistic bisimilarity. In the present work, we see that this is indeed impossible and we thus generalize the notion of open maps to also accommodate weighted and probabilistic bisimilarity. Also, extending the notions of strong path and path bisimulations into this new framework, we show that branching bisimilarity can be captured by this extended theory and that it can be viewed as the history preserving restriction of weak bisimilarity.
CRIS-Team Scopus Importer:2023-07-14
Keywords: Branching Bisimilarity; Open maps; Probabilistic Bisimilarity; Weak Bisimilarity; Weighted Bisimilarity