Journal Article To Parallelize or to Optimize? Get access Jonathan Ezekiel, Jonathan Ezekiel Department of Computing, Imperial College, London, UK.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Gerald Lüttgen, Gerald Lüttgen Department of Computer Science, University of York, Heslington, York YO10 5DD, UK.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Radu Siminiceanu Radu Siminiceanu National Institute of Aerospace, Hampton, Virginia, USA.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 21, Issue 1, February 2011, Pages 85–120, https://doi.org/10.1093/logcom/exp006 Published: 12 February 2009 Article history Received: 29 February 2008 Published: 12 February 2009

SMART is a software package integrating logic and stochastic modeling formalisms into a single environment. Models expressed in different formalisms can be combined in the same study. To study logical behavior, both explicit and symbolic state-space generation techniques, as well as CTL model-checking algorithms, are available. To study stochastic and timing behavior, both explicit and Kronecker-based numerical solution approaches are available. Since SMART is intended as an industry and research tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.