Schedulers are no Prophets

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088807" target="_blank" >RIV/00216224:14330/16:00088807 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-27810-0_11" target="_blank" >http://dx.doi.org/10.1007/978-3-319-27810-0_11</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-27810-0_11" target="_blank" >10.1007/978-3-319-27810-0_11</a>

Result language
angličtina
Original language name
Schedulers are no Prophets
Original language description
Several formalisms for concurrent computation have been proposed in recent years that incorporate means to express stochastic continuous-time dynamics and non-determinism. In this setting, some obscure phenomena are known to exist, related to the fact that schedulers may yield too pessimistic verification results, since current non-determinism can surprisingly be resolved based on prophesying the timing of future random events. This paper provides a thorough investigation of the problem, and it presents a solution: Based on a novel semantics of stochastic automata, we identify the class of schedulers strictly unable to prophesy, and show a path towards verification algorithms with respect to that class. The latter uses an encoding into the model of stochastic timed automata under arbitrary schedulers, for which model checking tool support has recently become available.
Czech name
—
Czech description
—

Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)