Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
From MaRDI portal
model checkingcontinuous-time Markov chainspiecewise-deterministic Markov processesdeterministic timed automatalinear-time specification
Applications of continuous-time Markov processes on discrete state spaces (60J28) Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Volterra integral equations (45D05) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
- Model-checking continuous-time Markov chains
- scientific article; zbMATH DE number 7760477
- Time-bounded model checking of infinite-state continuous-time Markov chains
- scientific article; zbMATH DE number 1670788
- scientific article; zbMATH DE number 1361121
- Theoretical Aspects of Computing - ICTAC 2004
- Model checking conditional CSL for continuous-time Markov chains
- Model checking for probabilistic timed automata
- LTL model checking of time-inhomogeneous Markov chains
Cited in
(25)- Probabilistic model checking for energy-utility analysis
- LTL model checking of time-inhomogeneous Markov chains
- scientific article; zbMATH DE number 1670788 (Why is no real title available?)
- Guarded autonomous transitions increase conciseness and expressiveness of timed automata
- Observing continuous-time MDPs by 1-clock timed automata
- Verification of linear duration properties over continuous-time Markov chains
- Automata-based CSL model checking
- CONCUR 2003 - Concurrency Theory
- Learning deterministic probabilistic automata from a model checking perspective
- Monitoring CTMCs by multi-clock timed automata
- On-the-fly verification and optimization of DTA-properties for large Markov chains
- Analysis of timed and long-run objectives for Markov automata
- Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
- Verification of linear duration properties over continuous-time markov chains
- Model-checking continuous-time Markov chains
- Fluid model checking of timed properties
- Model checking single agent behaviours by fluid approximation
- Checking individual agent behaviours in Markov population models by fluid approximation
- The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
- Measuring performance of continuous-time stochastic processes using timed automata
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- Strict Divergence for Probabilistic Timed Automata
- Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
- A probabilistic logic for verifying continuous-time Markov chains
- scientific article; zbMATH DE number 1759607 (Why is no real title available?)
This page was built for publication: Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003315)
