Validation of Stochastic Systems 2

• Applicant: Professorin Dr. Christel Baier
• Subject Area: Software Engineering and Programming Languages
• Term: from 2001 to 2008
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5307294

• Final Report Year: 2008

Final Report Abstract

No abstract available

Publications

• Interface automata, ACM SIGSOFT Softw. Eng. Notes, 26(5): 109-120, 2001
  L. de Alfaro, T.A. Henzinger
  
• (2005) Efficient computation of time-bounded reachability probabilities in uniform continuoustime Markov decision processes. Theoretical Computer Science (TCS), 345(1), 2-26. ISSN 0304-3975
  Baier, C. and Hermanns, H. and Katoen, J.P. and Haverkort, B.R.H.M
  
• A Model Checker for Markov Reward Models, Proceedings of Quantitative Evaluation of Systems (QEST 2005), 2005
  J.-P. Katoen, M. Khattri, I. Zapreev
  
• A Theory of Stochastic Systems Part I: Stochastic Automata, Information & Computation volume 203 no. 1, pp.1-38,-2005
  P.R. DArgenio and J.-P. Katoen
  
• A Theory of Stochastic Systems Part II: Process Algebra, Information & Computation volume 203, no. 1, pp.39-74,-2005
  P.R. DArgenio and J.-P. Katoen
  
• Activity-Local Symbolic State Graph Generation for High-Level Stochastic Models, Universität der Bundeswehr München, Fakultät für Informatik, 2005
  K. Lampka and M. Siegle
  
• Are you still there? A lightweight algorithm to monitor node absence in self-configuring networks, Proceedings of Dependable Systems & Networks (DSN 2005), IEEE CS Press, 2005
  H. Bohnenkamp, J. Gorter, J. Guidi and J.-P. Katoen
  
• Beyond Model-Checking CSL for QBDs: Resets, Batches and Rewards, Proceedings of the 7th Int.l Workshop on PMCCS, pp.23 - 26, 2005
  A. Remke, B.R. Haverkort
  
• Comparative branching-time semantics for Markov chains. Information and Compututation, 200(2), 149-214, 2005
  C. Baier, J.-P. Katoen, H. Hermanns, V. Wolf
  
• Hyperbolic PDEs for CSRL Model Checking: A Deja Vu. Proceedings of the 7th Int.l Workshop on Performability Modelling of Computer and Communication Systems, pp.19-22, September 2005
  L. Cloth, B.R. Haverkort
  
• Model checking for Survivability, Proceedings of the 2nd Int.l Conference on the Quantitative Evaluation of SysTems (QEST 2005), ISBN: 0-7695-2427-3, pp.145-154, September 2005
  L. Cloth, B.R. Haverkort
  
• Model Checking Infinite-State Markov Chains, Proceedings of llth Int.l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) ISBN: 3-540-25333-5, pp.237-252, April 2005
  A. Remke, B.R. Haverkort, L. Cloth
  
• Model checking Markov reward models with impulse rewards. Proceedings of Dependable Systems & Networks (DSN 2005), IEEE CS Press, 2005
  L. Cloth, J.-P. Katoen, M. Khattri and R. Pulungan
  
• Model checking meets performance evaluation, SIGMETRICS Performance Evaluation Review 32(4), pp.10-15, 2005
  C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen
  
• Probabilistic Models for Reo Connector Circuits. Journal of Universal Computer Science, 11(10): 1718-1748, 2005
  C. Baier
  
• ProbMela and Model Checking Markov Decision Processes. Special issue of ACM Performance Evaluation Review on Performance and Verification, 32(4), pp.22-27, 2005
  C. Baier and F. Ciesinski and M. Grosser
  
• Quantitative Analysis of Distributed Randomized Protocols. In Proc. of the 10th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2005). ACM Press, 2005
  C. Baier and P. Ciesinski and M. Grösser
  
