Three-Valued Abstraction for Continuous-Time Markov Chains

DOI10.1007/978-3-540-73368-3_37zbMath1135.68476OpenAlexW2157239333MaRDI QIDQ5429326

Verena Wolf, Martin Leucker, Daniel Klink, Joost-Pieter Katoen

Publication date: 29 November 2007

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73368-3_37

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (16)

Spotlight abstraction in model checking real-time task schedulability ⋮ Lumpability for uncertain continuous-time Markov chains ⋮ Least upper bounds for probability measures and their applications to abstractions ⋮ Analyzing Oscillatory Behavior with Formal Methods ⋮ Precise parameter synthesis for stochastic biochemical systems ⋮ Consistency and refinement for interval Markov chains ⋮ Specification Theories for Probabilistic and Real-Time Systems ⋮ Constraint Markov chains ⋮ The How and Why of Interactive Markov Chains ⋮ Abstract Probabilistic Automata ⋮ Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates ⋮ A linear process-algebraic format with data for probabilistic automata ⋮ Probabilistic model checking of biological systems with uncertain kinetic rates ⋮ Compositional Abstraction for Stochastic Systems ⋮ Model checking for performability ⋮ Smoothed model checking for uncertain continuous-time Markov chains

Uses Software

• Unnamed Item
• SMART_
• MRMC
• PEPA

This page was built for publication: Three-Valued Abstraction for Continuous-Time Markov Chains