Possible extensions:

[xhajnal]

This file summarises what has been done in our project (DiPS and Bees) and will be done in the foreseeable future. If you are aware of something missing or something which is worth to look at, please comment.

GENERAL FEATURES

Related Work

• parameter synthesis by the formal methods - see github mcss_papers
• other related work - see drive
  • Experimentally induced innovations lead to persistent culture via conformity in wild birds
  • Probabilistic Programming Process Algebra
  • Distributed Information Processing in Biological and Computational Systems
  • others???

Models

• pMCs
  • PRISM format
• pMDP
  • PRISM format
  • check on more models
• state-space reduction #small_project
  • use bisimulation minimisation, see Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2010)

Properties

• PCTL

Rational functions

• Obtaining the polynomials

  • PRISM
    • wrapper + parser (syntax error, ... , prop-by-prop , Java-heap memory)
  • Storm
    • wrapper + parser
    • how to call in Docker if Storm not installed

Data

• list observed values (probability or reward) for the respective property
• data weights
• generate observations from the data for MH

(Confidence) Intervals

• CI intervals #small_project
  • CLT / Wald / standard
  • Agresti-Coull
  • Wilson
  • Jefrreys
  • Clopper Pearson
  • Rule of Three
• intervals for moments #small_project look here

Constraints

• conjunction of domains and (functions in intervals)
• create constraints from intervals
• decouple constraints made from intervals for space refinement -- see z3 is not able to deal with 2 <,>,<=, >=, = in a single constraint #80

Visualisation

• for more details see add more visualisations #11 #small_project

Methods

• Optimization / Regression
  • Optimization (local min distance)
  • multiple optimisation methods, pick the best
  • weighted optimisation
• Space Sampling
  • grid sampling
  • 1D, 2D visualisation - see add more visualisations #11
  • multidim visualisation - see add more visualisations #11
• Quantitative Sampling
  • grid sampling
  • 1D, 2D visualisation - see add more visualisations #11
  • multidim visualisation - see add more visualisations #11
• Space Refinement
  • 2D visualisation - see add more visualisations #11
  • multidim visualisation - see add more visualisations #11
  • try different solvers
    • z3
    • dreal
    • NUSMV #small_project
  • interval arithmetics -- see 10170e8
  • presampled refinement -- see aa1f195
  • ❌ iterative method - see Refinement - Implement iterative approach with ordering of properties #2 - NOT_NOW
• Sampling-guided Space Refinement
  • split rectangle by sampling
    • in all dimensions
    • find_max_rect(point) for point in samples
  • z3, dreal, interval. arit.
