Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice


Share/Save/Bookmark

Hartog den, J.I. and Vink de, E.P. and Bakker de, J.W. (2001) Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice. In: First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2000, 20-21 July 2000, Cork, Ireland.

[img]
Preview
PDF
263Kb
Abstract:This paper provides a case-study in the field of metric semantics for probabilistic programming. Both an operational and a denotational semantics are presented for an abstract process language L_pr, which features action refinement and probabilistic choice. The two models are constructed in the setting of complete ultrametric spaces, here based on probability measures of compact support over sequences of actions. It is shown that the standard toolkit for metric semantics works well in the probabilistic context of L_pr, e.g. in establishing the correctness of the denotational semantics with respect to the operational one. In addition, it is shown how the method of proving full abstraction --as proposed recently by the authors for a nondeterministic language with action refinement-- can be adapted to deal with the probabilistic language L_pr as well.
Item Type:Conference or Workshop Item
Copyright:© 2001 Elsevier Science
Link to this item:http://purl.utwente.nl/publications/56322
Official URL:http://dx.doi.org/10.1016/S1571-0661(05)80038-6
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page