VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems. VESTA is a tool for statistical analysis of probabilistic systems. It supports statistical model-checking [6, 7] and statistical evaluation of expected values of temporal expressions. For model-checking VESTA uses a sequence of inter-related statistical hypothesis testing to check if a property specified in probabilistic computation tree logic (PCTL) [3] or continuous stochastic logic (CSL) is satisfied by a stochastic model. Furthermore, VESTA supports the statistical computation of expected values of expressions written in a query language called Quantitative Temporal Expressions (or QUATEX in short). We next describe the various components of the tool.

References in zbMATH (referenced in 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Bentriou, Mahmoud; Ballarini, Paolo; Cournède, Paul-Henry: Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models (2021)
  2. Liu, Si; Ölveczky, Peter Csaba; Wang, Qi; Gupta, Indranil; Meseguer, José: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis (2019)
  3. Wang, Yu; Roohi, Nima; West, Matthew; Viswanathan, Mahesh; Dullerud, Geir E.: Statistical verification of PCTL using antithetic and stratified samples (2019)
  4. Maximova, Maria; Giese, Holger; Krause, Christian: Probabilistic timed graph transformation systems (2018)
  5. Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: Command-based importance sampling for statistical model checking (2016)
  6. Ballarini, Paolo; Duflot, Marie: Applications of an expressive statistical model checking approach to the analysis of genetic circuits (2015)
  7. Arnold, Florian; Gebler, Daniel; Guck, Dennis; Hatefi, Hassan: A tutorial on interactive Markov chains (2014)
  8. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014) ioport
  9. Liu, Liya; Hasan, Osman; Aravantinos, Vincent; Tahar, Sofiène: Formal reasoning about classified Markov chains in HOL (2013)
  10. Liu, Liya; Hasan, Osman; Tahar, Sofiène: Formal reasoning about finite-state discrete-time Markov chains in HOL (2013)
  11. Bae, Kyungmin; Ölveczky, Peter Csaba; Feng, Thomas Huining; Lee, Edward A.; Tripakis, Stavros: Verifying hierarchical Ptolemy II discrete-event models using real-time maude (2012)
  12. Barbot, Benoît; Haddad, Serge; Picaronny, Claudine: Coupling and importance sampling for statistical model checking (2012)
  13. Bruni, Roberto; Corradini, Andrea; Gadducci, Fabio; Lluch Lafuente, Alberto; Vandin, Andrea: Modelling and analyzing adaptive self-assembly strategies with Maude (2012) ioport
  14. Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: A platform for high performance statistical model checking -- PLASMA (2012)
  15. Meseguer, José: Twenty years of rewriting logic (2012)
  16. AlTurki, Musab; Meseguer, José: PVeSTA: A parallel statistical model checking and quantitative analysis tool (2011) ioport
  17. Bentea, Lucian; Ölveczky, Peter Csaba: Probabilistic real-time rewrite theories and their expressive power (2011)
  18. Hasan, Osman; Tahar, Sofiène: Reasoning about conditional probabilities in a higher-order-logic theorem prover (2011)
  19. Liu, Liya; Hasan, Osman; Tahar, Sofiène: Formalization of finite-state discrete-time Markov chains in HOL (2011)
  20. Hasan, Osman; Abbasi, Naeem; Tahar, Sofiène: Formal probabilistic analysis of stuck-at faults in reconfigurable memory arrays (2009)

1 2 next