Bao, J;
Docherty, S;
Hsu, J;
Silva, A;
(2021)
A Bunched Logic for Conditional Independence.
In:
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
IEEE
(In press).
Preview |
Text
2008.09231-2.pdf - Accepted Version Download (629kB) | Preview |
Abstract
Independence and conditional independence are fundamental concepts for reasoning about groups of random variables in probabilistic programs. Verification methods for independence are still nascent, and existing methods cannot handle conditional independence. We extend the logic of bunched implications (BI) with a non-commutative conjunction and provide a model based on Markov kernels; conditional independence can be directly captured as a logical formula in this model. Noting that Markov kernels are Kleisli arrows for the distribution monad, we then introduce a second model based on the powerset monad and show how it can capture join dependency, a non-probabilistic analogue of conditional independence from database theory. Finally, we develop a program logic for verifying conditional independence in probabilistic programs.
Type: | Proceedings paper |
---|---|
Title: | A Bunched Logic for Conditional Independence |
Event: | 36th Annual ACM/IEEE Symposium on Logic in Computer Science |
ISBN-13: | 9781665448956 |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1109/LICS52264.2021.9470712 |
Publisher version: | https://doi.org/10.1109/LICS52264.2021.9470712 |
Language: | English |
Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher's terms and conditions. |
UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
URI: | https://discovery.ucl.ac.uk/id/eprint/10134633 |




Archive Staff Only
![]() |
View Item |