• Switched Probabilistic I/O Automata LNCS 3407, ISSN: 0302-9743: pp.494-510, 2005
  L. Cheung, N.A. Lynch, R. Segala, F.W. Vaandrager
  
• Symbolic and Parametric Model Checking of Discrete-Time Markov Chains LNCS 3407, ISSN: 0302-9743: pp.280-294, 2005
  C. Daws
  
• Timed Testing with TorX, Formal Methods 2005, LNCS 3582, pp.173-188, 2005
  H.C. Bohnenkamp, A. Belinfante
  
• "A Model Checking Strategy for a Performance Measure of Fluid Stochastic Models". Springer Verlag, LNCS 4054, EPEW 2006, pp.93-107
  M. L. Bujorianu, M. C. Bujorianu
  
• A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes, Proc. of 4th International Conference Formal Modeling and Analysis of Timed Systems (FORMATS 2006), Paris (France). Lecture Notes in Computer Science 4202, pp.352-367, Springer-Verlag, 2006
  N. Wolovick and S. Johr
  
• A note on the attractor-property of infinitestate Markov chains. Information Processing Letters, 97(2): 58-63, 2006
  C. Baier, N. Betrand, Ph. Schnoebelen
  
• A Semantic Framework for Test Coverage. Proceedings ATVA'06, 2006
  L. Brandan Briones, E. Brinksma, and M.I.A. Stoelinga
  
• A testing scenario for probabilistic processes, Technical Report ICIS-R06002, Institute for Computing and Information Sciences, Radboud University Nijmegen, January 2006
  L. Cheung, M.I.A. Stoelinga, and F.W. Vaandrager
  
• A tool for Qualitative and Quantitative Linear Time analysis of Reactive Systems, Proc. QEST'06, IEEE CS Press, pp.131-132, 2006
  F. Ciesinski, Ch. Baier, Li Quor
  
• A versatile infinite-state Markov reward model to study bottlenecks in 2-hop ad hoc networks, Proc. of Third International Conference on the Quantitative Evaluation of Systems, 11-14 Sept 2006, Riverside, CA. pp.63-72. IEEE Computer Society Press
  A. Remke, B.R.H.M. Haverkort and L. Cloth
  
• Activity-Local Symbolic State Graph Generation for High- Level Stochastic Models, Proc. of 13th GI/ITG Conference on "Measuring, Modelling and Evaluation of Computer and Communication Systems" (MMB), pp.245-263, 2006
  K. Lampka and M. Siegle
  
• Analysis of a protocol for dynamic configuration of IPv4 link local addresses using Uppaal, Technical Report ICIS-R06016, Institute for Computing and Information Sciences, Radboud University Nijmegen, 2006
  B. Gebremichael, F.W. Vaandrager, and M. Zhang
  
• Analysis of Markov Reward Models using Zero-suppressed Multi-terminal BDDs, Proc. of 1st Int. Conf. on Performance Evaluation Methodologies and Tools (Valuetools 2006), ACM press, ISBN 1-59593-504-5, 10 pages, 2006
  K. Lampka and M. Siegle
  
• Analysis of the zeroconf protocol using uppaal, Proceedings 6th Annual ACM & IEEE Conference on Embedded Software (EMSOFT 20D6), Seoul, South Korea, October 22-25, 2006, pp.242-251. ACM Press, 2006
  B. Gebremichael, F-W. Vaandrager, and M. Zhang
  
• Bisimulation and Simulation Relations for Markov Chains, Electronic Notes in Theoretical Computer Science, vol. 162, pp.73-78, 2006
  Ch. Baier, J.-P. Katoen, H. Hermanns and V. Wolf
  
• Bottlenecks in Two-Hop Ad Hoc Networks - Dividing Radio Capacity in a Smart Way, Proc. of Stochastic Performance Models for Resource Allocation in Communication Systems, 8-10 Nov, Amsterdam, pp.23-26, 2006
  A. Remke, B.R.H.M. Haverkort and L. Cloth
  
