Abstract
In this paper, we propose an efficient algorithm for the parameter synthesis of PLTL formulas with respect to parametric Markov chains. The PLTL formula is translated to an almost fully partitioned B¨uchi automaton which is then composed with the parametric Markov chain. We then reduce the problem to solving an optimisation problem, allowing to decide the satisfaction of the formula using an SMT solver. The algorithm works also for interval Markov chains. The complexity is linear in the size of the Markov chain, and exponential in the size of the formula. We provide a prototype and show the efficiency of our approach on a number of benchmarks.
Original language | English |
---|---|
Title of host publication | Dependable Software Engineering: Theories, Tools, and Applications |
Subtitle of host publication | Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings |
Editors | Martin Franzle, Deepak Kapur, Naijun Zhan |
Place of Publication | Cham |
Publisher | Springer |
Pages | 280-296 |
Number of pages | 17 |
ISBN (Electronic) | 978-3-319-47677-3 |
ISBN (Print) | 978-3-319-47676-6 |
DOIs | |
Publication status | Published - 2016 |
Externally published | Yes |
Event | 2nd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2016 - Beijing, China Duration: 9 Nov 2016 → 11 Nov 2016 Conference number: 2 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 9984 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 2nd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2016 |
---|---|
Abbreviated title | SETTA |
Country/Territory | China |
City | Beijing |
Period | 9/11/16 → 11/11/16 |
Keywords
- Markov chain
- Model check
- Markov chain model
- Product graph
- Strongly connect component