Dr. Daniel Hausmann

About me

I am a postdoctoral researcher at the Chair for Theoretical Computer Science of the Friedrich-Alexander University of Erlangen and Nuremberg. Currently, I am working in the project Coalgebraic Model Checking (CoMoC) supervised by Stefan Milius and Lutz Schröder.

I am interested in e.g.

general fixpoint theory
automata on infinite words
solving two-player games
the algorithmics of temporal logics (e.g. model and satisfiability checking for branching-time and linear-time logics)
coalgebra and coalgebraic logic

My recently completed PhD-thesis Satisfiability Checking for the Coalgebraic µ-Calculus (supervised by Lutz Schröder) gives a detailed discourse on decision procedures for the satisfiability problem of general modal fixpoint logics. In November 2019, this thesis was awarded with the Doctoral Thesis Award Promotionspreis des Freundeskreises der TF im ATE.

In my time as a PhD student, I have given lectures on Modal Logic (2016, 2017), and organized and held tutorials for courses on Complexity of Algorithms (2013), Theory of Programming (2014, 2015, 2016) and Logic for Computer Scientists (2015, 2016, 2017).

We have implemented various satisfiability and model checking algorithms for the coalgebraic µ-calculus within COOL.

Address:	FAU Erlangen-Nürnberg	Room:	11.130
	Chair for Theoretical Computer Science	Telephone:	+49-9131-85-64054
	Martensstraße 3	Fax:	+49-9131-85-64055
	D-91058 Erlangen	E-Mail:	daniel.hausmann(at)fau.de

Publications

NP Reasoning in the Monotone µ-Calculus (Daniel Hausmann, Lutz Schröder), In Proc. 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Lecture Notes in Artificial Intelligence (LNAI), vol. 12166, pp. 482–499, Springer International Publishing, 2020. [extended version on arXiv]
Cheap CTL Compassion in NuSMV (Daniel Hausmann, Tadeusz Litak, Christoph Rauch, Matthias Zinner), In Proc. 21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020, Lecture Notes in Computer Science (LNCS), vol. 11990, pp. 248–269, Springer International Publishing, 2020. [artifact]
Game-Based Local Model Checking for the Coalgebraic µ-Calculus (Daniel Hausmann, Lutz Schröder), In Proc. 30th International Conference on Concurrency Theory, CONCUR 2019, Leibniz International Proceedings in Informatics (LIPIcs), vol. 140, pp. 35:1–35:16, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2019. [pdf]
Optimal Satisfiability Checking for Arithmetic µ-Calculi (Daniel Hausmann, Lutz Schröder), In Proc. 22nd International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2019, Lecture Notes in Computer Science (LNCS), vol. 11425, pp. 277–294, Springer International Publishing, 2019. [extended version on arXiv]
Satisfiability Checking for the Coalgebraic µ-Calculus (Daniel Hausmann), Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), 2018. (PhD Thesis) [pdf]
Permutation Games for the Weakly Aconjunctive µ-Calculus (Daniel Hausmann, Lutz Schröder, Hans-Peter Deifel), In Proc. 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, Lecture Notes in Computer Science (LNCS), vol. 10805–10806, pp. 361–378, Springer International Publishing, 2018. [extended version on arXiv] [artifact]
Global Caching for the Alternation-free µ-Calculus (Daniel Hausmann, Lutz Schröder, Christoph Egger), In Proc. 27th International Conference on Concurrency Theory, CONCUR 2016, Leibniz International Proceedings in Informatics (LIPIcs), vol. 59, pp. 34:1–34:15, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2016. [pdf]
Global Caching for the Flat Coalgebraic µ-Calculus (Daniel Hausmann, Lutz Schröder), In Proc. 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, pp. 121–130, IEEE Comp. Soc., 2015. [preprint]
Optimal Tableaux for Conditional Logics with Cautious Monotonicity (Lutz Schröder, Dirk Pattinson, Daniel Hausmann), In Proc. 6th European Conference on Artificial Intelligence, ECAI 2010, Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 707–712, IOS Press, 2010. [preprint]
Optimizing Conditional Logic Reasoning within CoLoSS (Daniel Hausmann, Lutz Schröder), In Proc. 6th Workshop on Methods for Modalities, M4M-6 2009, Electronic Notes in Theoretical Computer Science (ENTCS), vol. 262, pp. 157–171, Elsevier Science; Amsterdam, 2010. [preprint]
The Importance of Being Formal (Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter), In Proc. Workshop on Certification of Safety-Critical Software Controlled Systems, SafeCert-08, Electronic Notes in Theoretical Computer Science (ENTCS), vol. 238 (4), pp. 57–70, Elsevier Science; Amsterdam, 2009. [pdf]
A Coalgebraic Approach to the Semantics of the Ambient Calculus (Daniel Hausmann, Till Mossakowski, Lutz Schröder), In Theoretical Computer Science, vol. 366, pp. 121–143, Elsevier, 2006. (extends Hausmann et al. 2005) [preprint]
Towards a Coalgebraic Semantics of the Ambient Calculus (Daniel Hausmann, Till Mossakowski, Lutz Schröder), In Proc. 1st International Conference on Algebra and Coalgebra in Computer Science, CALCO 2005, Lecture Notes in Computer Science (LNCS), vol. 3629, pp. 232–246, Springer International Publishing, 2005. [preprint]
Iterative Circular Coinduction for CoCasl in Isabelle/HOL (Daniel Hausmann, Till Mossakowski, Lutz Schröder), In Proc. 8th International Conference on Fundamental Approaches to Software Engineering, FASE 2005, Lecture Notes in Computer Science (LNCS), vol. 3442, pp. 341–356, Springer International Publishing, 2005. [preprint]

Also see my profiles at DBLP, Google Scholar or ResearchGate.

Recent Talks

NP Reasoning in the Monotone µ-Calculus presented at Highlights 2020, (Aachen), September, 2020 (video)
Harnessing LTL With Freeze Quantification at the Chair Seminar, (Erlangen), August 04, 2020
NP Reasoning in the Monotone µ-Calculus presented at IJCAR 2020, (Paris), July 02, 2020 (video)
Cheap CTL Compassion in NuSMV presented at VMCAI 2020, New Orleans, January 20, 2020
Satisfiability Checking for the Coalgebraic µ-Calculus (poster), honouring at Tag der Technischen Fakultät, Erlangen, November 22, 2019
Quasipolynomial Computation of Nested Fixpoints at the Chair Seminar, Erlangen, October 29, 2019
Computing Nested Fixpoints in Quasipolynomial Time at LaBRI Formal Methods Seminar, Bordeaux, October 22, 2019
Game-Based Local Model Checking for the Coalgebraic μ-Calculus presented at CONCUR 2019, Amsterdam, August 30, 2019
Optimal Satisfiability Checking for Arithmetic μ-Calculi presented at FoSSaCS 2019, Prague, April 10, 2019
Optimal Satisfiability Checking for the Coalgebraic μ-Calculus at the Chair Seminar, Erlangen, December 04, 2018
Permutation Games for the Weakly Aconjunctive µ-Calculus presented at Highlights 2018, Berlin, September 19, 2018
Satisfiability Checking for the Coalgebraic µ-Calculus, PhD Defense Talk, University Erlangen, June 28, 2018
Permutation Games for the Weakly Aconjunctive µ-Calculus (poster) presented at TACAS 2018, Thessaloniki, April 19, 2018