Abstract
This paper reports on our efforts to link an industrial state-of-the-art modelling tool to academic state-of-the-art analysis algorithms. In a nutshell, we enable timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from STATEMATE models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible. The entire tool flow has been implemented, and it is applied to a nontrivial example.
Original language | English |
---|---|
Title of host publication | 3rd International Conference on Quantitative Evaluation of Systems, QEST 2006 |
Publisher | IEEE Computer Society |
Pages | 167-176 |
Number of pages | 10 |
ISBN (Print) | 0-7695-2665-9 |
DOIs | |
Publication status | Published - 2006 |
Event | 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States Duration: 11 Sep 2006 → 14 Sep 2006 Conference number: 3 http://www.qest.org/qest2006/ |
Conference
Conference | 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 |
---|---|
Abbreviated title | QEST |
Country/Territory | United States |
City | Riverside |
Period | 11/09/06 → 14/09/06 |
Internet address |
Keywords
- EWI-9280
- METIS-237967