Holger Hermanns - Publications#

• Reza Pulungan, Holger Hermanns: A construction and minimization service for continuous probability distributions. International Journal on Software Tools for Technology Transfer 17(1): 77-90 (2015)

• FH-POPL15.pdf Luis María Ferrer Fioriti, Holger Hermanns: Probabilistic Termination: Soundness, Completeness, and Compositionality. POPL 2015: 489-501

• Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns: Abstraction-Based Computation of Reward Measures for Markov Automata. VMCAI 2015: 172-189

• Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer: Analysis of Timed and Long-Run Objectives for Markov Automata. Logical Methods in Computer Science 10(3) (2014)

• Andrea Turrini, Holger Hermanns: Cost Preserving Bisimulations for Probabilistic Automata. Logical Methods in Computer Science 10(4) (2014)

• Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns: Reachability and Reward Checking for Stochastic Timed Automata. ECEASST 70 (2014)

• Ali Jafari, Ehsan Khamespanah, Marjan Sirjani, Holger Hermanns: Performance Analysis of Distributed and Asynchronous Systems using Probabilistic Timed Actors. ECEASST 70 (2014)

• Holger Hermanns, Jan Krcál, Jan Kretínský: Probabilistic Bisimulation: Naturally on Distributions. CONCUR 2014: 249-265

• Alexander Graf-Brill, Holger Hermanns, Hubert Garavel: A Model-Based Certification Framework for the EnergyBus Standard. FORTE 2014: 84-99

• Florian Arnold, Holger Hermanns, Reza Pulungan, Mariëlle Stoelinga: Time-Dependent Analysis of Attacks. POST 2014: 285-305

• Arnd Hartmanns, Holger Hermanns: The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. TACAS 2014: 593-598

• Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns: MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata. QAPL 2014: 48-63

• Vahid Hashemi, Holger Hermanns, Andrea Turrini: On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation. ECEASST 66 (2013)

• Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, Joost-Pieter Katoen: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design 43(2): 191-232 (2013)

• Holger Hermanns, Arnd Hartmanns: An Internet Inspired Approach to Power Grid Stability. it - Information Technology 55(2): 45-51 (2013)

• Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, Lijun Zhang: A Semantics for Every GSPN. Petri Nets 2013: 90-109

• Holger Hermanns, Andrea Turrini: Cost Preserving Bisimulations for Probabilistic Automata. CONCUR 2013: 349-363

• Holger Hermanns, Jan Krcál, Jan Kretínský: Compositional Verification and Optimization of Interactive Markov Chains. CONCUR 2013: 364-379

• Hassan Hatefi, Holger Hermanns: Improving Time Bounded Reachability Computations in Interactive Markov Chains. FSEN 2013: 250-266

• Ernst Moritz Hahn, Holger Hermanns: Rewarding probabilistic hybrid automata. HSCC 2013: 313-322

• Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer: Modelling, Reduction and Analysis of Markov Automata. QEST 2013: 55-71

• Christian Eisentraut, Holger Hermanns, Julia Krämer, Andrea Turrini, Lijun Zhang: Deciding Bisimilarities on Distributions. QEST 2013: 72-88

• Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang: The Quest for Minimal Quotients for Probabilistic Automata. TACAS 2013: 16-31

• Hassan Hatefi, Holger Hermanns: Model Checking Algorithms for Markov Automata. ECEASST 53 (2012)

• Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn: Safety Verification for Probabilistic Hybrid Systems. Eur. J. Control 18(6): 572-587 (2012)

• Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns, Björn Wachter: Variable Probabilistic Abstraction Refinement. ATVA 2012: 300-316

• Marius Bozga, Alexandre David, Arnd Hartmanns, Holger Hermanns, Kim G. Larsen, Axel Legay, Jan Tretmans: State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. DATE 2012: 370-375

• Holger Hermanns, Andrea Turrini: Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time. FSTTCS 2012: 435-447

• Tomás Brázdil, Holger Hermanns, Jan Krcál, Jan Kretínský, Vojtech Rehák: Verification of Open Interactive Markov Chains. FSTTCS 2012: 474-485

