Where academic tradition
meets the exciting future

Algebraic Reasoning for Probabilistic Action Systems and While-Loops

Larissa Meinicke, Ian J. Hayes, Algebraic Reasoning for Probabilistic Action Systems and While-Loops. Acta Informatica 45(5), 321–382, 2008.

Abstract:

Back and von Wright have developed algebraic laws for reason- ing
about loops in a total correctness framework using the refinement
cal- culus. 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 and probabilistic while- loops. In
particular we focus on developing data refinement rules for these
two constructs. Our extension is interesting since some well
known transfor- mation 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.

BibTeX entry:

@ARTICLE{jMeHa08a,
  title = {Algebraic Reasoning for Probabilistic Action Systems and While-Loops},
  author = {Meinicke, Larissa and Hayes, Ian J.},
  journal = {Acta Informatica},
  volume = {45},
  number = {5},
  pages = {321–382},
  year = {2008},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 2

Edit publication