• CASPA: Symbolic Model Checking of Stochastic Systems. Proc. of 13th GI/ITG Conference on "Measuring, Modelling and Evaluation of Computer and Communication Systems" (MMB), pp.469-472, 2006
  M. Kuntz and M. Siegle
  
• Compositional Performability Evaluation for STATEMATE, Proc. of 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006, Riverside (USA), pp.167-178, IEEE Computer Society, 2006
  E. Boede, M. Herbstritt, H. Hermanns, S. Johr, Th. Peikenkamp, R. Pulungan, R. Wimmer and B. Becker
  
• Computer Aided Verification, 19th International Conference, CAV 2007. Lecture Notes in Computer Science 4590, Springer-Verlag, 2006
  Werner Damm and Holger Hermanns
  
• CONCUR 2006—Concurrency Theory, 16th International Conference. Lecture Notes in Computer Science 4137, Springer-Verlag, 2006
  Christel Baier and Holger Hermanns
  
• Constraint-oriented specification of performance aspects. In: Architectural Design of Open Distributed Systems: From Interface to Telematics (Liber Amicorum dedicated to Chris Vissers). Telematica Instituut, Enschede, 2006, pp.47- 54. ISBN 90-75176-41-4
  J.-P. Katoen
  
• Counterexamples in probabilistic model checking, Technical Report AIB 2006-09, RWTH Aachen, 2006
  T. Han and J.-P. Katoen.
  
• CSL model checking of deterministic and stochastic Petri nets, Proceedings 13th GI/ITG conference on measuring, Modelling and Evaluation of Computer and Communication Systems, March 27-29, 2006, Nuernberg, Germany, pp.265-282. Springer Verlag
  J.M. Martinez Verdugo and B.R.H.M. Haverkort
  
• Distributed Disk-Based Solution of Very Large Markov Chains. Formal Methods in System Design, 29(2): 177-196, 2006
  A. Bell and B.R.H.M. Haverkort
  
• Editorial for the special issue on DSN 2005. IEEE Transactions on Dependable and Secure Computing 3(3): 169-171, 2006
  J. Arlat, A. Bondavalli, B.R.H.M. Haverkort and P. Verissimo
  
• Five Performability Algorithms. A Comparison, Proc. of Markov Anniversary Meeting 2006 (MAM 2006), 12-14 Jun 2006, Charleston, SC, USA. pp.39-54. Boson Books
  L. Cloth and B.R.H.M. Haverkort
  
• Functional abstractions of stochastic hybrid systems, Proc. of 2nd IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2006, Alghero (Italy), pp. 160-165, 2006
  M. Bujorianu, H. A. P. Blom and H. Hermanns
  
• MathMC: A mathematica-based tool for CSL model checking of deterministic and stochastic Petri nets, Proceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems, September 11-14, 2006, Riverside, CA, USA. pp.133-134. IEEE Computer Society Press
  J.M. Martinez Verdugo and B.R.H.M. Haverkort
  
• Measuring and modelling of application flow length in commercial GPRS networks, Proc. of Third International Conference on the Quantitative Evaluation of Systems, 11-14 September 2006, Riverside, CA, USA. pp.83-92. IEEE Computer Society
  R.A. Kalden, R.A and B.R.H.M. Haverkort
  
• MoDeST: A compositional modeling formalism for real-time and stochastic systems. IEEE Transactions on Software Engineering, 32(10): 812-830, 2006
  H. Bohnenkamp, P.R. D'Argenio, H. Hermanns, and J-P. Katoen
  
• On computing fixpoints in well-ordered regular model checking, with applications to lossy channel systems, Proc. LPAR'06, Lecture Notes in Computer Science 4246, pp.347-361, 2006
  Ch. Baier, N. Bertrand and Ph. Schnoebelen
  