• Arnd Hartmanns, Holger Hermanns: Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids. ISoLA (1) 2012: 420-439

• Luis María Ferrer Fioriti, Holger Hermanns: Heuristics for Probabilistic Timed Automata with Abstraction Refinement. MMB/DFT 2012: 151-165

• Jonathan Bogdoll, Arnd Hartmanns, Holger Hermanns: Simulation and Statistical Model Checking for Modestly Nondeterministic Models. MMB/DFT 2012: 249-252

• Jonathan Bogdoll, Alexandre David, Arnd Hartmanns, Holger Hermanns: mctau: Bridging the Gap between Modest and UPPAAL. SPIN 2012: 227-233

• Holger Hermanns: Quantitative Models for a Not So Dumb Grid. TACAS 2012: 1

• Arnd Hartmanns, Holger Hermanns, Pascal Berrang: A comparative analysis of decentralized power grid stabilization strategies. Winter Simulation Conference 2012: 158

• Holger Hermanns, Andrea Turrini: Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time. CoRR abs/1205.0376 (2012)

• Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns: Automata-Based CSL Model Checking. Logical Methods in Computer Science 8(2) (2011)

• Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, Lijun Zhang: Probabilistic Logical Characterization. Inf. Comput. 209(2): 154-172 (2011)

• Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2): 90-104 (2011)

• Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang: Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer 13(1): 3-19 (2011)

• Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver E. Theel, Ralf Wimmer, Bettina Braitling, Bernd Becker: Bounded Fairness for Probabilistic Distributed Algorithms. ACSD 2011: 89-97

• Peter Buchholz, Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang: Model Checking Algorithms for CTMDPs. CAV 2011: 225-242

• Jonathan Bogdoll, Luis María Ferrer Fioriti, Arnd Hartmanns, Holger Hermanns: Partial Order Methods for Statistical Model Checking and Simulation. FMOODS/FORTE 2011: 59-74

• Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, Lijun Zhang: Measurability and safety verification for stochastic hybrid systems. HSCC 2011: 43-52

• Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns: Automata-Based CSL Model Checking. ICALP (2) 2011: 271-282

• Ralf Wimmer, Ernst Moritz Hahn, Holger Hermanns, Bernd Becker: Reachability analysis for incomplete networks of Markov decision processes. MEMOCODE 2011: 151-160

• Holger Hermanns: Formal Methods in Energy Informatics. SEFM 2011: 1-2

• Hernan Baro Graf, Holger Hermanns, Juhi Kulshrestha, Jens Peter, Anjo Vahldiek, Aravind Vasudevan: A verified wireless safety critical hard real-time design. WOWMOM 2011: 1-9

• Holger Hermanns, Lijun Zhang: From Concurrency Models to Numbers - Performance and Dependability. Software and Systems Safety - Specification and Verification 2011: 182-210

• Hans-Juergen Boehm, Ursula Goltz, Holger Hermanns, Peter Sewell: Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011). Dagstuhl Reports 1(1): 1-26 (2011)

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Performance evaluation and model checking join forces. Commun. ACM 53(9): 76-85 (2010)

• Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Performability assessment by model checking of Markov reward models. Formal Methods in System Design 36(1): 1-36 (2010)

• Ralf Wimmer, Salem Derisavi, Holger Hermanns: Symbolic partition refinement with automatic balancing of time and space. Perform. Eval. 67(9): 816-836 (2010)

• Angelika Mader, Henrik C. Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink, Holger Hermanns: Synthesis and stochastic assessment of cost-optimal schedules. International Journal on Software Tools for Technology Transfer 12(5): 305-318 (2010)

• Pepijn Crouzen, Holger Hermanns: Aggregation Ordering for Massively Compositional Models. ACSD 2010: 171-180

• Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn: Safety Verification for Probabilistic Hybrid Systems. CAV 2010: 196-211

• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang: PARAM: A Model Checker for Parametric Markov Models. CAV 2010: 660-664

• Christian Eisentraut, Holger Hermanns, Lijun Zhang: Concurrency and Composition in a Stochastic World. CONCUR 2010: 21-39

