Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

DOI10.2168/LMCS-7(1:12)2011zbMath1233.68156OpenAlexW3103183526MaRDI QIDQ3003315

Alexandru Mereacre, Taolue Chen, Tingting Han, Joost-Pieter Katoen

Publication date: 26 May 2011

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2168/lmcs-7(1:12)2011

zbMATH Keywords

model checkingcontinuous-time Markov chainspiecewise-deterministic Markov processesdeterministic timed automatalinear-time specification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Volterra integral equations (45D05) Applications of continuous-time Markov processes on discrete state spaces (60J28) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (12)

Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Fluid Model Checking of Timed Properties ⋮ Learning deterministic probabilistic automata from a model checking perspective ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Automata-Based CSL Model Checking ⋮ On-the-fly verification and optimization of DTA-properties for large Markov chains ⋮ Guarded autonomous transitions increase conciseness and expressiveness of timed automata ⋮ Probabilistic Model Checking for Energy-Utility Analysis ⋮ The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism ⋮ Model checking single agent behaviours by fluid approximation

Uses Software

• PRISM
• MRMC

This page was built for publication: Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications