swMATH ID: 8425
Software Authors: Koushik Sen, Mahesh Viswanathan, Gul Agha
Description: 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.
Homepage: http://osl.cs.illinois.edu/media/papers/sen-2005-qest-vesta.pdf
Related Software: PRISM; Maude; HOL; Ymer; PVeStA; PMaude; ML; COSMOS; Uppaal; PLASMA; APMC; HASL; MRMC; PAGODA; MultiVeStA; CafeOBJ; MACOM; Isabelle; MOMENT2; Ptolemy
Cited in: 22 Publications

Citations by Year