Schedulers are no Prophets

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Schedulers are no Prophets

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Schedulers are no Prophets

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

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

Název statě ve sborníku

Semantics, Logics, and Calculi

ISBN

9783319278094

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

22

Strana od-do

214-235

Název nakladatele

Springer International Publishing

Místo vydání

Berlin

Místo konání akce

Berlin

Datum konání akce

1. 1. 2016

Typ akce podle státní příslušnosti

CST - Celostátní akce

Kód UT WoS článku

000381922800011