About: [Image: see text] is a statistical model checker that uses antithetic and stratified sampling techniques to reduce the number of samples and, hence, the amount of time required before making a decision. The tool is capable of statistically verifying any black-box probabilistic system that [Image: see text] can simulate, against probabilistic bounds on any property that [Image: see text] can evaluate over individual executions of the system. We have evaluated our tool on many examples and compared it with both symbolic and statistical algorithms. When the number of strata is large, our algorithms reduced the number of samples more than 3 times on average. Furthermore, being a statistical model checker makes [Image: see text] able to verify models that are well beyond the reach of current symbolic model checkers. On large systems (up to [Formula: see text] states) [Image: see text] was able to check 100% of benchmark systems, compared to existing symbolic methods in [Image: see text] , which only succeeded on 13% of systems. The tool, installation instructions, benchmarks, and scripts for running the benchmarks are all available online as open source.   Goto Sponge  NotDistinct  Permalink

An Entity of Type : fabio:Abstract, within Data Space : covidontheweb.inria.fr associated with source document(s)

AttributesValues
type
value
  • [Image: see text] is a statistical model checker that uses antithetic and stratified sampling techniques to reduce the number of samples and, hence, the amount of time required before making a decision. The tool is capable of statistically verifying any black-box probabilistic system that [Image: see text] can simulate, against probabilistic bounds on any property that [Image: see text] can evaluate over individual executions of the system. We have evaluated our tool on many examples and compared it with both symbolic and statistical algorithms. When the number of strata is large, our algorithms reduced the number of samples more than 3 times on average. Furthermore, being a statistical model checker makes [Image: see text] able to verify models that are well beyond the reach of current symbolic model checkers. On large systems (up to [Formula: see text] states) [Image: see text] was able to check 100% of benchmark systems, compared to existing symbolic methods in [Image: see text] , which only succeeded on 13% of systems. The tool, installation instructions, benchmarks, and scripts for running the benchmarks are all available online as open source.
Subject
  • Statistical models
  • Prediction
  • Mathematical modeling
  • Decision-making
  • Scientific modeling
  • Statistical theory
  • Probability theory
part of
is abstract of
is hasSource of
Faceted Search & Find service v1.13.91 as of Mar 24 2020


Alternative Linked Data Documents: Sponger | ODE     Content Formats:       RDF       ODATA       Microdata      About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data]
OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software