Three-Valued Abstraction for Continuous-Time Markov Chains

DOI10.1007/978-3-540-73368-3_37MaRDI QIDQ5429326zbMATH OpenOpenAlexFDO

Authors Daniel Klink, Martin Leucker, Verena Wolf, 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)

Recommendations

• Three-valued abstraction for probabilistic systems
• Abstraction for Stochastic Systems by Erlang’s Method of Stages
• Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL
• Compositional abstraction for stochastic systems
• Sliding Window Abstraction for Infinite Markov Chains

Cited in

(20)

• Three-valued abstraction for probabilistic systems
• Smoothed model checking for uncertain continuous-time Markov chains
• Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates
• Lumpability for uncertain continuous-time Markov chains
• Spotlight abstraction in model checking real-time task schedulability
• The how and why of interactive Markov chains
• Analyzing oscillatory behavior with formal methods
• Constraint Markov chains
• Model checking for performability
• Compositional abstraction for stochastic systems
• Least upper bounds for probability measures and their applications to abstractions
• Consistency and refinement for interval Markov chains
• Model checking CSL for Markov population models
• Precise parameter synthesis for stochastic biochemical systems
• Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL
• A linear process-algebraic format with data for probabilistic automata
• Specification Theories for Probabilistic and Real-Time Systems
• Sliding Window Abstraction for Infinite Markov Chains
• Probabilistic model checking of biological systems with uncertain kinetic rates
• Abstract probabilistic automata

Describes a project that uses

Uses Software

• PEPA
• MRMC
• SMART_
• SIGREF

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5429326)