Další formáty:
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 a 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, s.~364-379. ISBN~978-3-642-40183-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-40184-8\_{}26.
|