SMC for incomplete models

We have uploaded a new experimental version (1.4.5) of Plasma Lab.
It includes new plugins for analyzing incomplete models (with unknowns):

  • The plugins work with normal RML models that have atomic propositions that may take three values (1 for True, 0 for False, and -1 for Unknown).
  • A new BLTLU plugin allows to check three-valued BLTL properties (same syntax as BLTL).
  • A new Monte-Carlo estimation algorithm for models with unknown.
  • A new hypothesis testing algorithm for models with unknown.
  • The demo examples include an example of an incomplete network model.

Comments are closed.