Schedulers are no Prophets
| Autor: | Holger Hermanns, Arnd Hartmanns, Jan Krčál |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Class (computer programming) Semantics (computer science) Computer science METIS-317202 Distributed computing 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences Rotation formalisms in three dimensions Automaton 010201 computation theory & mathematics Encoding (memory) Path (graph theory) IR-100653 0202 electrical engineering electronic engineering information engineering EWI-27014 EC Grant Agreement nr.: FP7/318490 Stochastic automata EC Grant Agreement nr.: FP7/295261 |
| Zdroj: | Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, 214-235 STARTPAGE=214;ENDPAGE=235;TITLE=Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays Semantics, Logics, and Calculi ISBN: 9783319278094 Semantics, Logics, and Calculi |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-319-27810-0_11 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|