TheĀ modularĀ architecture of Mudi is separated into two distinct layers:
  • The inference engine layer: Responsible for the evaluation of individual Probabilistic Bounded Linear Spatial Temporal Logic (PBLSTL) statements.
  • The model checking layer: Responsible for deciding if the model is valid using the algorithm chosen by the user.




One of the main advantages of this architecture is that Mudi can be easily extended with further approximate probabilistic model checking types without needing to update the inference engine layer code. Conversely any change at the inference engine level does not require updating the model checking layer as well.