Logical and stochastic modeling with smart. We describe the main features of Smart, a software package providing a seamless environment for the logic and probabilistic analysis of complex systems. Smart can combine different formalisms in the same modeling study. For the analysis of logical behavior, both explicit and symbolic state-space generation techniques, as well as symbolic CTL model-checking algorithms, are available. For the study of stochastic and timing behavior, both sparse-storage and Kronecker numerical solution approaches are available when the underlying process is a Markov chain. In addition, discrete-event simulation is always applicable regardless of the stochastic nature of the process, but certain classes of non-Markov models can still be solved numerically. Finally, since Smart targets both the classroom and realistic industrial settings as a learning, research, and application tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.

References in zbMATH (referenced in 33 articles )

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

1 2 next

  1. Jing, Yaping; Miner, Andrew S.: Computation tree measurement language (CTML) (2018)
  2. Juan F. Pérez; Daniel F. Silva; Julio C. Góez; Andrés Sarmiento; Andrés Sarmiento-Romero; Raha Akhavan-Tabatabaei; Germán Riaño: Algorithm 972: jMarkov: An Integrated Framework for Markov Chain Modeling (2017) not zbMATH
  3. Marussy, Kristóf; Klenik, Attila; Molnár, Vince; Vörös, András; Majzik, István; Telek, Miklós: Efficient decomposition algorithm for stationary analysis of complex stochastic Petri net models (2016)
  4. Amparore, Elvio Gilberto; Beccuti, Marco; Donatelli, Susanna: (Stochastic) model checking in GreatSPN (2014) ioport
  5. Iacono, M.; Barbierato, E.; Gribaudo, M.: The simthesys multiformalism modeling framework (2012) ioport
  6. Katoen, Joost-Pieter; Klink, Daniel; Leucker, Martin; Wolf, Verena: Three-valued abstraction for probabilistic systems (2012)
  7. Mühlberg, Jan Tobias; Lüttgen, Gerald: Verifying compiled file system code (2012) ioport
  8. Brázdil, Tomáš; Krčál, Jan; Křetínský, Jan; Řehák, Vojtěch: Fixed-delay events in generalized semi-Markov processes revisited (2011)
  9. Schwarick, Martin; Tovchigrechko, Alexej: IDD-based model validation of biochemical networks (2011)
  10. Ciardo, Gianfranco; Mecham, Galen; Paviot-Adet, Emmanuel; Wan, Min: P-semiflow computation with decision diagrams (2009)
  11. Henzinger, Thomas A.; Jobstmann, Barbara; Wolf, Verena: Formalisms for specifying Markovian population models (2009)
  12. Wan, Min; Ciardo, Gianfranco: Symbolic reachability analysis of integer timed Petri nets (2009)
  13. Wan, Min; Ciardo, Gianfranco: Symbolic state-space generation of asynchronous systems using extensible decision diagrams (2009)
  14. Yu, Andy Jinqing; Ciardo, Gianfranco; Lüttgen, Gerald: Decision-diagram-based techniques for bounded reachability checking of asynchronous systems (2009) ioport
  15. Zimmermann, Armin: Stochastic discrete event systems. Modeling, evaluation, applications. (2008)
  16. Aldini, Alessandro; Bernardo, Marco: Mixing logics and rewards for the component-oriented specification of performance measures (2007)
  17. Bozzano, Marco; Villafiorita, Adolfo: The fSAP/NuSMV-SA safety analysis platform (2007) ioport
  18. Ciardo, Gianfranco; Lüttgen, Gerald; Miner, Andrew S.: Exploiting interleaving semantics in symbolic state-space generation (2007)
  19. Katoen, Joost-Pieter; Klink, Daniel; Leucker, Martin; Wolf, Verena: Three-valued abstraction for continuous-time Markov chains (2007)
  20. Siminiceanu, Radu I.; Ciardo, Gianfranco: Formal verification of the NASA runway safety monitor (2007) ioport

1 2 next