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 28 articles , 2 standard articles )

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

1 2 next

  1. Daca, Przemysław; Henzinger, Thomas A.; Křetínský, Jan; Petrov, Tatjana: Faster statistical model checking for unbounded temporal properties (2017)
  2. Lukina, Anna; Esterle, Lukas; Hirsch, Christian; Bartocci, Ezio; Yang, Junxing; Tiwari, Ashish; Smolka, Scott A.; Grosu, Radu: ARES: adaptive receding-horizon synthesis of optimal plans (2017)
  3. D’Argenio, Pedro R.; Hartmanns, Arnd; Legay, Axel; Sedwards, Sean: Statistical approximation of optimal schedulers for probabilistic timed automata (2016)
  4. Jegourel, Cyrille; Legay, Axel; Sedwards, Sean: Command-based importance sampling for statistical model checking (2016)
  5. Mao, Hua; Chen, Yingke; Jaeger, Manfred; Nielsen, Thomas D.; Larsen, Kim G.; Nielsen, Brian: Learning deterministic probabilistic automata from a model checking perspective (2016)
  6. Damiani, Ferruccio; Viroli, Mirko: Type-based self-stabilisation for computational fields (2015)
  7. Dannenberg, Frits; Kwiatkowska, Marta; Thachuk, Chris; Turberfield, Andrew J.: DNA walker circuits: computational potential, design, and verification (2015)
  8. Latella, Diego; Loreti, Michele; Massink, Mieke: On-the-fly fast mean-field model-checking (2014)
  9. Dannenberg, Frits; Kwiatkowska, Marta; Thachuk, Chris; Turberfield, Andrew J.: DNA walker circuits: computational potential, design, and verification (2013)
  10. Fahrenberg, Uli; Larsen, Kim G.; Legay, Axel: Model-based verification, optimization, synthesis and performance evaluation of real-time systems (2013)
  11. Molesini, Ambra; Casadei, Matteo; Omicini, Andrea; Viroli, Mirko: Simulation in Agent-Oriented Software Engineering: the SODA case study (2013) ioport
  12. Zuliani, Paolo; Platzer, André; Clarke, Edmund M.: Bayesian statistical model checking with application to Stateflow/Simulink verification (2013)
  13. Ghorbal, Khalil; Duggirala, Parasara Sridhar; Kahlon, Vineet; Ivančić, Franjo; Gupta, Aarti: Efficient probabilistic model checking of systems with ranged probabilities (2012)
  14. Clarke, Edmund M.; Zuliani, Paolo: Statistical model checking for cyber-physical systems (2011)
  15. 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)
  16. Jha, Sumit Kumar; Langmead, Christopher James: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement (2011)
  17. Behjati, Razieh; Sirjani, Marjan; Nili Ahmadabadi, Majid: Bounded rational search for on-the-fly model checking of LTL properties (2010)
  18. Heiner, Monika; Lehrack, Sebastian; Gilbert, David; Marwan, Wolfgang: Extended stochastic Petri nets for model-based design of wetlab experiments (2009)
  19. Ölveczky, Peter Csaba; Thorvaldsen, Stian: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude (2009)
  20. Lassaigne, Richard; Peyronnet, Sylvain: Probabilistic verification and approximation (2008)

1 2 next