Reasoning about probabilistic sequential programs in a probabilistic logic

Ying, M

Reasoning about probabilistic sequential programs in a probabilistic logic

Ying, M

Permalink

Publication Type:: Journal Article
Citation:: Acta Informatica, 2003, 39 (5), pp. 315 - 389
Issue Date:: 2003-05-01

Closed Access

	Filename	Description	Size
	2008004833OK.pdf		455.72 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.date.issued	2003-05-01	en_US
dc.identifier.citation	Acta Informatica, 2003, 39 (5), pp. 315 - 389	en_US
dc.identifier.issn	0001-5903	en_US
dc.identifier.uri	http://hdl.handle.net/10453/8911
dc.description.abstract	We introduce a notion of strong monotonicity of probabilistic predicate transformers. This notion enables us to establish a normal form theorem for monotone probabilistic predicate transformers. Three other healthiness conditions, namely, conjunctivity, disjunctivity and continuity for probabilistic predicate transformers are also examined, and they are linked to strong monotonicity. A notion of probabilistic refinement index is proposed, and it provides us with a continuous strength spectrum of refinement relations which may be used to describe more flexible refinement between probabilistic programs. A notion of probabilistic correctness is introduced too. We give a probabilistic weakest-precondition, choice and game semantics to the contract language, and present a probabilistic generalization of the winning strategy theorem.	en_US
dc.relation.ispartof	Acta Informatica	en_US
dc.relation.isbasedon	10.1007/s00236-003-0113-z	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Reasoning about probabilistic sequential programs in a probabilistic logic	en_US
dc.type	Journal Article
utslib.citation.volume	5	en_US
utslib.citation.volume	39	en_US
utslib.for	0803 Computer Software	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0804 Data Format	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	closed_access
pubs.issue	5	en_US
pubs.publication-status	Published	en_US
pubs.volume	39	en_US

Abstract:

We introduce a notion of strong monotonicity of probabilistic predicate transformers. This notion enables us to establish a normal form theorem for monotone probabilistic predicate transformers. Three other healthiness conditions, namely, conjunctivity, disjunctivity and continuity for probabilistic predicate transformers are also examined, and they are linked to strong monotonicity. A notion of probabilistic refinement index is proposed, and it provides us with a continuous strength spectrum of refinement relations which may be used to describe more flexible refinement between probabilistic programs. A notion of probabilistic correctness is introduced too. We give a probabilistic weakest-precondition, choice and game semantics to the contract language, and present a probabilistic generalization of the winning strategy theorem.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/8911