• On reduction criteria for probabilistic reward models. In Proc. 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06). Lecture Notes in Computer Science 3337, pp.309-320, 2006
  M. Größer, G. Norman, Ch. Baier, F. Ciesinski, M. Kwiatkowska and D. Parker
  
• Orthogonal Distance Fitting for Phase-Type Distributions. ATR 10, SFB/TR 14 AVACS, 2006
  R. Pulungan and H. Hermanns
  
• Partial Order Reduction for Markov Decision Processes: A Survey. In Proc. of the 4th International Symposium on Formal Methods for Component and Objects (FMCO '05). Lecture Notes in Computer Science 4111, pp.408-427, 2006
  M. Grosser and C. Baier
  
• Partial Order Reduction for Probabilistic Branching Time. In Proc. of the 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL '05). ENTCS 153(2), pp.97-116, 2006
  C. Baier and P.R. D'Argenio and M. Grösser
  
• Probably on time and within budget: On reachability in priced probabilistic timed automata, Proceedings Third International Conference on the Quantitative Evaluation of SysTems (QEST 2006), 11-14 September 2006, Riverside, CA, USA, pages 311-322, Los Alamitos, CA, USA, 2006. IEEE Computer Society
  J. Berendsen, D.N. Jansen, and J.P. Katoen
  
• Probably on time and within budget: On reachability in priced probabilistic timed automata, Technical Report ICIS- R06023, Institute for Computing and Information Sciences, Radboud University Nijmegen, August 2006
  J. Berendsen, D.N. Jansen, and J.P. Katoen
  
• Probably on time and within budget: on reachability in priced probabilistic timed automata, Technical Report TR-CTIT- 06-26, Centre for Telematics and Information Technology, University of Twente, Enschede, June 2006
  J. Berendsen, D.N. Jansen, and J.P. Katoen
  
• Quantitative Compositional Reasoning, Proceedings of QEST06
  K. Chatterjee, L. de Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M.I.A. Stoelinga
  
• Safe on-the-fiy steady-state detection for timebounded reachability. In Quantitative Evaluation of Systems (QEST), pp.301-310, IEEE CS Press, 2006
  J.-P. Katoen, and I. S. Zapreev
  
• Sigref - A Symbolic Bisimulation Tool Box, Proc. 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006, Beijing (China). Lecture Notes in Computer Science 4218, Springer-Verlag, 2006
  R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp.and B. Becker
  
• Stochastic model checking. In Christos G. Cassandras, and John Lygeros, editors, Stochastic Hybrid Systems: Recent Developments and Research Trends. Taylor and Francis, 2006
  J.-P. Katoen
  
• Stochastic Reasoning About Channel-Based Component Connectors/ Proc 8th International Conference on Coordination Models and Languages (COORDINATION), Lecture Notes in Computer Science 4038, pages 1-15, 2006
  Ch. Baier, V. Wolf
  
• Switched PIOA: Parallel composition via distributed scheduling. Theoretical Computer Science 365(1/2): 83- 108, 2006
  L. Cheung, N.A. Lynch, R. Segala, and F.W. Vaandrager
  
• Symbolic Model Checking of Stochastic Systems: Theory and Implementation, Proc. of 13th Int. SPIN Workshop, LNCS 3925, pp.89-107, 2006
  M. Kuntz and M. Siegle
  
• Symbolic Reasoning with Weighted and Normalized Decision Diagrams. In Proc. of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus '05). ENTCS, 151(3), pp.39- 56, 2006
  J. Ossowski and C. Baier
  
• Symbolic verification of communication systems with probabilistic message losses: liveness and fairness, Proc. FORTE , Lecture Notes in Computer Science 4229, pp.212-227, 2006
  Ch. Baier, N. Bertrand and Ph. Schnoebelen
  
• Synthesis and Stochastic Assessment of Cost-Optimal Schedules, CTIT TR 06-14, University of Twente, 2006. ISSN 1381-3625
  A. Mader, H. Bohnenkamp, Y. S. Usenko, D. N. Jansen, J. Hurink and H. Hermanns
  
• Task-structured probabilistic I/O automata, Proceedings of the 8th International Workshop on Discrete Event Systems (WODES'06), 2006. Ann Arbor, Michigan, July 2006
  R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala
  
• Task-structured probabilistic I/O automata. Technical Report MIT-CSAIL- TR-2006-060, MIT CSAIL, 2006
  R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala
  
• Time-bounded task-PIOAs: a framework for analyzing security protocols, Proceedings of the 20th International Symposium on Distributed Computing (DISC '06), 2006. Stockholm, Sweden, September 2006
  R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala
  
• Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006. Lecture Notes in Computer Science 3920, Springer-Verlag, 2006
  Holger Hermanns and Jens Palsberg
  
• Towards a logic for performance and mobility. Electronic Notes in Theoretical Computer Science, 153:161175, 2006
  R. De Nicola, J.-P. Katoen, D. Latella, and M. Massink
  
• Towards Stochastic Hybrid System Modeling. Springer Verlag, Lecture Notes in Control and Information Sciences, 337, H.A.P. Blom and J. Lygeros (Eds.), "Stochastic Hybrid Systems: Theory and Safety Critical Applications". 2006, pp.3-30.
  M. L. Bujorianu, J. Lygeros
  
• Uniformization with Representatives - comprehensive transient analysis of infinite-state QBDs, Proc. of First International Conference on Performance Evaluation Methodologies and Tools, 10 Oct 2006, Pisa, Italy
  A. Remke, B.R.H.M. Haverkort and L. Cloth
  
• Using task-structured probabilistic I/O automata to analyze cryptographic protocols, Proc. Workshop on Formal and Computational Cryptography (FCC 2006), pages 34- 39, 2006
  R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala
  
• vEaluation of Battery Lifetimes using Inhomogeneous Markov Reward Models. Technical Report TR-CTIT-06-58 Centre for Telematics and Information Technology, University of Twente, Enschede, 2006
  L. Cloth, B.R.H.M. Haverkort and M.R. Jongerden
  
• Verifying Finite State Machines in Probabilistic Environments, Proc. of 9th ITG/GI/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV), pp.248-254, 2006
  M. Siegle
  
• Viewpoint Development of Stochastic Hybrid Systems. Proceedings IEEE Conference on Decision and Control 2006
  M. L. Bujorianu, M. C. Bujorianu
  
• YMCA — Why Markov Chain Algebra?, Electronic Notes in Theoretical Computer Science, vol. 162, pp. 107-112, 2006
  M. Bravetti, H. Hermanns and J.-P. Katoen
  
• (2007) A centralized feedback control model for resource management in wireless networks. In: Proceedings of the The Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8), 20 - 21 Sept 2007, Edinburgh, Scotland, pp.10- 16. CTIT Workshop Proceedings. Centre for Telematics and Information Technology, University of Twente. ISSN 0929-0672
  Yang, Y. and Haverkort, B.R.H.M. and Heijenk, G.J.
  
• (2007) A compositional reliability and availability evaluation tool. In: ARTIST workshop: Tool Platforms for Embedded Systems Modeling, Analysis and Validation. Presented at the 19th International conference on Computer Aided Verification, July 1-2, 2007, Berlin, Germany. ARTIST2 Network of Excellence on Embedded Systems Design
  Boudali, H. and Crouzen, P. and Stoelinga, M.I.A.
  
• (2007) A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. In: 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), October 22-25, 2007, Tokyo, Japan, pp.441-456. Lecture Notes in Computer Science 4762. Springer. ISSN 0302-9743 ISBN 978-3-540-75595-1
  oudali, H. and Crouzen, P. and Stoelinga, M.I.A.
  
