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
If you are interested in one of the publications and can't access it online, just drop me an email.
-
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.