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 lambda-calculus, project thesis during the master studies in computer science, 2014, PDF.

  • Transforming OWL ontologies with bounded self-reference to plain OWL ontologies, 2013, bachelor thesis in computer science, PDF.

Articles

2020

[17] From Generic Partition Refinement to Weighted Tree Automata Minimization (Hans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Accepted for publication in the Special Issue of Formal Aspects of Computing on Formal Methods (Available at https://arxiv.org/abs/2004.01250) [bibtex] [Preprint PDF]
@article{fmSpecialIssue,
  author       = {Deifel, Hans-Peter 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,
  journal      = {Accepted for publication in the Special Issue of Formal Aspects of Computing on Formal Methods},
  note         = {Available at https://arxiv.org/abs/2004.01250},
  preprinturl  = {https://arxiv.org/abs/2004.01250},
}
[16] Efficient and Modular Coalgebraic Partition Refinement (Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, Lutz Schröder) In: Logical Methods in Computer Science, Volume 16, Issue 1 [bibtex] [PDF] [DOI: 10.23638/LMCS-16(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/LMCS-16(1:8)2020},
  journal      = {{Logical Methods in Computer Science}},
  volume       = {{Volume 16, Issue 1}},
  year         = 2020,
  month        = {January},
}

2019

[15] A Coalgebraic View on Reachability (Thorsten Wißmann, Stefan Milius, Shin-ya Katsumata, Jérémy Dubut) In: Commentationes Mathematicae Universitatis Carolinae, 60, 4, pp. 605-638 [bibtex] [Preprint PDF] [DOI: 10.14712/1213-7243.2019.026]
@article{wmkd20reachability,
  author       = {Thorsten Wißmann and Stefan Milius and Katsumata, Shin-ya and Jérémy Dubut},
  title        = {A Coalgebraic View on Reachability},
  year         = 2019,
  month        = 12,
  journal      = {Commentationes Mathematicae Universitatis Carolinae},
  volume       = {60, 4},
  pages        = {605-638},
  preprinturl  = {https://arxiv.org/abs/1901.10717},
  doi          = {10.14712/1213-7243.2019.026},
}
[14] Finitely Presentable Algebras For Finitary Monads (Jiří Adámek, Stefan Milius, Lurdes Sousa, Thorsten Wißmann) 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        = {1179--1195},
  url          = {http://www.tac.mta.ca/tac/volumes/34/37/34-37abs.html},
  month        = 11,
  optmonth     = {},
  optnote      = {},
  optannote    = {},
}
[13] Generic Partition Refinement and Weighted Tree Automata (Hans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Formal Methods – The Next 30 Years, pp. 280–297 (Best Theory Paper Award at the FM 2019 Symposium) [bibtex] [PDF] [Preprint PDF] [DOI: 10.1007/978-3-030-30942-8_18]
@inproceedings{coparFM19,
  author       = {Deifel, Hans-Peter 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},
  year         = 2019,
  month        = 10,
  publisher    = {Springer International Publishing},
  address      = {Cham},
  pages        = {280--297},
  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.},
  isbn         = {978-3-030-30942-8},
  note         = {Best Theory Paper Award at the FM 2019 Symposium},
  url          = {https://link.springer.com/chapter/10.1007/978-3-030-30942-8_18},
  preprinturl  = {https://arxiv.org/abs/1811.08850},
  doi          = {10.1007/978-3-030-30942-8_18},
}
[12] On Finitary Functors (Jiří Adámek, Stefan Milius, Lurdes Sousa, Thorsten Wißmann) 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        = {1134--1164},
  url          = {http://www.tac.mta.ca/tac/volumes/34/35/34-35abs.html},
  month        = 10,
  optmonth     = {},
  optnote      = {},
  optannote    = {},
}
[11] A New Foundation for Finitary Corecursion and Iterative Algebras (Stefan Milius, Dirk Pattinson, Thorsten Wißmann) In: Information and Computation, pp. 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},
  pages        = 104456,
  year         = 2019,
  month        = 09,
  issn         = {0890-5401},
  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},
  keywords     = {coalgebra, fixpoints of functors, automata behaviour, algebraic trees},
  abstract     = {This paper contributes to a theory of the behaviour of “finite-state” 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 fg-iterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal power-series, regular trees etc. Moreover, we obtain a number of new examples, 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.},
}
[10] Path Category for Free (Thorsten Wißmann, Jérémy Dubut, Shin-ya Katsumata, Ichiro Hasuo) In: Foundations of Software Science and Computation Structures (FoSSaCS 2019), pp. 523–540 [bibtex] [PDF] [Preprint PDF] [DOI: 10.1007/978-3-030-17127-8_30]
@inproceedings{WDKH2019,
  author       = {Wi{\ss}mann, Thorsten and Dubut, J{\'e}r{\'e}my and Katsumata, Shin-ya and Hasuo, Ichiro},
  editor       = {Boja{\'{n}}czyk, Miko{\l}aj and Simpson, Alex},
  title        = {Path Category for Free},
  booktitle    = {Foundations of Software Science and Computation Structures (FoSSaCS 2019)},
  year         = 2019,
  month        = 04,
  publisher    = {Springer International Publishing},
  address      = {Cham},
  doi          = {10.1007/978-3-030-17127-8_30},
  pages        = {523--540},
  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.},
  isbn         = {978-3-030-17127-8},
  preprinturl  = {http://arxiv.org/abs/1811.12294},
  url          = {https://link.springer.com/chapter/10.1007%2F978-3-030-17127-8_30},
}

2018

[9] A coalgebraic treatment of conditional transition systems with upgrades (Harsh Beohar, Barbara König, Sebastian Küpper, Alexandra Silva, Thorsten Wißmann) In: Logical Methods in Computer Science, Volume 14, Issue 1 [bibtex] [PDF] [DOI: 10.23638/LMCS-14(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/LMCS-14(1:19)2018},
  journal      = {Logical Methods in Computer Science},
  volume       = {Volume 14, Issue 1},
  year         = 2018,
  month        = {February},
  keywords     = {Computer Science - Logic in Computer Science},
}
[8] Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages (Ulrich Dorsch, Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Coalgebraic Methods in Computer Science, pp. 56–77 [bibtex] [PDF] [Preprint PDF] [DOI: 10.1007/978-3-030-00389-0_5]
@incollection{DorschEA2018,
  doi          = {10.1007/978-3-030-00389-0_5},
  url          = {https://doi.org/10.1007/978-3-030-00389-0_5},
  year         = 2018,
  publisher    = {Springer International Publishing},
  pages        = {56--77},
  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    = {Coalgebraic Methods in Computer Science},
  preprinturl  = {https://arxiv.org/abs/1805.07211},
}

2017

[7] Nominal Automata with Name binding (Lutz Schröder, Dexter Kozen, Stefan Milius, Thorsten Wißmann) 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/978-3-662-54458-7_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       = {Lecture Notes Comput.~Sci. (ARCoSS)},
  pages        = {124--142},
  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/978-3-662-54458-7_8">http://dx.doi.org/10.1007/978-3-662-54458-7_8</a>.},
  optannote    = {},
  doi          = {10.1007/978-3-662-54458-7_8},
}
[6] Efficient Coalgebraic Partition Refinement (Ulrich Dorsch, Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Proc. 28th International Conference on Concurrency Theory (CONCUR 2017) [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},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year         = 2017,
  preprinturl  = {https://arxiv.org/abs/1705.08362},
  url          = {https://drops.dagstuhl.de/opus/volltexte/2017/7793/},
  doi          = {10.4230/LIPIcs.CONCUR.2017.32},
}

2016

[5] Regular Behaviours with Names (Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Applied Categorical Structures, 24, pp. 663–701 [bibtex] [Preprint PDF] [DOI: 10.1007/s10485-016-9457-8]
@article{msw16,
  author       = {Milius, Stefan and Schr{\"{o}}der, Lutz and Wi{\ss}mann, Thorsten},
  title        = {Regular Behaviours with Names},
  journal      = {Applied Categorical Structures},
  year         = 2016,
  month        = 08,
  volume       = 24,
  number       = 5,
  pages        = {663--701},
  issn         = {1572-9095},
  doi          = {10.1007/s10485-016-9457-8},
  preprinturl  = {https://arxiv.org/abs/1607.07828},
}
[4] A New Foundation for Finitary Corecursion - The Locally Finite Fixpoint and Its Properties (Stefan Milius, Dirk Pattinson, Thorsten Wißmann) In: Foundations of Software Science and Computation Structures, FOSSACS 2016, pp. 107–125 [bibtex] [Preprint PDF] [DOI: 10.1007/978-3-662-49630-5_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    = {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 2-8, 2016, Proceedings},
  pages        = {107--125},
  year         = 2016,
  month        = 04,
  xcrossref    = {DBLP:conf/fossacs/2016},
  preprinturl  = {http://arxiv.org/abs/1601.01532},
  doi          = {10.1007/978-3-662-49630-5_7},
}

2015

[3] Finitary Corecursion for the Infinitary Lambda Calculus (Stefan Milius, Thorsten Wißmann) In: Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 [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,
  url          = {http://coalg.org/calco15/papers/p21-Wi%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) (Daniel Gorín, Dirk Pattinson, Lutz Schröder, Florian Widmann, Thorsten Wißmann) In: Proc. 7th Internat. Joint Conf. on Automated Reasoning, IJCAR 2014, 8562, pp. 396–402 [bibtex] [PDF] [Preprint PDF] [DOI: 10.1007/978-3-319-08587-6_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 Internat.\ Joint Conf.\ on Automated Reasoning, IJCAR 2014},
  year         = 2014,
  editor       = {St{\'{e}}phane Demri and Deepak Kapur and Christoph Weidenbach},
  series       = {LNCS},
  publisher    = {Springer},
  pages        = {396--402},
  volume       = 8562,
  doi          = {10.1007/978-3-319-08587-6_31},
  preprinturl  = {http://www8.cs.fau.de/_media/research:papers:cool.pdf},
  url          = {https://link.springer.com/chapter/10.1007/978-3-319-08587-6_31},
}

2013

[1] Reasoning with Bounded Self-reference Using Logical Interpreters (Daniel Gorín, Lutz Schröder, Thorsten Wißmann) In: 26th International Workshop on Description Logics, DL 2013, 1014, pp. 689-703 [bibtex] [PDF]
@inproceedings{GorinEA13,
  author       = {Daniel Gor{\'{i}}n and Lutz Schr{\"{o}}der and Thorsten Wi{\ss}mann},
  title        = {Reasoning with Bounded Self-reference Using Logical Interpreters},
  pages        = {689-703},
  editor       = {Thomas Eiter and Birte Glimm and Yevgeny Kazakov and Markus Kr{\"{o}}tzsch},
  booktitle    = {26th International Workshop on Description Logics, DL 2013},
  publisher    = {CEUR-WS.org},
  series       = {CEUR Workshop Proceedings},
  volume       = 1014,
  year         = 2013,
  url          = {http://ceur-ws.org/Vol-1014/paper_75.pdf},
  bibsource    = {DBLP, http://dblp.uni-trier.de},
}