• Holger Hermanns, Kim Guldstrand Larsen, Jean-François Raskin, Jan Tretmans: Quantitative system validation in model driven design. EMSOFT 2010: 301-302

• Nicolas Coste, Hubert Garavel, Holger Hermanns, Frédéric Lang, Radu Mateescu, Wendelin Serwe: Ten Years of Performance Evaluation for Concurrent Systems Using CADP. ISoLA (2) 2010: 128-142

• Christian Eisentraut, Holger Hermanns, Lijun Zhang: On Probabilistic Automata in Continuous Time. LICS 2010: 342-351

• Arnaud Fietzke, Holger Hermanns, Christoph Weidenbach: Superposition-Based Analysis of First-Order Probabilistic Timed Automata. LPAR (Yogyakarta) 2010: 302-316

• Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, Oliver E. Theel: Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems. QEST 2010: 27-36

• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang: PASS: Abstraction Refinement for Infinite Probabilistic Models. TACAS 2010: 353-357

• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang: Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. Fundam. Inform. 95(1): 129-155 (2009)

• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Jan Rakow, Ralf Wimmer, Bernd Becker: Compositional Dependability Evaluation for STATEMATE. IEEE Trans. Software Eng. 35(2): 274-292 (2009)

• Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe: Towards Performance Prediction of Compositional Models in Industrial GALS Designs. CAV 2009: 204-218

• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang: INFAMY: An Infinite-State Markov Model Checker. CAV 2009: 641-647

• Holger Hermanns, Holger Wiechmann: Future Design Challenges for Electric Energy Supply. ETFA 2009: 1-8

• Holger Hermanns, Joost-Pieter Katoen: The How and Why of Interactive Markov Chains. FMCO 2009: 311-337

• Reza Pulungan, Holger Hermanns: Acyclic Minimality by Construction---Almost. QEST 2009: 63-72

• Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen: The Ins and Outs of the Probabilistic Model Checker MRMC. QEST 2009: 167-176

• Arnd Hartmanns, Holger Hermanns: A Modest Approach to Checking Probabilistic Timed Automata. QEST 2009: 187-196

• Jonathan Bogdoll, Holger Hermanns, Lijun Zhang: FlowSim Simulation Benchmarking Platform. QEST 2009: 211-212

• Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang: Probabilistic Reachability for Parametric Markov Models. SPIN 2009: 88-106

• Abhishek Dhama, Oliver E. Theel, Pepijn Crouzen, Holger Hermanns, Ralf Wimmer, Bernd Becker: Dependability Engineering of Silent Self-stabilizing Systems. SSS 2009: 238-253

• Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen: Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. Logical Methods in Computer Science 4(4) (2008)

• Holger Hermanns, Jens Palsberg: Improving the effectiveness of system verification. International Journal on Software Tools for Technology Transfer 10(2): 111-112 (2008)

• Christian Eisentraut, Holger Hermanns: Teaching Concurrency Concepts to Freshmen. T. Petri Nets and Other Models of Concurrency 1: 35-53 (2008)

• Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn, Björn Wachter: Time-bounded model checking of infinite-state continuous-time Markov chains. ACSD 2008: 98-107

• Reza Pulungan, Holger Hermanns: Effective Minimization of Acyclic Phase-Type Representations. ASMTA 2008: 128-143

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Reachability in continuous-time Markov reward decision processes. Logic and Automata 2008: 53-72

• Holger Hermanns, Björn Wachter, Lijun Zhang: Probabilistic CEGAR. CAV 2008: 162-175

• Pepijn Crouzen, Holger Hermanns, Lijun Zhang: On the Minimisation of Acyclic Models. CONCUR 2008: 295-309

• Nicolas Coste, Hubert Garavel, Holger Hermanns, Richard Hersemeule, Yvain Thonnart, Meriem Zidouni: Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures. DATE 2008: 88-89

• Jonathan Bogdoll, Holger Hermanns, Lijun Zhang: An Experimental Evaluation of Probabilistic Simulation. FORTE 2008: 37-52

• Martin Fränzle, Holger Hermanns, Tino Teige: Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems. HSCC 2008: 172-186

