Abstract
Continuous Stochastic Logic (CSL) can be interpreted over continuoustime
Markov decision processes (CTMDPs) to specify quantitative properties of
stochastic systems that allow some external control. Model checking CSL formulae
over CTMDPs requires then the computation of optimal control strategies to
prove or disprove a formula. The paper presents a conservative extension of CSL
over CTMDPs—with rewards—and exploits established results for CTMDPs for
model checking CSL. A new numerical approach based on uniformization is devised
to compute time bounded reachability results for time dependent control
strategies. Experimental evidence is given showing the efficiency of the approach.
Original language | English |
---|---|
Title of host publication | Computer Aided Verification : 23rd International Conference, CAV 2011 - Snowbird, UT, USA, July 14-20, 2011 - Proceedings |
Publisher | Springer |
Publication date | 2011 |
Pages | 225-242 |
ISBN (Print) | 978-3-642-22109-5 |
ISBN (Electronic) | 978-3-642-22110-1 |
DOIs | |
Publication status | Published - 2011 |
Event | 23rd International Conference on Computer Aided Verification - Snowbird, United States Duration: 14 Jul 2011 → 20 Jul 2011 Conference number: 23 |
Conference
Conference | 23rd International Conference on Computer Aided Verification |
---|---|
Number | 23 |
Country/Territory | United States |
City | Snowbird |
Period | 14/07/2011 → 20/07/2011 |
Series | Lecture Notes in Computer Science |
---|---|
Number | 6806 |
ISSN | 0302-9743 |