Reasoning algebraically about probabilistic loops

Larissa Meinicke*, Ian J. Hayes

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

3 Citations (Scopus)

Abstract

Back and von Wright have developed algebraic laws for reasoning about loops in the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems. In particular we focus on developing data refinement rules for probabilistic action systems. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible. In particular, our probabilistic action system data refinement rules are new.

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings
EditorsZhiming Liu, Jifeng He
PublisherSpringer, Springer Nature
Pages380-399
Number of pages20
Volume4260 LNCS
ISBN (Print)3540474609, 9783540474609
Publication statusPublished - 2006
Event8th International Conference on Formal Engineering Methods, ICFEM 2006 - Macao, China
Duration: 1 Nov 20063 Nov 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4260 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other8th International Conference on Formal Engineering Methods, ICFEM 2006
CountryChina
CityMacao
Period1/11/063/11/06

Fingerprint Dive into the research topics of 'Reasoning algebraically about probabilistic loops'. Together they form a unique fingerprint.

Cite this