A theory of slicing for probabilistic control flow graphs

DOI10.1007/978-3-662-49630-5_11zbMATH Open1475.68074arXiv1711.02246OpenAlexW2468557771MaRDI QIDQ2811339FDOQ2811339

Torben Amtoft, Anindya Banerjee

Publication date: 10 June 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: We present a theory for slicing probabilistic imperative programs -- containing random assignments, and ``observe statements (for conditioning) -- represented as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc to the probabilistic setting. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy; next we prove that any such slice is semantically correct; finally we give an algorithm to compute the least slice. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always. A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. This leads directly to a proof of correctness of probabilistic slicing. In a companion article we show adequacy of the semantics of pCFGs with respect to the standard semantics of structured probabilistic programs.

Full work available at URL: https://arxiv.org/abs/1711.02246

Recommendations

• Program Slicing
• Assertion-based slicing and slice graphs
• On slicing of programs with input statements
• On probabilistic techniques for data flow analysis
• Understanding probabilistic programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Labelled Markov processes.
• Semantics of probabilistic programs
• Program Slicing
• A unifying theory of control dependence and its application to arbitrary program structures
• Slicing for modern program structures: a theory for eliminating irrelevant loops
• A Theory of Slicing for Probabilistic Control Flow Graphs

Cited In (2)

• Efficient computation of arbitrary control dependencies
• A Theory of Slicing for Probabilistic Control Flow Graphs

This page was built for publication: A theory of slicing for probabilistic control flow graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811339)