% Encoding: UTF-8
@COMMENT{BibTeX export based on data in FAU CRIS: https://cris.fau.de/}
@COMMENT{For any questions please write to cris-support@fau.de}
@article{faucris.203998246,
author = {Harsh, Beohar and König, Barbara and Küpper, Sebastian and Silva, Alexandra and Wißmann, Thorsten},
doi = {10.23638/LMCS-14(1:19)2018},
faupublication = {yes},
journal = {Logical Methods in Computer Science},
keywords = {Computer Science - Logic in Computer Science},
peerreviewed = {Yes},
title = {{A} coalgebraic treatment of conditional transition systems with upgrades},
url = {https://lmcs.episciences.org/4330/pdf},
volume = {Volume 14, Issue 1},
year = {2018}
}
@article{faucris.233254775,
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.},
author = {Wißmann, Thorsten and Milius, Stefan and Katsumata, Shin-Ya and Dubut, Jeremy},
doi = {10.14712/1213-7243.2019.026},
faupublication = {yes},
journal = {Commentationes Mathematicae Universitatis Carolinae},
month = {Jan},
note = {CRIS-Team WoS Importer:2020-02-04},
pages = {605-638},
peerreviewed = {unknown},
title = {{A} coalgebraic view on reachability},
volume = {60},
year = {2019}
}
@inproceedings{faucris.309433199,
abstract = {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.},
author = {Vaandrager, Frits and Wißmann, Thorsten},
booktitle = {Leibniz International Proceedings in Informatics, LIPIcs},
date = {2023-07-10/2023-07-14},
doi = {10.4230/LIPIcs.ICALP.2023.137},
editor = {Kousha Etessami, Uriel Feige, Gabriele Puppis},
faupublication = {yes},
isbn = {9783959772785},
keywords = {Action Codes; Action Contraction; Action Refinement; Automata; Galois Connection; LTS; Model Learning; Model-Based Testing; Models of Reactive Systems},
note = {CRIS-Team Scopus Importer:2023-08-18},
peerreviewed = {unknown},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing},
title = {{Action} {Codes}},
venue = {Paderborn, DEU},
volume = {261},
year = {2023}
}
@article{faucris.227313367,
abstract = {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.},
author = {Wißmann, Thorsten and Pattinson, Dirk and Milius, Stefan},
doi = {10.1016/j.ic.2019.104456},
faupublication = {yes},
journal = {Information and Computation},
keywords = {Algebraic trees; Automata behaviour; Coalgebra; Fixpoints of functors},
note = {CRIS-Team Scopus Importer:2019-10-01},
peerreviewed = {Yes},
title = {{A} new foundation for finitary corecursion and iterative algebras},
year = {2019}
}
@inproceedings{faucris.108442884,
author = {Milius, Stefan and Pattinson, Dirk and Wißmann, Thorsten},
booktitle = {Foundations of Software Science and Computation Structures},
doi = {10.1007/978-3-662-49630-5},
faupublication = {yes},
isbn = {978-3-662-49629-9},
keywords = {coalgebra, rational fixed point, corecursion, locally finite fixed point},
note = {UnivIS-Import:2017-03-24:Pub.2016.tech.IMMD.profes{\_}1.anewfo},
pages = {107-125},
peerreviewed = {unknown},
series = {Lecture Notes in Computer Science},
title = {{A} {New} {Foundation} for {Finitary} {Corecursion}},
url = {http://link.springer.com/book/10.1007/978-3-662-49630-5},
venue = {Eindhoven, The Netherlands},
volume = {9634},
year = {2016}
}
@inproceedings{faucris.311728111,
abstract = {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.},
author = {Rot, Jurriaan and Wißmann, Thorsten},
booktitle = {Leibniz International Proceedings in Informatics, LIPIcs},
date = {2023-06-19/2023-06-21},
doi = {10.4230/LIPIcs.CALCO.2023.12},
editor = {Paolo Baldan, Valeria de Paiva},
faupublication = {yes},
isbn = {9783959772877},
keywords = {Bisimilarity; Coalgebra; ioco; Mealy Machines; Relation Lifting},
note = {CRIS-Team Scopus Importer:2023-10-06},
peerreviewed = {unknown},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing},
title = {{Bisimilar} {States} in {Uncertain} {Structures}},
venue = {Bloomington, IN, USA},
volume = {270},
year = {2023}
}
@inproceedings{faucris.264572293,
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.},
author = {Deifel, Hans-Peter and Milius, Stefan and Wißmann, Thorsten},
booktitle = {Leibniz International Proceedings in Informatics, LIPIcs},
date = {2021-07-17/2021-07-24},
doi = {10.4230/LIPIcs.FSCD.2021.28},
editor = {Naoki Kobayashi},
faupublication = {yes},
isbn = {9783959771917},
keywords = {Coalgebra; Minimization; Partition refinement; Transition systems},
note = {CRIS-Team Scopus Importer:2021-10-01},
peerreviewed = {unknown},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing},
title = {{Coalgebra} encoding for efficient minimization},
venue = {Virtual},
volume = {195},
year = {2021}
}
@inproceedings{faucris.119920504,
abstract = {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.},
address = {Berlin},
author = {Gorin, Daniel and Pattinson, Dirk and Schröder, Lutz and Widmann, Florian and Wißmann, Thorsten},
booktitle = {Automated Reasoning},
date = {2014-07-19/2014-07-22},
doi = {10.1007/978-3-319-08587-6{\_}31},
faupublication = {yes},
isbn = {978-3-319-08587-6},
note = {UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes{\_}1.coolag},
pages = {396-402},
peerreviewed = {Yes},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
title = {{COOL} — {A} {Generic} {Reasoner} for {Coalgebraic} {Hybrid} {Logics} ({System} {Description})},
url = {http://www8.cs.fau.de/{\_}media/research:papers:cool.pdf},
venue = {Wien},
volume = {8562},
year = {2014}
}
@article{faucris.233535580,
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⋅logn)" 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.},
author = {Wißmann, Thorsten and Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz},
faupublication = {yes},
journal = {Logical Methods in Computer Science},
pages = {1–63},
peerreviewed = {Yes},
title = {{Efficient} and {Modular} {Coalgebraic} {Partition} {Refinement}},
volume = {16},
year = {2020}
}
@inproceedings{faucris.106397764,
author = {Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz and Wißmann, Thorsten},
booktitle = {Proc. 28th International Conference on Concurrency Theory (CONCUR 2017)},
editor = {Meyer R, Nestmann U},
faupublication = {yes},
pages = {28:1--28:16},
peerreviewed = {Yes},
publisher = {Schloss Dagstuhl},
title = {{Efficient} {Coalgebraic} {Partition} {Refinement}},
volume = {85},
year = {2017}
}
@inproceedings{faucris.264571269,
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).},
author = {Wißmann, Thorsten 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.32},
editor = {Serge Haddad, Daniele Varacca},
faupublication = {yes},
isbn = {9783959772037},
keywords = {Bisimulation; Coalgebra; Distinguishing formulae; Modal logic; Partition refinement},
note = {CRIS-Team Scopus Importer:2021-10-01},
peerreviewed = {unknown},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing},
title = {{Explaining} {Behavioural} {Inequivalence} {Generically} in {Quasilinear} {Time}},
venue = {Virtual, Online},
volume = {203},
year = {2021}
}
@inproceedings{faucris.122980704,
author = {Milius, Stefan and Wißmann, Thorsten},
booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015},
date = {2015-06-24/2015-06-26},
doi = {10.4230/LIPIcs.CALCO.2015.336},
faupublication = {yes},
isbn = {978-3-939897-84-2},
keywords = {rational trees, infinitary lambda calculus, coinduction},
note = {UnivIS-Import:2016-06-01:Pub.2015.tech.IMMD.profes{\_}1.finita},
pages = {336-351},
peerreviewed = {unknown},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {{Finitary} {Corecursion} for the {Infinitary} {Lambda} {Calculus}},
url = {https://coalg.org/calco15/papers/p21-Wi%C3%9Fmann.pdf},
venue = {Nijmegen (NL)},
volume = {35},
year = {2015}
}
@article{faucris.229927337,
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.},
author = {Adámek, J. and Milius, Stefan and Sousa, L. and Wißmann, Thorsten},
faupublication = {yes},
journal = {Theory and Applications of Categories},
keywords = {Finitary functor; Finitely generated object; Finitely presentable object; Regular monad},
note = {CRIS-Team Scopus Importer:2019-11-29},
pages = {1179-1195},
peerreviewed = {Yes},
title = {{Finitely} presentable algebras for finitary monads},
volume = {34},
year = {2019}
}
@article{faucris.253782820,
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.},
author = {Wißmann, Thorsten and Deifel, Hans-Peter and Milius, Stefan and Schröder, Lutz},
doi = {10.1007/s00165-020-00526-z},
faupublication = {yes},
journal = {Formal Aspects of Computing},
note = {Created from Fastlane, WoS look-up},
peerreviewed = {Yes},
title = {{From} generic partition refinement to weighted tree automata minimization},
year = {2021}
}
@inproceedings{faucris.228665432,
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.},
address = {Cham},
author = {Deifel, Hans-Peter and Milius, Stefan and Schröder, Lutz and Wißmann, Thorsten},
booktitle = {Formal Methods -- The Next 30 Years},
doi = {10.1007/978-3-030-30942-8{\_}18},
editor = {Beek MH, McIver A, Oliveira JN},
faupublication = {yes},
isbn = {978-3-030-30942-8},
pages = {280--297},
peerreviewed = {Yes},
publisher = {Springer International Publishing},
title = {{Generic} {Partition} {Refinement} and {Weighted} {Tree} {Automata}},
year = {2019}
}
@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.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}
}
@article{faucris.228665688,
author = {Adámek, Jiří and Milius, Stefan and Sousa, Lourdes and Wißmann, Thorsten},
faupublication = {yes},
journal = {Theory and Applications of Categories},
pages = {1134--1164},
peerreviewed = {Yes},
title = {{On} {Finitary} {Functors}},
url = {http://www.tac.mta.ca/tac/volumes/34/35/34-35abs.html},
volume = {34},
year = {2019}
}
@inproceedings{faucris.217159761,
abstract = {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.},
author = {Wißmann, Thorsten and Dubut, Jérémy and Katsumata, Shin ya and Hasuo, Ichiro},
booktitle = {22nd International Conference, FOSSACS 2019},
doi = {10.1007/978-3-030-17127-8{\_}30},
editor = {Mikolaj Bojanczyk, Alex Simpson},
faupublication = {yes},
keywords = {Categories; Coalgebra; Nominal sets; Open maps},
note = {CRIS-Team Scopus Importer:2019-05-09},
pages = {523-540},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Path} {Category} for {Free}: {Open} {Morphisms} from {Coalgebras} with {Non}-deterministic {Branching}},
volume = {11425 LNCS},
year = {2019}
}
@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)},
doi = {10.1007/978-3-030-00389-0{\_}5},
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.285684027,
abstract = {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).},
author = {Wißmann, Thorsten and Milius, Stefan and Schröder, Lutz},
doi = {10.46298/LMCS-18(4:6)2022},
faupublication = {yes},
journal = {Logical Methods in Computer Science},
keywords = {bisimulation; coalgebra; distinguishing formulae; modal logic; partition refinement},
note = {CRIS-Team Scopus Importer:2022-11-25},
pages = {6:1-6:48},
peerreviewed = {Yes},
title = {{QUASILINEAR}-{TIME} {COMPUTATION} {OF} {GENERIC} {MODAL} {WITNESSES} {FOR} {BEHAVIOURAL} {INEQUIVALENCE}},
volume = {18},
year = {2022}
}
@inproceedings{faucris.118715564,
abstract = {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.},
address = {Aachen},
author = {Gorin, Daniel and Schröder, Lutz and Wißmann, Thorsten},
booktitle = {Proc. 26th International Workshop on Description Logics, DL 2013},
date = {2013-07-23/2013-07-26},
faupublication = {yes},
note = {UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes{\_}1.reason},
pages = {689-703},
peerreviewed = {Yes},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
title = {{Reasoning} with {Bounded} {Self}-reference {Using} {Logical} {Interpreters}},
venue = {Ulm},
volume = {1014},
year = {2013}
}
@article{faucris.121046244,
author = {Milius, Stefan and Schröder, Lutz and Wißmann, Thorsten},
doi = {10.1007/s10485-016-9457-8},
faupublication = {yes},
journal = {Applied Categorical Structures},
keywords = {Nominal sets; rational fixpoints; regular languages; coalgebra},
pages = {663--701},
peerreviewed = {Yes},
title = {{Regular} {Behaviours} with {Names} - {On} {Rational} {Fixpoints} of {Endofunctors} on {Nominal} {Sets}},
volume = {24},
year = {2016}
}
@inproceedings{faucris.307579288,
abstract = {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.},
author = {Dubut, Jérémy and Wißmann, Thorsten},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
date = {2023-04-22/2023-04-27},
doi = {10.1007/978-3-031-30829-1{\_}15},
editor = {Orna Kupferman, Pawel Sobocinski},
faupublication = {yes},
isbn = {9783031308284},
keywords = {Branching Bisimilarity; Open maps; Probabilistic Bisimilarity; Weak Bisimilarity; Weighted Bisimilarity},
note = {CRIS-Team Scopus Importer:2023-07-14},
pages = {308-327},
peerreviewed = {unknown},
publisher = {Springer Science and Business Media Deutschland GmbH},
title = {{Weighted} and {Branching} {Bisimilarities} from {Generalized} {Open} {Maps}},
venue = {Paris},
volume = {13992 LNCS},
year = {2023}
}