• (2007) A testing scenario for probabilistic processes. Journal of the Association for Computing Machinery, 54 (6). 29:1-29:45. ISSN 0004-5411
  Cheung, L. and Stoelinga, M.I.A. and Vaandrager, F.W.
  
• (2007) Best of Three Worlds: Towards Sound Architectural Dependability Models. In: 8th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), September 20-21, 2007, Edinburgh, UK. pp.45-49. CTIT Workshop Proceedings. ISSN 0929-0672
  Boudali, H. and Haverkort, B.R.H.M. and Kuntz, G.W.M. and Stoelinga, M.I.A.
  
• (2007) Computing Battery Lifetime Distributions. In: Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2007), 25-28 Jun 2007, Edinburgh, UK. pp.780-789. IEEE Computer Society Press. ISBN 978-0-7695-2855-7
  Cloth, L. and Haverkort, B.R.H.M. and Jongerden, M.R.
  
• (2007) CSL model checking algorithms for QBDs. Theoretical Computer Science, 382 (1). pp.24-41. ISSN 0304- 3975
  Remke, A.K.I, and Haverkort, B.R.H.M. and Cloth, L.
  
• (2007) Dynamic Fault Tree analysis using Input/Output Interactive Markov Chains. In: Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 25-28 June 2007, Edinburgh, UK. pp.708-717. IEEE Computer Society Press. ISBN 0-7695-2855-4
  Boudali, H. and Crouzen, P and Stoelinga, M.I.A.
  
