Attributes | Values |
---|
rdf:type
| |
Description
| - 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.
- 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. (en)
|
Title
| - Compositional Verification and Optimization of Interactive Markov Chains
- Compositional Verification and Optimization of Interactive Markov Chains (en)
|
skos:prefLabel
| - Compositional Verification and Optimization of Interactive Markov Chains
- Compositional Verification and Optimization of Interactive Markov Chains (en)
|
skos:notation
| - RIV/00216224:14330/13:00066202!RIV14-MSM-14330___
|
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| |
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216224:14330/13:00066202
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - interactive Markov chains; continuous-time stochstic systems; composition; verification; specification (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...v/mistoKonaniAkce
| - Heidelberg Dordrecht London New York
|
http://linked.open...i/riv/mistoVydani
| - Heidelberg Dordrecht London New York
|
http://linked.open...i/riv/nazevZdroje
| - CONCUR 2013 - Concurrency Theory - 24th International Conference
|
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...vavai/riv/projekt
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...iv/tvurceVysledku
| - Krčál, Jan
- Křetínský, Jan
- Hermanns, Holger
|
http://linked.open...vavai/riv/typAkce
| |
http://linked.open.../riv/zahajeniAkce
| |
issn
| |
number of pages
| |
http://bibframe.org/vocab/doi
| - 10.1007/978-3-642-40184-8_26
|
http://purl.org/ne...btex#hasPublisher
| |
https://schema.org/isbn
| |
http://localhost/t...ganizacniJednotka
| |