• Holger Hermanns, Sven Johr: May we reach it? Or must we? In what time? With what probability? MMB 2008: 125-140

• Reza Pulungan, Holger Hermanns: The Minimal Representation of the Maximum of Erlang Distributions. MMB 2008: 207-222

• Ralf Wimmer, Salem Derisavi, Holger Hermanns: Symbolic Partition Refinement with Dynamic Balancing of Time and Space. QEST 2008: 65-74

• Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen: Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. CoRR abs/0808.3651 (2008)

• Lijun Zhang, Holger Hermanns: Deciding Simulations on Probabilistic Automata. ATVA 2007: 207-222

• Holger Hermanns, Sven Johr: Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems. DSN 2007: 718-728

• Christian Groß, Holger Hermanns, Reza Pulungan: Does Clock Precision Influence ZigBee's Energy Consumptions?. OPODIS 2007: 174-188

• Björn Wachter, Lijun Zhang, Holger Hermanns: Probabilistic Model Checking Modulo Theories. QEST 2007: 129-140

• Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen: Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. TACAS 2007: 155-169

• Henrik C. Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen: motor: The modestTool Environment. TACAS 2007: 500-504

• Werner Damm, Holger Hermanns (Eds.): Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. Lecture Notes in Computer Science 4590, Springer 2007, ISBN 978-3-540-73367-6

• Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Verena Wolf: Bisimulation and Simulation Relations for Markov Chains. Electr. Notes Theor. Comput. Sci. 162: 73-78 (2006)

• Mario Bravetti, Holger Hermanns, Joost-Pieter Katoen: YMCA: - Why Markov Chain Algebra? - . Electr. Notes Theor. Comput. Sci. 162: 107-112 (2006)

• Henrik C. Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen: MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE Trans. Software Eng. 32(10): 812-830 (2006)

• Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker: Sigref- A Symbolic Bisimulation Tool Box. ATVA 2006: 477-492

• Grégory Batt, Jeremy T. Bradley, Roland Ewald, François Fages, Holger Hermanns, Jane Hillston, Peter Kemper, Alke Martens, Pieter J. Mosterman, Flemming Nielson, Oleg Sokolsky, Adelinde M. Uhrmacher: 06161 Working Groups' Report: The Challlenge of Combining Simulation and Verification. Simulation and Verification of Dynamic Systems 2006

• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker: Compositional Performability Evaluation for STATEMATE. QEST 2006: 167-178

• Christel Baier, Holger Hermanns (Eds.): CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings. Lecture Notes in Computer Science 4137, Springer 2006, ISBN 3-540-37376-4

• Holger Hermanns, Jens Palsberg (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings. Lecture Notes in Computer Science 3920, Springer 2006, ISBN 3-540-33056-9

• Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Verena Wolf: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2): 149-214 (2005)

• Markus Lohrey, Pedro R. D'Argenio, Holger Hermanns: Axiomatising divergence. Inf. Comput. 203(2): 115-144 (2005)

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Model checking meets performance evaluation. SIGMETRICS Performance Evaluation Review 32(4): 10-15 (2005)

• David N. Jansen, Holger Hermanns: QoS modelling and analysis with UML-statecharts: the StoCharts approach. SIGMETRICS Performance Evaluation Review 32(4): 28-33 (2005)

• Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Boudewijn R. Haverkort: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci. 345(1): 2-26 (2005)

• Husain Aljazzar, Holger Hermanns, Stefan Leue: Counterexamples for Timed Probabilistic Reachability. FORMATS 2005: 177-195

• Lijun Zhang, Holger Hermanns, David N. Jansen: Logic and Model Checking for Hidden Markov Models. FORTE 2005: 98-112

• Holger Hermanns, David N. Jansen, Yaroslav S. Usenko: From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. WOSP 2005: 13-23

• Christel Baier, Holger Hermanns, Joost-Pieter Katoen: Probabilistic weak simulation is decidable in polynomial time. Inf. Process. Lett. 89(3): 123-130 (2004)

