SMART: the stochastic model checking analyzer for reliability and timing

SMART provides a seamless environment for the logic and probabilistic analysis of complex systems, for use in both the classroom and industrial applications. While initially designed as a powerful stochastic environment integrating multiple modeling formalisms, SMART now includes logical analysis and employs some of the most efficient data structures and algorithms for the analysis of discrete-state systems. For logical behavior, explicit and symbolic state-space generation techniques and symbolic CTL model-checking algorithms are available. For stochastic and timing behavior, sparse-storage and Kronecker-based numerical solution approaches are available when the underlying process is a Markov chain, and discrete-event simulation is available for any type of underlying process. In addition, certain classes of nonMarkov models can be solved numerically.