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 proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationDependable Software Engineering: Theories, Tools, and Applications
Subtitle of host publicationSecond International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings
EditorsMartin Franzle, Deepak Kapur, Naijun Zhan
Place of PublicationCham
PublisherSpringer
Pages280-296
Number of pages17
ISBN (Electronic)978-3-319-47677-3
ISBN (Print)978-3-319-47676-6
DOIs
Publication statusPublished - 2016
Externally publishedYes
Event2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, China
Duration: 9 Nov 201611 Nov 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9984
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016
CountryChina
CityBeijing
Period9/11/1611/11/16

Keywords

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

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