Details

Autor(en) / Beteiligte

• Canetti, Ran
• Cheung, Ling
• Kaynar, Dilsun
• Liskov, Moses
• Lynch, Nancy
• Pereira, Olivier
• Segala, Roberto

Titel

Task-structured probabilistic I/O automata

Ist Teil von

• Journal of computer and system sciences, 2018-06, Vol.94, p.63-97

Ort / Verlag

Elsevier Inc

Erscheinungsjahr

2018

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Modeling frameworks such as Probabilistic I/O Automata (PIOA) and Markov Decision Processes permit both probabilistic and nondeterministic choices. In order to use these frameworks to express claims about probabilities of events, one needs mechanisms for resolving nondeterministic choices. For PIOAs, nondeterministic choices have traditionally been resolved by schedulers that have perfect information about the past execution. However, these schedulers are too powerful for certain settings, such as cryptographic protocol analysis, where information must sometimes be hidden. In this paper, we propose a new, less powerful nondeterminism-resolution mechanism for PIOAs, consisting of tasks and local schedulers. Tasks are equivalence classes of system actions that are scheduled by oblivious, global task sequences. Local schedulers resolve nondeterminism within system components, based on local information only. The resulting task-PIOA framework yields simple notions of external behavior and implementation, a new kind of simulation relation that is sound for proving implementation, and supports simple compositionality results. •Task-PIOAs, a probabilistic modeling framework based on PIOAs.•A nondeterministic resolution mechanism tailored for cryptographic applications.•Notions of external behavior and implementation for task-PIOAs.•A simulation relation for task-PIOAs that is sound for proving implementation.•Composition results for task-PIOAs.