• Metropolis-Hastings
  • wire up Tanja`s code
  • optimise (evaluation of )
  • 2D visualisation - see add more visualisations #11
  • multidim visualisation - see add more visualisations #11
  • run MH from the previous one, using previous posterior as prior
  • multiple independent runs
    - [ ] estimate convergence - necessary number of iterations #small_project
  • estimate burn-in period #small_project
    • I havent found any general rule, these papers try to estimate it [TBA] [TBA] and this is against any burn-in [TBA]
  • covariance estimator to set thinning #small_project
  • ❔ consult prior estimator @tatjanapetrov @xsafran1
  • ❔ consult prior estimator - I see only first two params there @tatjanapetrov @xsafran1
  • ❔ consult walker - sd=0.3 (In the walker, there is the standard deviation of 0.3 in the code, which was fine when we had params from [0,1] but in the sigmoidal model and in general, the sd should maybe look like old_point_value * sd (vector multiplication)) @tatjanapetrov @xsafran1
• MHMH (Metropolis-Hastings guided refinement)
  • propose method
  • implement method
• multithreading computation / parallelisation (in process) #small_project
  • parametric model checking
  • sampling
    • pool.map
  • refinement
    • pool.map
    • asyn 3 queues
  • ❌ Metropolis-Hastings (hard)
  • MHMH
    • pool.map
  • gui - see GUI - do computations in a separate thread/process #33
• identifiability of parameters #small_project
• Combining the methods
  • regression + sampling #small_project
    • sample regression point #small_project
  • regression + MH #small_project
    • start in the regression point #small_project
  • sampling + refinement #small_project
    • presampling of the space before splitting -- see Presampled refinement- how to merge possibly (un)safe (hyper)rectangles #21 Presampled refinement - iterating thought presampled space of unknown dimension #22 (in progress)
      sampling
      • uniform sampling
      • using orthogonal hull
  • MCMC/MH + refinement #small_project
    • refine the space based on some of MH bins

Tool/GUI

• Features

  • load, edit, save model
  • load, edit, save properties
  • call PRISM, parse the output
  • call Storm, parse the output
  • factorise, load, save the functions
  • sample functions
    • Grid sampling
    • selected point
    • heatmap (2D)
  • load (.p/csv) and save data
  • show data
  • load, compute, save data intervals
  • compute, load, save, append constraints
  • show rat. functions (with data (with data intervals))
  • Space Sampling
    • possible imporovements
  • Space Refinement
    • possible imporovements
  • Quantitative Space Sampling
    • possible imporovements
  • config file
  • Model selection #small_project

• User testing #small_project discuss with @tatjanapetrov

  answer design, layout, readability, and also to query possible new features, potentially suggested by biologists.
  • 1 Design user testing
  • 2 set minimal number of participants
  • 3 ask people
  • 4 conduct test
  • 5 evaluate results

Notebooks

• Features
  • create models
  • sample functions
  • etc.

CASE STUDY - BEE PROJECT #small_project

see Gdrive and Git

Models

• Models by recursive functions

  • obtain recursive functions for rational functions for new bee models
    • synchronous model: see github mcss_papers/Tatjana_draft
    • ❌ semisynchronous model - NOT_NOW
    • ❌ asynchronous model - NOT_NOW

• Models by composition

  we adapted Sokolova SCCS composition with PMDPs: see github mcss_papers/Tatjana_draft

  • define generic single agent
  • draw general generic single agent
  • draw generic single agent for two bees
  • define population abstraction
  • define synchronous parallel composition of generic single agents
  • 2 bees
    • draw synchronous parallel composition of 2 generic single agents.
    • draw synchronous parallel composition of 2 generic single agents.
    • draw population abstraction of synchronous parallel composition of 2 generic single agents.
  • 3 bees
    • draw synchronous parallel composition of 3 generic single agents.
    • ❌ draw synchronous parallel composition of 3 generic single agents. - NOT NOW (probably too large)
    • draw population abstraction of synchronous parallel composition of 3 generic single agents.
  • ❌ semisynchronous model - NOT_NOW
  • ❌ asynchronous model - NOT_NOW
  • add references to the papers on composition in the related work

• PRISM Models (DTMCs) see Gdrive, and Git

  • HSB models
    • old [hsb19] 2-param (p, q) (syn|syn, syn|asyn, asyn|asyn)
    • old [hsb19] mutliparam (p, q₀, q₁, .... , q_n-1) (syn|syn, syn|asyn, asyn|asyn)
  • NEW MODEL
    • new model (r₀, r₁, .... , r_n-1) (syn|syn)
    • new model (r₀, r₁, .... , r_n-1) (syn|asyn)
      • design
      • generator (not optimised)
        - [ ] optimise
    • new model (r₀, r₁, .... , r_n-1) (asyn|asyn)
      • design
      • generator
  • DIFFERENT MODEL
    • 🆕 asyn, superfast spread of pheromone model (see paper drawings)
      • design
      • generator

Properties

• P=?(FG BSCCi)
  • Generate properties

Rational functions

• Obtaining the polynomials
  • parse PRISM/Storm, results @ Gdrive
    • new models syn up to 20
  • formula: recursive function
    • bee synchronous
• model selection
  • CHECK SECOND FACTORISATION of functions
  • linear model
  • ❔ sigmoidal model: which to run first:
    • ❔ sigmoidal 2-param model
      • (Km, n): r_i = 1 / (1 + (Km / (i+1))^n)
      • other option
    • ❔ sigmoidal 3-param model
    • (r_0, Km, n)
    • (Vmax, Km, n) with fixed r_0
      - [ ] how to fix r_0
    • ❔ sigmoidal 4-param model
      • (Vmax, r_0, Km, n)

Data

• generator of synthetic data
• obtains the real data
  • normal bees: 2,3,5,10
  • aggressive bees: 2,3,5,7,10,15
• generate observations from data (histogram)
• besmart the data
  • 4 ways how to do it
    • multinomial [DEFAULT] (counting all outcomes)
    • ❌ binomial (counting for 2 bins)
    • bins
      • no shuffling vs shuffling
        - [x] no shuffling
      • generate 4bins of functions (done from functions)
      • generate 4bins data
      • CHECK SECOND FACTORISATION of functions
    • ❌ quantiles
    • ❌ neglect small outcomes/bins
    • moments
      • CHECK SECOND FACTORISATION of functions
      • ❔ pick weighted vs. unweighted @tatjanapetrov @xsafran1
      • generate moments of functions (done from functions)
      • generate moments from data
      • ❔ formula for CI of higher moments @tatjanapetrov @xsafran1
      • ❔ set number of moments to be used for each population @tatjanapetrov @xsafran1
  • ❔ discuss why we use data encoding only for sig and lin model @tatjanapetrov @xsafran1

(Confidence) Intervals

• ❔ which formula (margin) we should use? @tatjanapetrov @xsafran1
  • so far done with the margin: (st.norm.ppf(1 - (1 - confidence) / 2) * math.sqrt(data_point * (1 - data_point) / n_samples) + 0.5 / n_samples)
  • another alterative is to skip the + 0.5 / n_samples
• ❔ confidence level = 0.9 for intervals @xsafran1
  - Tanja: so far yes

Constraints

• obtain constraints - BLOCKED BY THE INTERVALS

Methods

• Develop non-decreasing constrainst on parameters
  • regression, MH
• Refinement
  • ❔ what is the timeout/coverage vs. the best results we simply have @tatjanapetrov @xsafran1
    • best results we have regardless of time and coverage (to be verified by looking)
    • fix coverage
    • [ ] fix depth
    • fix time
• MH
  • ❔ burn-in 25% (keep last 75%) @xsafran1
    • Tanja: LOOK in the literature
      • I haven't found any general rule, these papers try to estimate it [TBA] [TBA] and this is against any burn-in [TBA]
  • ❔ how many iterations to have vs. the best results we simply have @tatjanapetrov @xsafran1
    • best results we have regardless of time and iterations (to be verified by looking)
    • fix the number of iterations
    • fix time

Analysis

• ❔ use only synchronous models? Morgane says yes
  • Tanja: so far yes
• Rerun sigmoidal models
• ❔ 4 baskets - observability of subset of params [when double factorised] @tatjanapetrov @xsafran1