Model checking CSL until formulae with random time bounds
From MaRDI portal
Numerical analysis or methods applied to Markov chains (65C40) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Recommendations
Cited in
(11)- Consecutive customer losses in regular and oscillating \(M^{X}/ G /1/ n\) systems
- Analysis of \(GI^{X}/ M(n)// N\) systems with stochastic customer acceptance policy
- Analysis of \(\text{GI}/\text{M}/s/c\) queues using uniformisation
- Model checking expected time and expected reward formulae with random time bounds
- Model checking continuous-time Markov chains by transient analysis
- Time-bounded model checking of infinite-state continuous-time Markov chains
- CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
- A Uniformization-Based Algorithm for Model Checking the CSL Until Operator on Labeled Queueing Networks
- Beyond memoryless distributions: model checking semi-Markov chains
- Randomization helps in LTL model checking
- Consecutive customer losses in oscillating \(GI^X/M//n\) systems with state dependent services rates
This page was built for publication: Model checking CSL until formulae with random time bounds
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4813203)
