An efficient synthesis algorithm for parametric markov chains against linear time properties

Yong Li; Wanwei Liu; Andrea Turrini; Ernst Moritz Hahn; Lijun Zhang

doi:10.1007/978-3-319-47677-3_18

An efficient synthesis algorithm for parametric markov chains against linear time properties

Yong Li, Wanwei Liu, Andrea Turrini^*, Ernst Moritz Hahn, Lijun Zhang

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

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	https://doi.org/10.1007/978-3-319-47677-3_18
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

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
Country	China
City	Beijing
Period	9/11/16 → 11/11/16

Keywords

Markov chain
Model check
Markov chain model
Product graph
Strongly connect component

Access to Document

10.1007/978-3-319-47677-3_18

Link to publication in Scopus

Fingerprint Dive into the research topics of 'An efficient synthesis algorithm for parametric markov chains against linear time properties'. Together they form a unique fingerprint.

Cite this

Li, Y., Liu, W., Turrini, A., Hahn, E. M., & Zhang, L. (2016). An efficient synthesis algorithm for parametric markov chains against linear time properties. In M. Franzle, D. Kapur, & N. Zhan (Eds.), Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings (pp. 280-296). (Lecture Notes in Computer Science; Vol. 9984). Springer. https://doi.org/10.1007/978-3-319-47677-3_18

Li, Yong ; Liu, Wanwei ; Turrini, Andrea ; Hahn, Ernst Moritz ; Zhang, Lijun. / An efficient synthesis algorithm for parametric markov chains against linear time properties. Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. editor / Martin Franzle ; Deepak Kapur ; Naijun Zhan. Cham : Springer, 2016. pp. 280-296 (Lecture Notes in Computer Science).

@inproceedings{4d799c23d19b4183a1e1385550e851b2,

title = "An efficient synthesis algorithm for parametric markov chains against linear time properties",

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.",

keywords = "Markov chain, Model check, Markov chain model, Product graph, Strongly connect component",

author = "Yong Li and Wanwei Liu and Andrea Turrini and Hahn, {Ernst Moritz} and Lijun Zhang",

year = "2016",

doi = "10.1007/978-3-319-47677-3_18",

language = "English",

isbn = "978-3-319-47676-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "280--296",

editor = "Martin Franzle and Deepak Kapur and Naijun Zhan",

booktitle = "Dependable Software Engineering: Theories, Tools, and Applications",

note = "2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 ; Conference date: 09-11-2016 Through 11-11-2016",

}

Li, Y, Liu, W, Turrini, A, Hahn, EM & Zhang, L 2016, An efficient synthesis algorithm for parametric markov chains against linear time properties. in M Franzle, D Kapur & N Zhan (eds), Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9984, Springer, Cham, pp. 280-296, 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016, Beijing, China, 9/11/16. https://doi.org/10.1007/978-3-319-47677-3_18

An efficient synthesis algorithm for parametric markov chains against linear time properties. / Li, Yong; Liu, Wanwei; Turrini, Andrea; Hahn, Ernst Moritz; Zhang, Lijun.

Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. ed. / Martin Franzle; Deepak Kapur; Naijun Zhan. Cham : Springer, 2016. p. 280-296 (Lecture Notes in Computer Science; Vol. 9984).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - An efficient synthesis algorithm for parametric markov chains against linear time properties

AU - Li, Yong

AU - Liu, Wanwei

AU - Turrini, Andrea

AU - Hahn, Ernst Moritz

AU - Zhang, Lijun

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Markov chain

KW - Model check

KW - Markov chain model

KW - Product graph

KW - Strongly connect component

UR - http://www.scopus.com/inward/record.url?scp=84994496504&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-47677-3_18

DO - 10.1007/978-3-319-47677-3_18

M3 - Conference contribution

SN - 978-3-319-47676-6

T3 - Lecture Notes in Computer Science

SP - 280

EP - 296

BT - Dependable Software Engineering: Theories, Tools, and Applications

A2 - Franzle, Martin

A2 - Kapur, Deepak

A2 - Zhan, Naijun

PB - Springer

CY - Cham

T2 - 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016

Y2 - 9 November 2016 through 11 November 2016

ER -

Li Y, Liu W, Turrini A, Hahn EM, Zhang L. An efficient synthesis algorithm for parametric markov chains against linear time properties. In Franzle M, Kapur D, Zhan N, editors, Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Cham: Springer. 2016. p. 280-296. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-47677-3_18