Experiments with Deterministic omega-Automata for Formulas of Linear Temporal Logic. - Joachim Klein 001; Christel Baier (CIAA, 2005)

Experiments with deterministic omega-automata for formulas of linear temporal logic. - Joachim Klein 001; Christel Baier (Theor. Comput. Sci., 2006)

On-the-Fly Stuttering in the Construction of Deterministic omega -Automata. - Joachim Klein 001; Christel Baier (CIAA, 2007)

Formal Verification for Components and Connectors. - Christel Baier; Tobias Blechmann 001; Joachim Klein 001; Sascha Klüppelholz (FMCO, 2008)

Reduction Techniques for Model Checking Markov Decision Processes. - Frank Ciesinski; Christel Baier; Marcus Größer; Joachim Klein 001 (QEST, 2008)

A Uniform Framework for Modeling and Verifying Components and Connectors. - Christel Baier; Tobias Blechmann 001; Joachim Klein 001; Sascha Klüppelholz (COORDINATION, 2009)

The Credo Methodology - (Extended Version). - Immo Grabe; Mohammad Mahdi Jaghoori; Joachim Klein 001; Sascha Klüppelholz; Andries Stam; Christel Baier; Tobias Blechmann 001; Bernhard K. Aichernig; Frank S. de Boer; Andreas Griesmayer (FMCO, 2009)

Credo Methodology: Modeling and Analyzing A Peer-to-Peer System in Credo. - Immo Grabe; Mohammad Mahdi Jaghoori; Bernhard K. Aichernig; Christel Baier; Tobias Blechmann 001; Frank S. de Boer; Andreas Griesmayer; Einar Broch Johnsen; Joachim Klein 001; Sascha Klüppelholz; Marcel Kyas; Wolfgang Leister; et al. (TTSS, 2009)

Design and Verification of Systems with Exogenous Coordination Using Vereofy. - Christel Baier; Tobias Blechmann 001; Joachim Klein 001; Sascha Klüppelholz; Wolfgang Leister (ISoLA (2), 2010)

A Compositional Framework for Controller Synthesis. - Christel Baier; Joachim Klein 001; Sascha Klüppelholz (CONCUR, 2011)

Hierarchical Modeling and Formal Verification. An Industrial Case Study Using Reo and Vereofy. - Joachim Klein 001; Sascha Klüppelholz; Andries Stam; Christel Baier (FMICS, 2011)

Modeling and Verification of Components and Connectors. - Christel Baier; Joachim Klein 001; Sascha Klüppelholz (SFM, 2011)

Waiting for Locks: How Long Does It Usually Take? - Christel Baier; Marcus Daum; Benjamin Engel; Hermann Härtig; Joachim Klein 001; Sascha Klüppelholz; Steffen Märcker; Hendrik Tews; Marcus Völp (FMICS, 2012)

Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code - Christel Baier; Marcus Daum; Benjamin Engel; Hermann Härtig; Joachim Klein 001; Sascha Klüppelholz; Steffen Märcker; Hendrik Tews; Marcus Völp (SSV, 2012)

Compositional synthesis and most general controllers. - Joachim Klein 001 (2013)

Probabilistic Model Checking for Energy-Utility Analysis. - Christel Baier; Clemens Dubslaff; Joachim Klein 001; Sascha Klüppelholz; Sascha Wunderlich (Horizons of the Mind, 2014)

Weight monitoring with linear temporal logic: complexity and decidability. - Christel Baier; Joachim Klein 001; Sascha Klüppelholz; Sascha Wunderlich (CSL-LICS, 2014)

Probabilistic Model Checking and Non-standard Multi-objective Reasoning. - Christel Baier; Clemens Dubslaff; Sascha Klüppelholz; Marcus Daum; Joachim Klein 001; Steffen Märcker; Sascha Wunderlich (FASE, 2014)

Are Good-for-Games Automata Good for Probabilistic Model Checking? - Joachim Klein 001; David Müller 001; Christel Baier; Sascha Klüppelholz (LATA, 2014)

