An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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üchi 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 - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings
PublisherSpringer
Pages280-296
Volume9984
DOIs
Publication statusPublished - 06 Oct 2016
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume 9984
ISSN (Electronic)0302-9743

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