Other formats:
BibTeX
LaTeX
RIS
@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.
|