• Henrik C. Bohnenkamp, Holger Hermanns, David N. Jansen, Joost-Pieter Katoen, Yaroslav S. Usenko: An industrial-strength formal method -- A Modest survey. ISoLA (Preliminary proceedings) 2004: 284-295

• Henrik C. Bohnenkamp, Holger Hermanns, Ric Klaren, Angelika Mader, Yaroslav S. Usenko: Synthesis and Stochastic Assessment of Schedules for Lacquer Production. QEST 2004: 28-37

• David N. Jansen, Holger Hermanns: Dependability Checking with StoCharts: Is Train Radio Reliable Enough for Trains? QEST 2004: 250-259

• Joost-Pieter Katoen, Henrik C. Bohnenkamp, Ric Klaren, Holger Hermanns: Embedded Software Analysis with MOTOR. SFM 2004: 268-294

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. TACAS 2004: 61-76

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen, Markus Siegle (Eds.): Validation of Stochastic Systems - A Guide to Current Research. Lecture Notes in Computer Science 2925, Springer 2004, ISBN 3-540-22265-0

• Salem Derisavi, Holger Hermanns, William H. Sanders: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6): 309-315 (2003)

• Holger Hermanns, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Markus Siegle: On the use of MTBDDs for performability analysis and verification of stochastic systems. J. Log. Algebr. Program. 56(1-2): 23-67 (2003)

• Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle: A tool for model-checking Markov chains. International Journal on Software Tools for Technology Transfer 4(2): 153-172 (2003)

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(6): 524-541 (2003)

• Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Verena Wolf: Comparative Branching-Time Semantics. CONCUR 2003: 482-497

• Henrik C. Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen, Ric Klaren: The Modest Modeling Tool and Its Implementation. Computer Performance Evaluation / TOOLS 2003: 116-133

• Henrik C. Bohnenkamp, Peter van der Stok, Holger Hermanns, Frits W. Vaandrager: Cost-Optimization of the IPv4 Zeroconf Protocol. DSN 2003: 531-540

• Henrik C. Bohnenkamp, Tod Courtney, David Daly, Salem Derisavi, Holger Hermanns, Joost-Pieter Katoen, Ric Klaren, Vinh Vi Lam, William H. Sanders: On Integrating the MÖBIUS and MODEST Modeling Tools. DSN 2003: 671

• Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle: ETMCC: Model Checking Performability Properties of Markov Chains. DSN 2003: 673-

• Suzana Andova, Holger Hermanns, Joost-Pieter Katoen: Discrete-Time Rewards Model-Checked. FORMATS 2003: 88-104

• Holger Hermanns, Christophe Joubert: A Set of Performance and Dependability Analysis Components for CADP. TACAS 2003: 425-430

• David N. Jansen, Holger Hermanns, Joost-Pieter Katoen: A QoS-Oriented Extension of UML Statecharts. UML 2003: 76-91

• Holger Hermanns: Interactive Markov Chains: The Quest for Quantified Quality. Lecture Notes in Computer Science 2428, Springer 2002, ISBN 3-540-44261-8

• Holger Hermanns, Joost-Pieter Katoen: Guest editors' introduction: Model checking in a nutshell. J. Log. Algebr. Program. 52-53: 1-5 (2002)

• Holger Hermanns, Ulrich Herzog, Joost-Pieter Katoen: Process algebra for performance evaluation. Theor. Comput. Sci. 274(1-2): 43-87 (2002)

• Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Boudewijn R. Haverkort: Simulation for Continuous-Time Markov Chains. CONCUR 2002: 338-354

• Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier: Model Checking Performability Properties. DSN 2002: 103-112

• Hubert Garavel, Holger Hermanns: On Combining Functional Verification and Performance Evaluation Using CADP. FME 2002: 410-429

• David N. Jansen, Holger Hermanns, Joost-Pieter Katoen: A Probabilistic Extension of UML Statecharts. FTRTFT 2002: 355-374

• Markus Lohrey, Pedro R. D'Argenio, Holger Hermanns: Axiomatising Divergence. ICALP 2002: 585-596

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Automated Performance and Dependability Evaluation Using Model Checking. Performance 2002: 261-289