• (2007) Faster SPDL Model Checking Through Property-Driven State Space Generation. In: Proceedings of the Fourth European Performance Engineering Workshop, EPEW 2007, 27-28 Sept 2007, Berlin, Germany, pp.80-96. Lecture Notes in Computer Science 4748. Springer Verlag. ISBN 978-3-540-75210-3
  Kuntz, G.W.M. and Haverkort, B.R.H.M.
  
• (2007) Game Relations and Metrics. In: Twenty-Second Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2007), 1014 July 2007, Wroclav, Poland, pp.99-108. IEEE Computer Society Press. ISSN 1055-0143
  de Alfaro, L. and Majumdar, R. and Raman, V. and Stoelinga, M.I.A.
  
• (2007) GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. In: Proceedings of The Eighth International Workshop on Performability Modeling of Computer and Communication Systems, 20-21 Sept 2007, Edinburgh, UK. pp.50-56. Centre for Telematics and Information Technology, University of Twente. ISSN 0929-0672
  Kuntz, G.W.M. and Haverkort, B.R.H.M.
  
• (2007) Model Checking Markov Chains with Actions and State Labels. IEEE transactions on software engineering, 33(4), 209-224. ISSN 0098-5589
  Baier, C. and Cloth, L. and Haverkort, B.R.H.M. and Kuntz, G.W.M. and Siegle, M.
  
• (2007) Parallel CSRL Model Checking: First Results and Pointers to the Future. In: Proceedings of the Sixth International Workshop on Parallel and Distributed Methods in Verification, 08 July 2007, Berlin, Germany, pp. 105-120. CTIT. ISSN 0929-0672
  Kuntz, G.W.M. and Haverkort, B.R.H.M.
  
• 2007) CSL Model Checking Algorithms for Infinite-state Structured Markov chains. In: 5th International Conference, FOR- MATS 2007, 3-5 Oct 2007, Salzburg, pp.336-351. Lecture Notes in Computer Science 4763. Springer Verlag. ISBN 978-3-540-75453-4
  Remke, A.K.I, and Haverkort, B.R.H.M.
  
