Command-based importance sampling for statistical model checking

DOI10.1016/J.TCS.2016.08.009MaRDI QIDQ313977zbMATH OpenOpenAlexFDO

Authors Cyrille Jegourel, Axel Legay, Sean Sedwards

Publication date 12 September 2016

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2016.08.009

zbMATH Keywords

cross entropyguarded commandsimportance samplingMonte Carlorare eventsstatistical model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Coupling and importance sampling for statistical model checking
• Statistical model checking for cyber-physical systems
• Rare-event verification for stochastic hybrid systems
• Importance sampling for stochastic timed automata
• Statistical model checking

Cites work

• A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations
• A platform for high performance statistical model checking -- PLASMA
• A study on the cross-entropy method for rare-event probability estimation
• Axiomatic derivation of the principle of maximum entropy and the principle of minimum cross-entropy
• Computer Aided Verification
• Coupling and importance sampling for statistical model checking
• Fast simulation of Markov chains with small transition probabilities
• Fast simulation of rare events in queueing and reliability models
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 3514781 (Why is no real title available?)
• scientific article; zbMATH DE number 2087806 (Why is no real title available?)
• scientific article; zbMATH DE number 2117879 (Why is no real title available?)
• scientific article; zbMATH DE number 3241743 (Why is no real title available?)
• Importance Sampling for the Simulation of Highly Reliable Markovian Systems
• Importance sampling simulations of Markovian reliability systems using cross-entropy
• Optimization of computer simulation models with rare events
• Probability Inequalities for Sums of Bounded Random Variables
• Rare Event Simulation using Monte Carlo Methods
• Sequential Tests of Statistical Hypotheses
• Some inequalities relating to the partial sum of binomial probabilities
• Statistical model checking for cyber-physical systems
• Symbolic model checking: \(10^{20}\) states and beyond
• The cross-entropy method for combinatorial and continuous optimization
• The Monte Carlo Method
• The Zagreb coindices of graph operations

Cited in

(4)

• Importance sampling for stochastic timed automata
• Coupling and importance sampling for statistical model checking
• Importance sampling for determining SRAM yield and optimization with statistical constraint
• Statistical model checking for cyber-physical systems

Describes a project that uses

Uses Software

• PLASMA
• PRISM
• VESTA
• COSMOS
• PLASMA-lab
• Uppaal
• Ymer
• APMC

This page was built for publication: Command-based importance sampling for statistical model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q313977)