Energy-Utility Quantiles. - Christel Baier; Marcus Daum; Clemens Dubslaff; Joachim Klein 001; Sascha Klüppelholz (NASA Formal Methods, 2014)

Computing Conditional Probabilities in Markovian Models Efficiently. - Christel Baier; Joachim Klein 001; Sascha Klüppelholz; Steffen Märcker (TACAS, 2014)

Synthesis of Reo Connectors for Strategies and Controllers. - Christel Baier; Joachim Klein 001; Sascha Klüppelholz (Fundam. Informaticae, 2014)

The Hanoi Omega-Automata Format. - Tomás Babiak; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; Jan Kretínský; David Müller 001; David Parker 001; Jan Strejcek (CAV (1), 2015)

Compositional construction of most general controllers. - Joachim Klein 001; Christel Baier; Sascha Klüppelholz (Acta Informatica, 2015)

Locks: Picking key methods for a scalable quantitative analysis. - Christel Baier; Marcus Daum; Benjamin Engel; Hermann Härtig; Joachim Klein 001; Sascha Klüppelholz; Steffen Märcker; Hendrik Tews; Marcus Völp (J. Comput. Syst. Sci., 2015)

Modeling Role-Based Systems with Exogenous Coordination. - Philipp Chrszon; Clemens Dubslaff; Christel Baier; Joachim Klein 001; Sascha Klüppelholz (Theory and Practice of Formal Methods, 2016)

Markov Chains and Unambiguous Büchi Automata. - Christel Baier; Stefan Kiefer; Joachim Klein 001; Sascha Klüppelholz; David Müller 001; James Worrell 001 (CAV (1), 2016)

Advances in Symbolic Probabilistic Model Checking with PRISM. - Joachim Klein 001; Christel Baier; Philipp Chrszon; Marcus Daum; Clemens Dubslaff; Sascha Klüppelholz; Steffen Märcker; David Müller 001 (TACAS, 2016)

Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. - Christel Baier; Joachim Klein 001; Linda Leuschner; David Parker 001; Sascha Wunderlich (CAV (1), 2017)

Computing Conditional Probabilities: Implementation and Evaluation. - Steffen Märcker; Christel Baier; Joachim Klein 001; Sascha Klüppelholz (SEFM, 2017)

Maximizing the Conditional Expected Reward for Reaching the Goal. - Christel Baier; Joachim Klein 001; Sascha Klüppelholz; Sascha Wunderlich (TACAS (2), 2017)

Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination. - Lisa Hutschenreiter; Christel Baier; Joachim Klein 001 (GandALF, 2017)

Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination. - Christel Baier; Philipp Chrszon; Clemens Dubslaff; Joachim Klein 001; Sascha Klüppelholz (It's All About Coordination, 2018)

Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. - Joachim Klein 001; Christel Baier; Philipp Chrszon; Marcus Daum; Clemens Dubslaff; Sascha Klüppelholz; Steffen Märcker; David Müller 001 (Int. J. Softw. Tools Technol. Transf., 2018)

Generic Emptiness Check for Fun and Profit. - Christel Baier; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; David Müller 001; Jan Strejcek (ATVA, 2019)

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). - Ernst Moritz Hahn; Arnd Hartmanns; Christian Hensel; Michaela Klauck; Joachim Klein 001; Jan Kretínský; David Parker 001; Tim Quatmann; Enno Ruijters; Marcel Steinmetz (TACAS (3), 2019)

Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. - Christel Baier; Christian Hensel; Lisa Hutschenreiter; Sebastian Junges; Joost-Pieter Katoen; Joachim Klein 001 (Inf. Comput., 2020)

From LTL to unambiguous Büchi automata via disambiguation of alternating automata. - Simon Jantsch; David Müller 001; Christel Baier; Joachim Klein 001 (Formal Methods Syst. Des., 2021)

Markov chains and unambiguous automata. - Christel Baier; Stefan Kiefer; Joachim Klein 001; David Müller 001; James Worrell 001 (J. Comput. Syst. Sci., 2023)