Utilisateur:JP Garcia Ballester
Un article de APMC.
Sommaire |
My current work on APMC
As you surely know, APMC calculates probabilities of LTL formulas. It means you give it a formula φ, a precision parameter ε, a confidence parameter δ, and APMC calculates ρ, an approximation of the probability p of φ being true.
When testing p against a threshold θ, we do not always need a high precision. Indeed, when p is far from θ, the precision required is lower than when p is near θ. We just need to be sure that p is superior or inferior to θ. For example, suppose p is 0.7 and we want to know whether it is superior or inferior to 0.5: if we calculate ρ to be 0.8 with ε equals 0.2, we do not need a more accurate precision.
Therefore, I'm working on an iterative version of APMC which would stop when ε is big enough to take a decision. We know
p > ρ - ε
p < ρ + ε
Therefore, decision can be reach when ρ - ε > θ or ρ + ε < θ.
Here is the algorithm doing this optimization:
Input: diagram, φ, θ, δ, k A := 0 N := 0 R := 0 While R = 0 do Generate a random path σ of length k with the diagram If φ is true on σ then A := A + 1 N := N + 1, ε := sqrt(4log(2/δ)/N), ρ := A / N If ρ - ε > θ then R := 1 If ρ + ε < θ then R := -1
This algorithm has been implemented in the standalone Java version and in the cluster implementation of APMC.
Some unuseful informations about myself
- Who I am: a student in mathematics
- Where I live: somewhere in france
- What I like: unuseful talk and stupid jokes
Some nearly less unuseful informations about myself
- My mail: giga@le-pec.org
- My jabber-id: giga@le-pec.org
- My phone number: (+33) 06 31 78 40 48