• Holger Hermanns, Roberto Segala (Eds.): Process Algebra and Probabilistic Methods, Performance Modeling and Verification, Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002, Proceedings. Lecture Notes in Computer Science 2399, Springer 2002, ISBN 3-540-43913-7

• Holger Hermanns: Construction and Verification of Performance and Reliability Models. Bulletin of the EATCS 74: 135-153 (2001)

• Holger Hermanns, Joost-Pieter Katoen: Performance Evaluation : = (Process Algebra + Model Checking) × Markov Chains. CONCUR 2001: 59-81

• Gabriel G. Infante López, Holger Hermanns, Joost-Pieter Katoen: Beyond Memoryless Distributions: Model Checking Semi-Markov Chains. PAPM-PROBMIV 2001: 57-70

• Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen, Ric Klaren: MoDeST - A Modelling and Description Language for Stochastic Timed Systems. PAPM-PROBMIV 2001: 87-104

• Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen (Eds.): Lectures on Formal Methods and Performance Analysis, First EEF/Euro Summer School on Trends in Computer Science, Berg en Dal, The Netherlands, July 3-7, 2000, Revised Lectures. Lecture Notes in Computer Science 2090, Springer 2001, ISBN 3-540-42479-2

• Holger Hermanns, Ulrich Herzog, Ulrich Klehmet, Vassilis Mertsiotakis, Markus Siegle: Compositional performance modelling with the TIPPtool. Perform. Eval. 39(1-4): 5-35 (2000)

• Holger Hermanns, Joost-Pieter Katoen: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36(1): 97-127 (2000)

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Model Checking Continuous-Time Markov Chains by Transient Analysis. CAV 2000: 358-372

• Ed Brinksma, Holger Hermanns: Process Algebra and Markov Chains. European Educational Forum: School on Formal Methods and Performance Analysis 2000: 183-231

• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: On the Logical Characterisation of Performability Properties. ICALP 2000: 780-792

• Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle: Towards Model Checking Stochastic Process Algebra. IFM 2000: 420-439

• Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: On the Use of Model Checking Techniques for Dependability Evaluation. SRDS 2000: 228-237

• Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle: A Markov Chain Model Checker. TACAS 2000: 347-362

• Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen: On Generative Parallel Composition. Electr. Notes Theor. Comput. Sci. 22: 30-54 (1999)

• Holger Hermanns, Markus Siegle: Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation. ARTS 1999: 244-264

• Holger Hermanns, Vassilis Mertsiotakis, Markus Siegle: TIPPtool: Compositional Specification and Analysis of Markovian Performance Models. CAV 1999: 487-490

• Christel Baier, Joost-Pieter Katoen, Holger Hermanns: Approximate Symbolic Model Checking of Continuous-Time Markov Chains. CONCUR 1999: 146-161

• Holger Hermanns, Ulrich Herzog, Vassilis Mertsiotakis: Stochastic Process Algebras - Between LOTOS and Markov Chains. Computer Networks 30(9-10): 901-924 (1998)

• Holger Hermanns, Markus Lohrey: Priority and Maximal Progress Are Completely Axiomatisable (Extended Abstract). CONCUR 1998: 237-252

• Holger Hermanns, Ulrich Herzog, Ulrich Klehmet, Vassilis Mertsiotakis, Markus Siegle: Compositional Performance Modelling with TIPPtool. Computer Performance Evaluation (Tools) 1998: 51-62

• Holger Hermanns, Marina Ribaudo: Exploiting Symmetries in Stochastic Process Algebras. ESM 1998: 763-770

• Christel Baier, Holger Hermanns: Weak Bisimulation for Fully Probabilistic Processes. CAV 1997: 119-130

• Holger Hermanns, Vassilis Mertsiotakis, Michael Rettelbach: A Construction and Analysis Tool Based on the Stochastic Process Algebra TIPP. TACAS 1996: 427-430

• Holger Hermanns, Michael Rettelbach, Thorsten Weiss: Formal Characterisation of Immediate Actions in SPA with Nondeterministic Branching. Comput. J. 38(7): 530-541 (1995)