What would you suggest for someone who is interested both in Coq (formal proofs and maybe even formally verified software) and statistics? A topic for bachelor thesis, it is.
Thanks in advance!
one interesting intersection between formal proofs, logic, and statistics is statistical model checking
if someone wants to do this in Coq I would probably recommend using the Infotheo library, since for basics only discrete random variables are needed
so a bachelor thesis topic might be to formalize a logic like PCTL (or adapt someone else's formalization of a similar logic) and write a verified procedure for probabilistic verification of PCTL formulas using traces assumed to be randomly sampled - e.g., Wald's SPRT or something even simpler
Karl Palmskog said:
if someone wants to do this in Coq I would probably recommend using the Infotheo library, since for basics only discrete random variables are needed
If one wants to use continuous random variables, they has to make a library for that, right?
Another possibility is the FormalML library, available at https://github.com/IBM/FormalML
We plan on making an announcement about it in the next day or so. It includes general probability (including over continuous random variables), and provides tools for working with Expectations, ConditionalExpectations (over general random variables, not just discrete ones), some martingale theory, and more.
@Avi Shinnar nice, please consider submitting a package for the library to the Coq opam archive for easier reuse: https://github.com/coq/opam-coq-archive/ (recommended name for package: coq-formal-ml
)
Had a chat with potential supervisor (?) of bachelor's thesis. :) Now my task is to prepare some presentation which motivates SMC - why it is necessary and how it was created, what it achieves, few practical examples, how good it is (compared to other methods)...
So, I will ask questions here but I will try not to spam too much. Is it okay?
@Lessness sure, go ahead
the survey I linked has quite a lot of the answers to those questions, though. The main reason for SMC is scaling better than other verification methods with the size of the random process state space
I can give a direct link to the survey PDF in private message if you want
this paper cited in the survey compares SMC performance against numerical methods and explains the case in more detail (but a bit out of date now): https://www.prismmodelchecker.org/papers/sttt_stat.pdf
I'm still thinking about this etc., I just have exams, tests, homeworks and work too to do. A bit busy right now... So I will post random brain bits here rarely, until I get more time. :|
I was reading the https://dl.acm.org/doi/pdf/10.1007/BF01211866 and there is my attempt to formalize syntax of PCTL formulas.
Require Import Reals.
Open Scope R.
Module PCTL.
Variable A: Type. (* A should be finite, right? *)
Variable atom: A -> Prop.
Definition probability := { p: R | 0 <= p <= 1 }.
Inductive formula :=
| atomic: A -> formula
| negation: formula -> formula
| conjunction: formula -> formula -> formula
| until_finite: formula -> formula -> nat -> probability -> formula
| until_infinite: formula -> formula -> probability -> formula
| until_strong_finite: formula -> formula -> nat -> probability -> formula
| until_strong_infinite: formula -> formula -> probability -> formula.
End PCTL.
Print PCTL.formula.
But I don't get what's the difference between "until" operator and "strong until" operator... isn't it the same thing because for continuous probabilities <= and < are the same?
what you call until and strong until are not the same, since they are different at the purely logical level (e.g., when you set probability bound to 1, ). See for example "until" vs. "weak until" here: https://en.wikipedia.org/wiki/Computation_tree_logic#Operators
the idea with PCTL is that it is compatible with regular CTL at the edges of the probability range, so it's a good idea to understand (and possibly encode in Coq) regular CTL first to get a better understanding of meanings of operators.
Thank you!
here's one encoding of CTL (not saying it's a simple one, but maybe useful): https://github.com/coq-community/comp-dec-modal/blob/master/theories/CTL/CTL_def.v
Last updated: Dec 05 2023 at 06:01 UTC