Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice

J.I. den Hartog; E.P. de Vink; J.W. de Bakker

doi:10.1016/S1571-0661(05)80038-6

Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice

J.I. den Hartog, E.P. de Vink, J.W. de Bakker

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

13 Citations (Scopus)

78 Downloads (Pure)

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.

Original language	English
Title of host publication	MFCSIT2000
Subtitle of host publication	The First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology
Editors	Ted Hurley, Michel Schellekens, Anthony Seda, M. Mac an Airchinnigh
Publisher	Elsevier
Pages	72-99
Number of pages	28
DOIs	https://doi.org/10.1016/S1571-0661(05)80038-6
Publication status	Published - Mar 2001
Event	1st Irish Conference on the Mathematical Foundations of Computer Science and Information, MFCSIT 2000 - Cork, Ireland Duration: 20 Jul 2000 → 21 Jan 2006 Conference number: 1

Publication series

Name	Electronic Notes in Theoretical Computer Science
Publisher	Elsevier
Volume	40

Conference

Conference	1st Irish Conference on the Mathematical Foundations of Computer Science and Information, MFCSIT 2000
Abbreviated title	MFCSIT
Country/Territory	Ireland
City	Cork
Period	20/07/00 → 21/01/06

Access to Document

10.1016/S1571-0661(05)80038-6Licence: CC BY-NC-ND

DenHartog2001metricFinal published version, 283 KBLicence: CC BY-NC-ND

Cite this

den Hartog, J. I., de Vink, E. P., & de Bakker, J. W. (2001). Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice. In T. Hurley, M. Schellekens, A. Seda, & M. Mac an Airchinnigh (Eds.), MFCSIT2000: The First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (pp. 72-99). (Electronic Notes in Theoretical Computer Science; Vol. 40). Elsevier. https://doi.org/10.1016/S1571-0661(05)80038-6

den Hartog, J.I. ; de Vink, E.P. ; de Bakker, J.W. / Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice. MFCSIT2000: The First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology. editor / Ted Hurley ; Michel Schellekens ; Anthony Seda ; M. Mac an Airchinnigh. Elsevier, 2001. pp. 72-99 (Electronic Notes in Theoretical Computer Science).

@inproceedings{2bddc3e68aa542dd9ec5029ae4a6a333,

title = "Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice",

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.",

author = "{den Hartog}, J.I. and {de Vink}, E.P. and {de Bakker}, J.W.",

year = "2001",

month = mar,

doi = "10.1016/S1571-0661(05)80038-6",

language = "English",

series = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

pages = "72--99",

editor = "Ted Hurley and Michel Schellekens and Anthony Seda and {Mac an Airchinnigh}, M.",

booktitle = "MFCSIT2000",

note = "1st Irish Conference on the Mathematical Foundations of Computer Science and Information, MFCSIT 2000, MFCSIT ; Conference date: 20-07-2000 Through 21-01-2006",

}

den Hartog, JI, de Vink, EP & de Bakker, JW 2001, Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice. in T Hurley, M Schellekens, A Seda & M Mac an Airchinnigh (eds), MFCSIT2000: The First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology. Electronic Notes in Theoretical Computer Science, vol. 40, Elsevier, pp. 72-99, 1st Irish Conference on the Mathematical Foundations of Computer Science and Information, MFCSIT 2000, Cork, Ireland, 20/07/00. https://doi.org/10.1016/S1571-0661(05)80038-6

Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice. / den Hartog, J.I.; de Vink, E.P.; de Bakker, J.W.
MFCSIT2000: The First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology. ed. / Ted Hurley; Michel Schellekens; Anthony Seda; M. Mac an Airchinnigh. Elsevier, 2001. p. 72-99 (Electronic Notes in Theoretical Computer Science; Vol. 40).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice

AU - den Hartog, J.I.

AU - de Vink, E.P.

AU - de Bakker, J.W.

N1 - Conference code: 1

PY - 2001/3

Y1 - 2001/3

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

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

U2 - 10.1016/S1571-0661(05)80038-6

DO - 10.1016/S1571-0661(05)80038-6

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 72

EP - 99

BT - MFCSIT2000

A2 - Hurley, Ted

A2 - Schellekens, Michel

A2 - Seda, Anthony

A2 - Mac an Airchinnigh, M.

PB - Elsevier

T2 - 1st Irish Conference on the Mathematical Foundations of Computer Science and Information, MFCSIT 2000

Y2 - 20 July 2000 through 21 January 2006

ER -

den Hartog JI, de Vink EP, de Bakker JW. Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice. In Hurley T, Schellekens M, Seda A, Mac an Airchinnigh M, editors, MFCSIT2000: The First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology. Elsevier. 2001. p. 72-99. (Electronic Notes in Theoretical Computer Science). doi: 10.1016/S1571-0661(05)80038-6

Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this