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

DOI10.2168/LMCS-7(1:12)2011zbMath1233.68156MaRDI 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 checking; continuous-time Markov chains; piecewise-deterministic Markov processes; deterministic timed automata; linear-time specification

Mathematics Subject Classification ID

68Q45: Formal languages and automata

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

45D05: Volterra integral equations

60J28: Applications of continuous-time Markov processes on discrete state spaces

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

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

Uses Software

• PRISM
• MRMC