A CTL Model Checker for Stochastic Automata Networks

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. PRISM (Probabilistic Model Checker), http://www.prismmodelchecker.org/

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)

   Chapter  Google Scholar 

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)

   Article  Google Scholar 

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)

   Article  Google Scholar 

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. 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)

   Chapter  Google Scholar 

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)

   Chapter  Google Scholar 

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. Lampka, K., Siegle, M.: Analysis of Markov reward models using zero-suppressed multi-terminal BDDs. In: VALUETOOLS, p. 35 (2006)

    Google Scholar 

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. 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. PEPS Project, http://www-id.imag.fr/Logiciels/peps/userguide.html

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. 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 

Download references