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

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

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

Publication date: 26 May 2011

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

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, 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