Compositional Verification and Optimization of Interactive
Markov Chains

D 2013

Compositional Verification and Optimization of Interactive Markov Chains

HERMANNS, Holger, Jan KRČÁL and Jan KŘETÍNSKÝ

Basic information

Original name

Compositional Verification and Optimization of Interactive Markov Chains

Authors

HERMANNS, Holger (276 Germany), Jan KRČÁL (203 Czech Republic, belonging to the institution) and Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution)

Edition

Heidelberg Dordrecht London New York, CONCUR 2013 - Concurrency Theory - 24th International Conference, p. 364-379, 16 pp. 2013

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00066202

Organization unit

Faculty of Informatics

ISBN

978-3-642-40183-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-40184-8_26

Keywords in English

interactive Markov chains; continuous-time stochstic systems; composition; verification; specification

Abstract

V originále

Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms for compositional verification and optimization of IMC with respect to time-bounded properties. Firstly, we give a specification formalism for IMC. Secondly, given a time-bounded property, an IMC component and the assumption that its unknown environment satisfies a given specification, we synthesize a scheduler for the component optimizing the probability that the property is satisfied in any such environment.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

MUNI/A/0739/2012, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

MUNI/A/0760/2012, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)

Investor: Masaryk University, Category A

Citovat

HERMANNS, Holger, Jan KRČÁL and Jan KŘETÍNSKÝ. Compositional Verification and Optimization of Interactive Markov Chains. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, p. 364-379. ISBN 978-3-642-40183-1. Available from: https://dx.doi.org/10.1007/978-3-642-40184-8_26.

@inproceedings{1112167,
   author = {Hermanns, Holger and Krčál, Jan and Křetínský, Jan},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {CONCUR 2013 - Concurrency Theory - 24th International Conference},
   doi = {http://dx.doi.org/10.1007/978-3-642-40184-8_26},
   keywords = {interactive Markov chains; continuous-time stochstic systems; composition; verification; specification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg Dordrecht London New York},
   isbn = {978-3-642-40183-1},
   pages = {364-379},
   publisher = {Springer},
   title = {Compositional Verification and Optimization of Interactive Markov Chains},
   year = {2013}
}

TY  - JOUR
ID  - 1112167
AU  - Hermanns, Holger - Krčál, Jan - Křetínský, Jan
PY  - 2013
TI  - Compositional Verification and Optimization of Interactive Markov Chains
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783642401831
KW  - interactive Markov chains
KW  - continuous-time stochstic systems
KW  - composition
KW  - verification
KW  - specification
N2  - Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms for compositional verification and optimization of IMC with respect to time-bounded properties. Firstly, we give a specification formalism for IMC. Secondly, given a time-bounded property, an IMC component and the assumption that its unknown environment satisfies a given specification, we synthesize a scheduler for the component optimizing the probability that the property is satisfied in any such environment.
ER  -

HERMANNS, Holger, Jan KRČÁL and Jan KŘETÍNSKÝ. Compositional Verification and Optimization of Interactive Markov Chains. In \textit{CONCUR 2013 - Concurrency Theory - 24th International Conference}. Heidelberg Dordrecht London New York: Springer, 2013, p.~364-379. ISBN~978-3-642-40183-1. Available from: https://dx.doi.org/10.1007/978-3-642-40184-8\_{}26.

Detailed Information on Publication Record