Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification of probabilistic systems. However, the representation of the transition matrix may be expensive for very large systems and may induce a prohibitive cost for the model checking algorithm. In this paper, we propose an approximation method to verify quantitative properties on discrete Markov chains. We give a randomized algorithm to approximate the probability that a property expressed by some positive LTL formula is satisfied with high confidence by a probabilistic system. Our randomized algorithm requires only a succinct representation of the system and is based on an execution sampling method. We also present an implementation and a few classical examples to demonstrate the effectiveness of our approach.

References in zbMATH (referenced in 24 articles , 2 standard articles )

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

1 2 next

  1. Damiani, Ferruccio; Viroli, Mirko: Type-based self-stabilisation for computational fields (2015)
  2. Dannenberg, Frits; Kwiatkowska, Marta; Thachuk, Chris; Turberfield, Andrew J.: DNA walker circuits: computational potential, design, and verification (2013)
  3. Zuliani, Paolo; Platzer, André; Clarke, Edmund M.: Bayesian statistical model checking with application to Stateflow/Simulink verification (2013)
  4. Ghorbal, Khalil; Duggirala, Parasara Sridhar; Kahlon, Vineet; Ivančić, Franjo; Gupta, Aarti: Efficient probabilistic model checking of systems with ranged probabilities (2012)
  5. Clarke, Edmund M.; Zuliani, Paolo: Statistical model checking for cyber-physical systems (2011)
  6. David, Alexandre; Larsen, Kim G.; Legay, Axel; Mikučionis, Marius; Poulsen, Danny Bøgsted; van Vliet, Jonas; Wang, Zheng: Statistical model checking for networks of priced timed automata (2011)
  7. Jha, Sumit Kumar; Langmead, Christopher James: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement (2011)
  8. Behjati, Razieh; Sirjani, Marjan; Nili Ahmadabadi, Majid: Bounded rational search for on-the-fly model checking of LTL properties (2010)
  9. Alturki, Musab; Meseguer, José; Gunter, Carl A.: Probabilistic modeling and analysis of dos protection for the ASV protocol (2009)
  10. Ciocchetta, Federica; Gilmore, Stephen; Guerriero, Maria Luisa; Hillston, Jane: Integrated simulation and model-checking for the analysis of biochemical systems (2009)
  11. Heiner, Monika; Lehrack, Sebastian; Gilbert, David; Marwan, Wolfgang: Extended stochastic Petri nets for model-based design of wetlab experiments (2009)
  12. Ölveczky, Peter Csaba; Thorvaldsen, Stian: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude (2009)
  13. Lassaigne, Richard; Peyronnet, Sylvain: Probabilistic verification and approximation (2008)
  14. Cadilhac, Michaël; Hérault, Thomas; Lassaigne, Richard; Peyronnet, Sylvain; Tixeuil, Sébastien: Evaluating complex MAC protocols for sensor networks with APMC (2007)
  15. Cadilhac, Michaël; Hérault, Thomas; Lassaigne, Richard; Peyronnet, Sylvain; Tixeuil, Sébastien: Evaluating complex MAC protocols for sensor networks with APMC. (2007)
  16. Bournez, Olivier; Garnier, Florent: Proving positive almost sure termination under strategies (2006)
  17. Grosu, Radu; Smolka, Scott A.: Monte Carlo methods for process algebra. (2006)
  18. Guirado, Guillaume; Hérault, Thomas; Lassaigne, Richard; Peyronnet, Sylvain: Distribution, approximation and probabilistic model checking. (2006)
  19. Lassaigne, Richard; Peyronnet, Sylvain: Probabilistic verification and approximation. (2006)
  20. Markey, Nicolas; Schnoebelen, Philippe: Mu-calculus path checking (2006)

1 2 next