Projects & Tools

• HOA tools: Libraries and tools for the "Hanoi Omega Automata Format".
• ltl2dstar: Tool for translating LTL formulas to deterministic omega-automata.

About

Joachim Klein

Until 2019, I did research as a PhD student and postdoc at TU Dresden on topics such as omega-automata, compositional synthesis as well as probabilistic and non-probabilistic model checking.

Find me on GitHub, DBLP, Google Scholar.
Contact: joachim.klein AT automata.tools

List of Publications

• Christel Baier, Philipp Chrszon, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz
  Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination
  It's All About Coordination. Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab. Lecture Notes in Computer Science 10865, pp 38-56, 2018. Link, additional materials.
• Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, David Müller
  Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata
  International Journal on Software Tools for Technology Transfer, Volume 20(2) (Special issue "TACAS'16"), pp 179-194, 2018. Link, additional materials.
• Lisa Hutschenreiter, Christel Baier, Joachim Klein
  Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination
  Proceedings of the 8th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF'17)
  Electronic Proceedings in Theoretical Computer Science 256, pp. 16-30, Open Publishing Association, 2017. Link, additional materials.
• Steffen Märcker, Christel Baier, Joachim Klein, Sascha Klüppelholz
  Computing Conditional Probabilities: Implementation and Evaluation
  Proceedings of the 15th International Conference on Software Engineering and Formal Methods (SEFM'17)
  Lecture Notes in Computer Science 10469, pp 349-366, 2017. Link, additional materials.
• Christel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich
  Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes
  Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17), Part I
  Lecture Notes in Computer Science 10426, pp 160-180, 2017. Link, additional materials.
• Christel Baier, Joachim Klein, Sascha Klüppelholz, Sascha Wunderlich
  Maximizing the Conditional Expected Reward for Reaching the Goal
  Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Part II
  Lecture Notes in Computer Science 10206, pp 269-285, 2017. Link, additional materials.
• Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, James Worrell
  Markov Chains and Unambiguous Büchi Automata
  Proceedings of the 28th International Conference on Computer Aided Verification (CAV'16),
  Lecture Notes in Computer Science 9779, pp 23-42, 2016. Link, additional materials.
• Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, David Müller
  Advances in Symbolic Probabilistic Model Checking with PRISM
  Proceedings of the 22th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16),
  Lecture Notes in Computer Science 9636, pp 349-366, 2016. Link, additional materials.
• Philipp Chrszon, Clemens Dubslaff, Christel Baier, Joachim Klein, Sascha Klüppelholz
  Modeling Role-Based Systems with Exogenous Coordination
  Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday,
  Lecture Notes in Computer Science 9660, pp 122-139, 2016. Link.
• Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, Jan Strejček
  The Hanoi Omega-Automata Format
  Proceedings of the 27th Conference on Computer Aided Verification, Part I (CAV'15),
  Lecture Notes in Computer Science 9206, pp 479-486, 2015. Link, Tools.
• Joachim Klein, Christel Baier, Sascha Klüppelholz
  Compositional Construction of Most General Controllers
  Acta Informatica, Special Issue: Combining Compositionality and Concurrency: Part 2, Volume 52(4-5), 2015, pp 443-482. Link.
• Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp
  Locks: Picking key methods for a scalable quantitative analysis
  Journal of Computer and System Sciences, Volume 81(1), 2015, pp 258-287. Link.
• Christel Baier, Joachim Klein, Sascha Klüppelholz, Sascha Wunderlich
  Weight Monitoring with Linear Temporal Logic: Complexity and Decidability
  Proceedings of the 23rd Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS'14), pp 11:1-11:10, ACM, 2014. Link, Extended version.
• Christel Baier, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz, Sascha Wunderlich
  Probabilistic Model Checking for Energy-Utility Analysis
  Horizons of the Mind. A Tribute to Prakash Panangaden
  Lecture Notes in Computer Science 8464, pp 96-123, 2014. Link.
• Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz
  Energy-Utility Quantiles
  Proceedings of the 6th NASA Formal Methods Symposium (NFM'14)
  Lecture Notes in Computer Science 8430, pp 285-299, 2014. Link, Extended Version.
• Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, Marcus Daum, Joachim Klein, Steffen Märcker, Sascha Wunderlich
  Probabilistic Model Checking and Non-standard Multi-objective Reasoning
  Proceedings of the 17th International Conference of Fundamental Approaches to Software Engineering (FASE'14)
  Lecture Notes in Computer Science 8411, pp 1-16, 2014. Link.
• Christel Baier, Joachim Klein, Sascha Klüppelholz, Steffen Märcker
  Computing Conditional Probabilities in Markovian Models Efficiently
  Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)
  Lecture Notes in Computer Science 8413, pp 515-530, 2014, (EATCS best paper award). Link, Extended version.
• Christel Baier, Joachim Klein, Sascha Klüppelholz
  Synthesis of Reo Connectors for Strategies and Controllers
  Fundamenta Informaticae, Volume 130, Issue 1, pp 1-20, 2014. Link.
• Joachim Klein, David Müller, Christel Baier, Sascha Klüppelholz
  Are Good-for-Games Automata Good for Probabilistic Model Checking?
  Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA'14)
  Lecture Notes in Computer Science 8370, pp 453-465, 2014. Link, Extended version.
• Joachim Klein
  Compositional Synthesis and Most General Controllers
  PhD thesis, Technische Universität Dresden, 2013. Link.
• Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp
  Waiting for locks: How long does it usually take?
  Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'12),
  Lecture Notes in Computer Science 7437, pp 47-62, 2012. Link, Extended version.
• Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp
  Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code
  Proceedings of the 7th International Workshop on Systems Software Verification (SSV'12),
  EPTCS 102, pp 156-166, 2012. Link.
• Christel Baier, Joachim Klein, Sascha Klüppelholz
  A Compositional Framework for Controller Synthesis
  Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR'11),
  Lecture Notes in Computer Science 6901, pp 512-527, 2011. Link.
• Christel Baier, Joachim Klein, Sascha Klüppelholz
  Synthesis of Reo Connectors for Strategies and Controllers
  International Workshop on Logic, Agents, and Mobility (LAM'11), 2011. Download: PDF file.
• Joachim Klein, Sascha Klüppelholz, Andries Stam, Christel Baier
  Hierarchical Modeling and Formal Verification. An industrial case study using Reo and Vereofy
  Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'11),
  Lecture Notes in Computer Science 6959, pp 228-243, 2011. Link.
• Christel Baier, Joachim Klein, Sascha Klüppelholz
  Modeling and Verification of Components and Connectors
  Formal Methods for Eternal Networked Software Systems (SFM'11),
  Lecture Notes in Computer Science 6659, pp 114-147, 2011. Link.
• Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz, Wolfgang Leister
  Design and Verification of Systems with Exogenous Coordination using Vereofy
  Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'10),
  Lectures Notes in Computer Science 6416, pp 97-111, 2010. Springer Link.
• Immo Grabe, Mohammad Mahdi Jaghoori, Bernhard Aichernig, Christel Baier, Tobias Blechmann, Frank de Boer, Andreas Griesmayer, Einar Broch Johnsen, Joachim Klein, Sascha Klüppelholz, Marcel Kyas, Wolfgang Leister, Rudolf Schlatte, Andries Stam, Martin Steffen, Simon Tschirner, Xuedong Liang, Wang Yi
  Credo Methodology - Extended Version
  Proceedings of the 8th International Symposium on Formal Methods for Component and Objects (FMCO'09),
  Lectures Notes in Computer Science 6286, pp 41-69, 2010. Link.
• Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz
  Formal Verification for Components and Connectors
  Proceedings of the 7th International Symposium on Formal Methods for Component and Objects (FMCO'08),
  Lectures Notes in Computer Science 5751, pp 82-101, 2009. Link.
• Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz
  A Uniform Framework for Modeling and Verifying Components and Connectors
  Proceedings of the 11th International Conference on Coordination Models and Languages (Coordination'09),
  Lectures Notes in Computer Science 5521, pp 247-267, 2009. Link.
• Frank Ciesinski, Christel Baier, Marcus Größer, Joachim Klein
  Reduction techniques for model checking Markov decision processes
  Proceedings of the 5th International Conference on Quantitative Evaluation of SysTems (QEST'08),
  pp 45-54, IEEE Computer Society Press, 2008. Link.
• Joachim Klein, Christel Baier
  On-the-fly Stuttering in the Construction of Deterministic omega-Automata
  Proceedings of the 12th International Conference on Implementation and Application of Automata (CIAA'07),
  Lectures Notes in Computer Science 4783, pp 51-61, 2007. Link.
• Joachim Klein, Christel Baier
  Experiments with deterministic ω-automata for formulas of linear temporal logic
  Theoretical Computer Science 363(2), pp 182-195, 2006. Link.
• Joachim Klein, Christel Baier
  Experiments with Deterministic ω-automata for Formulas of Linear temporal Logic
  Proceedings of the 10th International Conference on Implementation and Application of Automata (CIAA'05),
  Lectures Notes in Computer Science 3845, pp 199-212, 2005. Link.
• Joachim Klein
  Linear Time Logic and Deterministic omega-Automata
  Diploma thesis, January 2005, University of Bonn. Link.