Theses

Coalgebraic Semantics and Minimization in Sets and Beyond, PhD Dissertation (Dr.Ing.), PDF (university library entry, slides for the defense)

The Locally Finite Fixpoint and its properties, Master Thesis in Computer Science, 2015, PDF.

The rational fixed point in nominal sets and its application to infinitary lambdacalculus, project thesis during the master studies in computer science, 2014, PDF.

Transforming OWL ontologies with bounded selfreference to plain OWL ontologies, 2013, bachelor thesis in computer science, PDF.
Articles
2020
[17]  From Generic Partition Refinement to Weighted Tree Automata Minimization
( )
In: Formal Aspects of Computing, pp. 1–33 (To appear, available at https://arxiv.org/abs/2004.01250)
[bibtex]
[Preprint PDF]
@article{fmSpecialIssue, author = {Deifel, HansPeter and Milius, Stefan and Schr{\"o}der, Lutz and Wi{\ss}mann, Thorsten}, title = {From Generic Partition Refinement to Weighted Tree Automata Minimization}, year = 2020, month = 11, pages = {133}, journal = {Formal Aspects of Computing}, note = {To appear, available at https://arxiv.org/abs/2004.01250}, preprinturl = {https://arxiv.org/abs/2004.01250}, } 
[16]  Efficient and Modular Coalgebraic Partition Refinement
( )
In: Logical Methods in Computer Science, 16:1, pp. 8:18:63
[bibtex]
[PDF] [DOI: 10.23638/LMCS16(1:8)2020]
@article{concurSpecialIssue, title = {{Efficient and Modular Coalgebraic Partition Refinement}}, author = {Wißmann, Thorsten and Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz}, url = {https://lmcs.episciences.org/6064}, doi = {10.23638/LMCS16(1:8)2020}, journal = {{Logical Methods in Computer Science}}, pages = {8:18:63}, volume = {{16:1}}, year = 2020, month = {January}, } 
2019
[15]  A Coalgebraic View on Reachability
( )
In: Commentationes Mathematicae Universitatis Carolinae, 60:4, pp. 605638
[bibtex]
[Preprint PDF] [DOI: 10.14712/12137243.2019.026]
@article{wmkd20reachability, author = {Thorsten Wißmann and Stefan Milius and Katsumata, Shinya and Jérémy Dubut}, title = {A Coalgebraic View on Reachability}, year = 2019, month = 12, journal = {Commentationes Mathematicae Universitatis Carolinae}, volume = {60:4}, pages = {605638}, preprinturl = {https://arxiv.org/abs/1901.10717}, doi = {10.14712/12137243.2019.026}, } 
[14]  Finitely Presentable Algebras for Finitary Monads
( )
In: Theory and Applications of Categories, 34, pp. 1179–1195
[bibtex]
[PDF]
@article{amsw19b, author = {Ji\v{r}\'i{} Ad\'amek and Stefan Milius and Lurdes Sousa and Thorsten Wi{\ss}mann}, title = {Finitely Presentable Algebras for Finitary Monads}, journal = {Theory and Applications of Categories}, year = 2019, optkey = {}, volume = 34, number = 37, pages = {11791195}, url = {http://www.tac.mta.ca/tac/volumes/34/37/3437abs.html}, month = 11, optmonth = {}, optnote = {}, optannote = {}, } 
[13]  Generic Partition Refinement and Weighted Tree Automata
( )
In: Formal Methods – The Next 30 Years, Proc. 3rd World Congress on Formal Methods (FM 2019), 11800, pp. 280–297 (Best Theory Paper Award at the FM'2019 Symposium)
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.1007/9783030309428_18]
@inproceedings{coparFM19, author = {Deifel, HansPeter and Milius, Stefan and Schr{\"o}der, Lutz and Wi{\ss}mann, Thorsten}, editor = {ter Beek, Maurice H. and McIver, Annabelle and Oliveira, Jos{\'e} N.}, title = {Generic Partition Refinement and Weighted Tree Automata}, booktitle = {Formal Methods  The Next 30 Years, Proc.~3rd World Congress on Formal Methods (FM 2019)}, year = 2019, month = 10, publisher = {Springer International Publishing}, series = {LNCS}, volume = 11800, address = {Cham}, pages = {280297}, 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 noncancellative 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 preimplemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.}, isbn = {9783030309428}, note = {Best Theory Paper Award at the FM'2019 Symposium}, url = {https://link.springer.com/chapter/10.1007/9783030309428_18}, preprinturl = {https://arxiv.org/abs/1811.08850}, doi = {10.1007/9783030309428_18}, } 
[12]  On Finitary Functors
( )
In: Theory and Applications of Categories, 34, pp. 1134–1164
[bibtex]
[PDF]
@article{amsw19, author = {Ji\v{r}\'i{} Ad\'amek and Stefan Milius and Lurdes Sousa and Thorsten Wi{\ss}mann}, title = {On Finitary Functors}, journal = {Theory and Applications of Categories}, year = 2019, optkey = {}, volume = 34, number = 35, pages = {11341164}, url = {http://www.tac.mta.ca/tac/volumes/34/35/3435abs.html}, month = 10, optmonth = {}, optnote = {}, optannote = {}, } 
[11]  A New Foundation for Finitary Corecursion and Iterative Algebras
( )
In: Information and Computation, 271, pp. 1–28 (Article 104456)
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.1016/j.ic.2019.104456]
@article{lffiac, title = {A New Foundation for Finitary Corecursion and Iterative Algebras}, journal = {Information and Computation}, note = {Article 104456}, year = 2019, month = 09, volume = 271, pages = {128}, pagesnote = {page range is according to authors proof}, issn = {08905401}, doi = {10.1016/j.ic.2019.104456}, url = {http://www.sciencedirect.com/science/article/pii/S0890540119300720}, preprinturl = {https://arxiv.org/abs/1802.08070}, author = {Stefan Milius and Dirk Pattinson and Thorsten Wi{\ss}mann}, publisher = {Elsevier}, keywords = {coalgebra, fixpoints of functors, automata behaviour, algebraic trees}, abstract = {This paper contributes to a theory of the behaviour of “finitestate” systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor is finitary and preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius, and Velebil). Moreover, we show that the LFF is characterized by two universal properties: (1) as the final locally finitely generated coalgebra, and (2) as the initial fgiterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal powerseries, regular trees etc. Moreover, we obtain a number of new examples, e.g. (realtime deterministic resp. nondeterministic) contextfree languages, constructively Salgebraic formal powerseries (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.}, } 
[10]  Path Category for Free
( )
In: Proc. 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019), 11425, pp. 523–540
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.1007/9783030171278_30]
@inproceedings{WDKH2019, author = {Wi{\ss}mann, Thorsten and Dubut, J{\'e}r{\'e}my and Katsumata, Shinya and Hasuo, Ichiro}, editor = {Boja{\'{n}}czyk, Miko{\l}aj and Simpson, Alex}, title = {Path Category for Free}, series = {LNCS}, volume = 11425, booktitle = {Proc.~22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019)}, year = 2019, month = 04, publisher = {Springer International Publishing}, address = {Cham}, doi = {10.1007/9783030171278_30}, pages = {523540}, 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 Gcoalgebra 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 pathcategory for pointed Gcoalgebras and lax homomorphisms, such that the open morphisms turn out to be precisely the Gcoalgebra homomorphisms. The above construction provides pathcategories and trace semantics for free for different flavours of transition systems: (1) nondeterministic 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.}, isbn = {9783030171278}, preprinturl = {http://arxiv.org/abs/1811.12294}, url = {https://link.springer.com/chapter/10.1007%2F9783030171278_30}, } 
2018
[9]  A coalgebraic treatment of conditional transition systems with upgrades
( )
In: Logical Methods in Computer Science, 14:1, pp. 19:1–19:32
[bibtex]
[PDF] [DOI: 10.23638/LMCS14(1:19)2018]
@article{lmcsCTS, title = {A coalgebraic treatment of conditional transition systems with upgrades}, author = {Beohar, Harsh and K{\"o}nig, Barbara and K{\"u}pper, Sebastian and Silva, Alexandra and Wi{\ss}mann, Thorsten}, url = {http://lmcs.episciences.org/4330}, doi = {10.23638/LMCS14(1:19)2018}, journal = {Logical Methods in Computer Science}, volume = {14:1}, pages = {19:119:32}, year = 2018, month = {February}, keywords = {Computer Science  Logic in Computer Science}, } 
[8]  Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages
( )
In: Proc. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2018), 11202, pp. 56–77
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.1007/9783030003890_5]
@inproceedings{DorschEA2018, doi = {10.1007/9783030003890_5}, url = {https://doi.org/10.1007/9783030003890_5}, year = 2018, publisher = {Springer}, pages = {5677}, author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"{o}der and Thorsten Wi{\ss}mann}, title = {Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages}, booktitle = {Proc.~14th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2018)}, series = {LNCS}, volume = 11202, preprinturl = {https://arxiv.org/abs/1805.07211}, } 
2017
[7]  Efficient Coalgebraic Partition Refinement
( )
In: Proc. 28th International Conference on Concurrency Theory (CONCUR 2017), 85, pp. 32:1–32:16
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.4230/LIPIcs.CONCUR.2017.32]
@inproceedings{DorschEA17, author = {Ulrich Dorsch and Stefan Milius and Lutz Schr{\"o}der and Thorsten Wi{\ss}mann}, title = {Efficient Coalgebraic Partition Refinement}, booktitle = {Proc.~28th International Conference on Concurrency Theory (CONCUR 2017)}, series = {LIPIcs}, volume = 85, pages = {32:132:16}, publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik}, year = 2017, month = 09, preprinturl = {https://arxiv.org/abs/1705.08362}, url = {https://drops.dagstuhl.de/opus/volltexte/2017/7793/}, doi = {10.4230/LIPIcs.CONCUR.2017.32}, } 
[6]  Nominal Automata with Name Binding
( )
In: Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), 10203, pp. 124–142
[bibtex]
[Preprint PDF] [DOI: 10.1007/9783662544587_8]
@inproceedings{skmw17, author = {Lutz Schr\"oder and Dexter Kozen and Stefan Milius and Thorsten Wi\ss{}mann}, title = {Nominal Automata with Name Binding}, optcrossref = {}, optkey = {}, booktitle = {Proc.~20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)}, year = 2017, editor = {Javier Esparza and Andrzej Murawski}, volume = 10203, optnumber = {}, series = {LNCS}, pages = {124142}, month = 04, optmonth = {}, optaddress = {}, optorganization = {}, publisher = {Springer}, preprinturl = {http://arxiv.org/abs/1603.01455}, comment = {The final publication is available at Springer via <a href="http://dx.doi.org/10.1007/9783662544587_8">http://dx.doi.org/10.1007/9783662544587_8</a>.}, optannote = {}, doi = {10.1007/9783662544587_8}, } 
2016
[5]  Regular Behaviours with Names
( )
In: Applied Categorical Structures, 24, pp. 663–701
[bibtex]
[Preprint PDF] [DOI: 10.1007/s1048501694578]
@article{msw16, author = {Milius, Stefan and Schr{\"{o}}der, Lutz and Wi{\ss}mann, Thorsten}, title = {Regular Behaviours with Names}, journal = {Applied Categorical Structures}, publisher = {Springer}, year = 2016, month = 08, volume = 24, number = 5, pages = {663701}, issn = {15729095}, doi = {10.1007/s1048501694578}, preprinturl = {https://arxiv.org/abs/1607.07828}, } 
[4]  A New Foundation for Finitary Corecursion  The Locally Finite Fixpoint and Its Properties
( )
In: Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016), 9634, pp. 107–125
[bibtex]
[Preprint PDF] [DOI: 10.1007/9783662496305_7]
@inproceedings{mpw16, author = {Stefan Milius and Dirk Pattinson and Thorsten Wi{\ss}mann}, title = {A New Foundation for Finitary Corecursion  The Locally Finite Fixpoint and Its Properties}, booktitle = {Proc.~19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016)}, booktitlefull = {Foundations of Software Science and Computation Structures  19th International Conference, {FOSSACS} 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands, April 28, 2016, Proceedings}, series = {LNCS}, volume = 9634, pages = {107125}, year = 2016, month = 04, xcrossref = {DBLP:conf/fossacs/2016}, preprinturl = {http://arxiv.org/abs/1601.01532}, doi = {10.1007/9783662496305_7}, } 
2015
[3]  Finitary Corecursion for the Infinitary Lambda Calculus
( )
In: Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), 35, pp. 336–351
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.4230/LIPIcs.CALCO.2015.336]
@inproceedings{MiliusWissmannRatlambda, title = {Finitary Corecursion for the Infinitary Lambda Calculus}, author = {Stefan Milius and Thorsten Wi{\ss}mann}, booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)}, series = {Leibniz International Proceedings in Informatics}, year = 2015, pages = {336351}, volume = 35, url = {http://coalg.org/calco15/papers/p21Wi%C3%9Fmann.pdf}, doi = {10.4230/LIPIcs.CALCO.2015.336}, preprinturl = {https://arxiv.org/abs/1505.07736}, } 
2014
[2]  COOL – A Generic Reasoner for Coalgebraic Hybrid Logics (System Description)
( )
In: Proc. 7th International Joint Conference on Automated Reasoning (IJCAR 2014), 8562, pp. 396–402
[bibtex]
[PDF] [Preprint PDF] [DOI: 10.1007/9783319085876_31]
@inproceedings{GorinEA14, author = {Daniel Gor{\'{i}}n and Dirk Pattinson and Lutz Schr{\"{o}}der and Florian Widmann and Thorsten Wi{\ss}mann}, title = {{COOL}  A Generic Reasoner for Coalgebraic Hybrid Logics (System Description)}, booktitle = {Proc.~7th International Joint Conference on Automated Reasoning (IJCAR 2014)}, year = 2014, editor = {St{\'{e}}phane Demri and Deepak Kapur and Christoph Weidenbach}, series = {LNCS}, publisher = {Springer}, pages = {396402}, volume = 8562, doi = {10.1007/9783319085876_31}, preprinturl = {https://www8.cs.fau.de/ext/thorsten/coolijcar2014.pdf}, url = {https://link.springer.com/chapter/10.1007/9783319085876_31}, } 
2013
[1]  Reasoning with Bounded Selfreference Using Logical Interpreters
( )
In: Proc. 26th International Workshop on Description Logics (DL 2013), 1014, pp. 689703
[bibtex]
[PDF]
@inproceedings{GorinEA13, author = {Daniel Gor{\'{i}}n and Lutz Schr{\"{o}}der and Thorsten Wi{\ss}mann}, title = {Reasoning with Bounded Selfreference Using Logical Interpreters}, pages = {689703}, editor = {Thomas Eiter and Birte Glimm and Yevgeny Kazakov and Markus Kr{\"{o}}tzsch}, booktitle = {Proc.~26th International Workshop on Description Logics (DL 2013)}, publisher = {CEURWS.org}, series = {CEUR Workshop Proceedings}, volume = 1014, year = 2013, url = {http://ceurws.org/Vol1014/paper_75.pdf}, bibsource = {DBLP, http://dblp.unitrier.de}, } 
generated by publistgen.py