A CTL Model Checker for Stochastic Automata Networks

  • Lucas Oleksinski
  • Claiton Correa
  • Fernando Luís Dotti
  • Afonso Sales
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)


Stochastic Automata Networks (SAN) is a Markovian formalism devoted to the quantitative evaluation of concurrent systems. Unlike other Markovian formalisms and despite its interesting features, SAN does not count with the support of model checking. This paper discusses the architecture, the main features and the initial results towards the construction of a symbolic CTL Model Checker for SAN. A parallel version of this model checker is also briefly discussed.


Model Checker Computation Tree Logic Node Memory Reachable State Space Markov Reward Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Brenner, L., Fernandes, P., Sales, A.: The Need for and the Advantages of Generalized Tensor Algebra for Structured Kronecker Representations. Int. Journal of Simulation: Systems, Science & Technology (IJSIM) 6(3-4), 52–60 (2005)Google Scholar
  2. 2.
    PRISM (Probabilistic Model Checker),
  3. 3.
    Ciardo, G., Lüttgen, G., Siminiceanu, R.I.: Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS Performance Evaluation Review 36(4), 58–63 (2009)CrossRefGoogle Scholar
  5. 5.
    Ciardo, G., Zhao, Y., Jin, X.: Ten Years of Saturation: A Petri Net Perspective. Transactions Petri Nets and Other Models of Concurrency 5, 51–95 (2012)CrossRefGoogle Scholar
  6. 6.
    Dotti, F.L., Fernandes, P., Sales, A., Santos, O.M.: Modular Analytical Performance Models for Ad Hoc Wireless Networks. In: WiOpt 2005, pp. 164–173 (2005)Google Scholar
  7. 7.
    Kuntz, M., Siegle, M., Werner, E.: Symbolic Performance and Dependability Evaluation with the Tool CASPA. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol. 3236, pp. 293–307. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Lampka, K., Siegle, M.: Activity-local symbolic state graph generation for high-level stochastic models. In: 13th MMB, pp. 245–264. VDE Verlag (2006)Google Scholar
  10. 10.
    Lampka, K., Siegle, M.: Analysis of Markov reward models using zero-suppressed multi-terminal BDDs. In: VALUETOOLS, p. 35 (2006)Google Scholar
  11. 11.
    Miner, A., Parker, D.: Symbolic Representations and Analysis of Large Probabilistic Systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) AUTONOMY 2003. LNCS, vol. 2925, pp. 296–338. Springer, Heidelberg (2004)Google Scholar
  12. 12.
    Plateau, B.: On the stochastic structure of parallelism and synchronization models for distributed algorithms. In: ACM SIGMETRICS Conf. on Measurements and Modeling of Computer Systems, Austin, USA, pp. 147–154. ACM Press (1985)Google Scholar
  13. 13.
  14. 14.
    Sales, A.: SAN lite-solver: a user-friendly software tool to solve SAN models. In: SpringSim (TMS-DEVS), Orlando, FL, USA, vol. 44, pp. 9–16. SCS/ACM (2012)Google Scholar
  15. 15.
    Sales, A., Plateau, B.: Reachable state space generation for structured models which use functional transitions. In: QEST 2009, Budapest, Hungary, pp. 269–278 (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Lucas Oleksinski
    • 1
  • Claiton Correa
    • 1
  • Fernando Luís Dotti
    • 1
  • Afonso Sales
    • 1
  1. 1.PUCRS - FACINPorto AlegreBrazil

Personalised recommendations