Task-Structured Probabilistic I/O Automata
Modeling frameworks such as Probabilistic I/O Automata (PIOA) andMarkov Decision Processes permit both probabilistic andnondeterministic choices. In order to use such frameworks to express claims about probabilities of events, one needs mechanisms for resolving nondeterministic choices. For PIOAs,...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2006
|
| Online Access: | http://hdl.handle.net/1721.1/33964 |
| _version_ | 1811095840444383232 |
|---|---|
| author | Canetti,, Ran Cheung,, Ling Kaynar,, Dilsun Liskov,, Moses Lynch,, Nancy Pereira,, Olivier Segala, Roberto |
| author2 | Nancy Lynch |
| author_facet | Nancy Lynch Canetti,, Ran Cheung,, Ling Kaynar,, Dilsun Liskov,, Moses Lynch,, Nancy Pereira,, Olivier Segala, Roberto |
| author_sort | Canetti,, Ran |
| collection | MIT |
| description | Modeling frameworks such as Probabilistic I/O Automata (PIOA) andMarkov Decision Processes permit both probabilistic andnondeterministic choices. In order to use such 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, such schedulers are too powerful for certain settings, such as cryptographic protocol analysis, where information must sometimes be hidden. Here, we propose a new, less powerful nondeterminism-resolutionmechanism for PIOAs, consisting of tasks and local schedulers.Tasks are equivalence classes of system actions that are scheduled byoblivious, 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, and supports simple compositionality results.We also define a new kind of simulation relation, and show it to besound for proving implementation. We illustrate the potential of the task-PIOA framework by outlining its use in verifying an Oblivious Transfer protocol. |
| first_indexed | 2024-09-23T16:30:21Z |
| id | mit-1721.1/33964 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:30:21Z |
| publishDate | 2006 |
| record_format | dspace |
| spelling | mit-1721.1/339642019-04-12T08:35:55Z Task-Structured Probabilistic I/O Automata Canetti,, Ran Cheung,, Ling Kaynar,, Dilsun Liskov,, Moses Lynch,, Nancy Pereira,, Olivier Segala, Roberto Nancy Lynch Theory of Computation Modeling frameworks such as Probabilistic I/O Automata (PIOA) andMarkov Decision Processes permit both probabilistic andnondeterministic choices. In order to use such 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, such schedulers are too powerful for certain settings, such as cryptographic protocol analysis, where information must sometimes be hidden. Here, we propose a new, less powerful nondeterminism-resolutionmechanism for PIOAs, consisting of tasks and local schedulers.Tasks are equivalence classes of system actions that are scheduled byoblivious, 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, and supports simple compositionality results.We also define a new kind of simulation relation, and show it to besound for proving implementation. We illustrate the potential of the task-PIOA framework by outlining its use in verifying an Oblivious Transfer protocol. 2006-09-07T20:14:22Z 2006-09-07T20:14:22Z 2006-09-05 MIT-CSAIL-TR-2006-060 http://hdl.handle.net/1721.1/33964 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory http://hdl.handle.net/1721.1/32525 http://hdl.handle.net/1721.1/32525 34 p. 2343188 bytes 369503 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Canetti,, Ran Cheung,, Ling Kaynar,, Dilsun Liskov,, Moses Lynch,, Nancy Pereira,, Olivier Segala, Roberto Task-Structured Probabilistic I/O Automata |
| title | Task-Structured Probabilistic I/O Automata |
| title_full | Task-Structured Probabilistic I/O Automata |
| title_fullStr | Task-Structured Probabilistic I/O Automata |
| title_full_unstemmed | Task-Structured Probabilistic I/O Automata |
| title_short | Task-Structured Probabilistic I/O Automata |
| title_sort | task structured probabilistic i o automata |
| url | http://hdl.handle.net/1721.1/33964 |
| work_keys_str_mv | AT canettiran taskstructuredprobabilisticioautomata AT cheungling taskstructuredprobabilisticioautomata AT kaynardilsun taskstructuredprobabilisticioautomata AT liskovmoses taskstructuredprobabilisticioautomata AT lynchnancy taskstructuredprobabilisticioautomata AT pereiraolivier taskstructuredprobabilisticioautomata AT segalaroberto taskstructuredprobabilisticioautomata |