• A Multilevel Algorithm based on Binary Decision Diagramms, 14th Int. Conf. on Analytical and Stochastic Modelling Techniques and Applications (ASMTA'07), pp.129-136, 2007
  J. Schuster and M. Siegle
  
• Abstraction of Probabilistic Systems. In Formal Methods for Timed Systems (FORMATS'07). pages 13. Volume 4763 of LNCS. Springer-Verlag, 2007
  J.-P. Katoen
  
• An easy-to-use, efficient tool-chain to analyze the availability of 1 elecommunication equipment, Proc. of llth Int. Workshop on Formal Methods foi Industrial Critical Systems (FMICS'06), Springer, LNCS 4346, pages 35-50, 2007
  K. Lampka, M. Siegle and M. Walter
  
• Arcade - A Formal, Extensible, Model-based Dependability Evaluation Framework. Proceedings of the 3rd International IEEE UML/AADL Workshop, 2007
  H. Boudali and P.Crouzen and B.R.H.M. Haverkort and M. Kuntz and M.I.A. Stoelinga
  
• Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. In 18th International Conference on Concurrency Theory (CONCUR'07). pages 412427. Volume 4703 of LNCS. Springer-Verlag, 2007
  M.R. Neuhäusser, and J.-P. Katoen
  
• Bisimulation minimisation mostly speeds up probabilistic model checking.. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07). pages 7692. Volume 4424 of Lecture Notes in Computer Science. Springer Verlag, 2007
  J.-P. Katoen, T. Kemna, IS. Zapreev, and D.N. Jansen
  
• Can matrix-layout-independent numerical solvers be efficient? - Implementing the Moebius State-Level Abstract Functional Interface for ZDDs, Proc. 2nd Int. Conf. on Performance Evaluation Methodologies and Tools (Valuetools'07), SMCtools Workshop, 10 pages, ACM press, 2007
  K. Lampka, S. Harwarth, M. Siegle
  
• Compositional abstraction in real-time model checking. Technical Report 1C1S-R07027, Institute for Computing and Information Sciences, Radboud University Nijmegen, November 2007
  J. Berendsen and F.W. Vaandrager
  
• Compositional security for task-PIOAs. In Proceedings 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 125-139, Los Alamitos, CA, USA, 2007. IEEE Computer Society
  R. Canetti, L. Cheung, D. Kaynar, N. Lynch, and O. Pereira
  
• Deciding Simulations on Probabilistic Automata. In Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings. Lecture Notes in Computer Science 4762, pp.207-222, Springer-Verlag, 2007
  L. Zhang and H. Hermanns
  
• Does Clock Precision Influence ZigBee's Energy Consumptions? In: Principles of Distributed Systems, llth International Conference, OPODIS 2007. Lecture Notes in Computer Science 4878, pp. 174-188, Springer-Verlag, 2007
  C. Groß, H. Hermanns, and R. Pulungan
  
• Flow faster: efficient decision algorithms for probabilistic simulations. In Orna Grumberg, and Michael Huth, editors, Tools and algorithms for the construction and analysis of systems. pages 155169. Volume 4424 of Lecture notes in computer science. Springer, 2007
  L. Zhang, H. Hermanns, F. Eisenbrand, and D.N. Jansen
  
• Formal Methods: Applications and Technology, llth International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006. Lecture Notes in Computer Science 4346, Springer-Verlag 2007
  Lubos Brim, Boudewijn R. Haverkort, Martin Leucker, Jaco van de Pol
  
• Formal specification and analysis of Zeroconf using Uppaal. Technical Report ICIS-R07032, Radboud University Nijmegen, December 2007
  J. Berendsen, B. Gebremichael, Miaomiao Zhang, and F.W. Vaandrager
  
• Model checking mobile stochastic logic. Theoretical Computer Science, 382:4270, 2007
  R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti, and M. Massink
  
• Motor: The MoDeST Tool Environment. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07). pages 500504. Volume 4424 of Lecture Notes in Computer Science. Springer-Verlag, 2007
  H. Bohnenkamp, H. Hermanns, and J.-R Katoen
  
• Observing branching structure through probabilistic contexts. SIAM Journal on Computing, 37(4):977-1013, 2007
  N.A. Lynch, R. Segala, and F.W. Vaandrager
  
• OpenSESAME: The Simple but Extensive, Structured Availability Modeling Environment, Reliability Engineering and System Safety 93(6): 857-873, 200
  M. Walter and M. Siegle and A. Bode
  
• Probabilistic Model Checking Modulo Theories. In Fourth International Conference on the Quantitative Evaluation of Systems, QEST 2007, Edinburgh, Scotland, 17-19 September 2007. pp.718-727, IEEE CS press, 2007
  B. Wachter, L. Zhang and H. Hermanns
  
• Providing evidence of likely being on time Counterexample generation for CTMC model checking. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07). Lecture Notes in Computer Science, pp.60-75, Springer Verlag, 2007
  T. Han, and J.-P. Katoen
  
• Stochastic Game Logic. In Proc. of the 4th International Conference on Quantitative Evaluation of SysTems (QEST '07). IEEE Computer Society Press, pp.227-236, 2007
  C. Baier and T. Brazdil and M. Grösser and A. Kucera
  
• Three-valued abstraction for continuous-time Markov chains. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV). pages 311324. Volume 4590 of Lecture Notes in Computer Science. Springer Verlag, 2007
  J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf
  
• Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems. In: Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2007), Edinburgh, UK. pp.718-728. IEEE Computer Society Press
  H. Hermanns and S. Johr
  
• A symbolic multilevel method with sparse submatrix representation for memory-speed tradeoff, 14. GI/ITG Konferenz Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen (MMB08), pp.191-206, 2008
  J. Schuster and M. Siegle
  
• An Experimental Evaluation of Probabilistic Simulation. In FORTE. Lecture Notes in Computer Science, Springer Verlag, 2008
  J. Bogdoll, H. Hermanns, and L. Zhang
  
• Architectural Dependability evaluation with Arcade, Proceedings 38th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, IEEE Computer Society, 2008
  H. Boudali, P. Crouzen, B.R. Haverkort, M. Kuntz, M.I.A. Stoelinga
  
• Effective Minimization of Acyclic Phase-Type Representations. In 15th International Conference on Analytical and Stochastic Modelling Techniques and Applications, ASMTA'08. Lecture Notes in Computer Science 5055, pp.128-143, Springer-Verlag, 2008
  R. Pulungan and H. Hermanns.
  
• May We Reach It? Or Must We? In What Time? With What Probability?, 14. GI/ITG Konferenz Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen (MMB08), pp. 125-140, 2008
  H. Hermanns and S. Johr
  
• On Decision Problems for Probabilistic Buechi Automata. In Proc. of the llth International Conference on Foundations of Software Science and Computation Structures (FOSSACS '08). Lecture Notes in Computer Science 4962, pp.287-301, 2008
  C. Baier and N. Bertrand and M. Grösser
  
• Preface: Special issue: CONCUR 2006. Information and Computation 206(5):461, 2008
  C. Baier and H. Hermanns
  
• Probabilistic CEGAR. In Computer Aided Verification, 20th International Conference, CAV 2008. Lecture Notes in Computer Science. Springer Verlag, 2008
  H. Hermanns, B. Wachter and L. Zhang
  
• Reduction Methods for Probabilistic Model Checking. PhD thesis, TU Dresden
  M. Grosser
  
• The Minimal Representation of the Maximum of Erlang Distributions, 14. GI/ITG Konferenz Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen (MMB08), pp. 207-221, 2008
  R. Pulungan and H. Hermanns
  
• Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. In Proceedings of the 8th International Conference on Application of Concurrency to System Design. IEEE Computer Society Press. 2008
  L. Zhang, H. Hermanns, E.M. Hahn, and B. Wachter
  
• Compositional Dependability Evaluation for STATEMATE, IEEE Transactions on Software Engineering, 2008
  E. Boede, M. Herbßtritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, R. Wimmer and B. Becker