Central limit model checking

We consider probabilistic model checking for continuous-time Markov chains (CTMCs) induced from Stochastic Reaction Networks against a fragment of Continuous Stochastic Logic (CSL) extended with reward operators. Classical numerical algorithms for CSL model checking based on uniformisation are limit...

Full description

Bibliographic Details
Main Authors: Bortolussi, L, Cardelli, L, Kwiatkowska, M, Laurenti, L
Format: Journal article
Published: Association for Computing Machinery 2019