Hi, in this video I present MOMBA, a flexible Python framework for working with formal models from construction through analysis centered around the JANI model interchange format. I will demonstrate how MOMBA can help you creating, validating and analyzing quantitative models.

So, let's get started! Being based on JANI, MOMBA supports a variety of different model types, from simple label transition systems to stochastic hybrid automata. It supports modeling probabilistic and real-time aspects as well as continuous dynamics. A JANI model is a network of automata with variables interacting via synchronized actions.

The JANI specification defines the semantics of these models together with a JSON-based format to represent them. For the analysis of JANI models, several state-of-the-art tools are available, for instance STORM or the models toolset. Now, MOMBA brings to the table three core features.

First and foremost, it provides an API to import, export, create and to a certain extent modify JANI models. Second, it comes with a built-in state-space exploration engine, which can for instance be used to rapidly prototype an interactive simulation of a model. Third, MOMBA provides unified interfaces with sensible defaults to existing tools such as model checkers.

So, MOMBA really strives to deliver an integrated and intuitive experience throughout the whole process from model construction to analysis. Let's now have a look at a particular example where MOMBA can help. Imagine you would like to model a jump and run game where the player moves forward at

a constant speed from left to right while having to avoid obstacles by moving up or down. The moves of the player are subject to probabilistic noise. That is, not every input action is guaranteed to have an effect on the game and the player may continue straight instead of moving with a certain probability.

Imagine further you have a collection of maps for which you would like to create a respective model. Now, this is where MOMBA comes in. Given a domain-specific description of the scenario to be modeled, in our case a map of the game, MOMBA's modeling API allows you to programmatically create a JANI model with Python.

MOMBA does not aim to compete with general-purpose modeling languages such as MODIS or the PRISM language. Instead, it aims to give you the tools to roll your own domain-specific language or other kind of tailored scenario description. So, with MOMBA, you can harvest the ease of Python and its ecosystem to turn your domain-specific scenario descriptions into a formal model.

Coming back to our example, such a description may be an ASCII-art-like representation of a map the player has to navigate through. I will now give you a brief glimpse on what MOMBA provides to turn such an ASCII-art representation into a formal model.

As a first step, we will pass the ASCII-art representation into a more formal data structure representing a map. We define two classes, cell for representing an individual cell of the map and map for representing the complete map. A cell has an x and a y-coordinate and a map has a width, a height and a set of cells indicating where the obstacles are.

Parsing the ASCII-art representation is achieved by a few lines of Python code providing us with a map object. Having parsed our domain-specific scenario description, it remains to construct the actual model. To this end, we import MOMBA's modeling API, exposing the functionality we need.

The base of every model constructed with MOMBA is a modeling context determining the type of the model. Every modeling context can hold several automata and automata networks comprised of these automata. Also, global variables, functions and properties are declared on the modeling context.

In our case, the model will be a Markov Decision Process or MDP for short, so we create an MDP modeling context. To represent the position of the player, we declare two global variables, posx and posy with an initial value of zero.

JANI supports different types of variables. In this case, both variables are integers. During construction, MOMBA will check the model for validity and type correctness. For instance, it does not allow adding an expression to the model where one subtracts an integer from a boolean. To give the player a way to interact with the game, we define three

action types allowing the player to move up, down or stay at its vertical position. These action types are again defined on the modeling context. At the heart of our model will be an automaton modeling the game logic. We create this automaton and add an initial location name ready to it.

We further add two boolean variables to the automaton indicating whether the player won the game or crashed. Now the idea is to add an edge for each of the action types which probabilistically applies the respective move to the state by updating all the variables accordingly.

To this end, we define two auxiliary functions. The function hasOne takes an expression for an x-coordinate on the map and returns an expression indicating whether the player won when reaching that coordinate. Here we use MOMBA's convenience function xpr for constructing an expression with a concise syntax in a syntax-aware way.

The player won if and only if the x-coordinate is greater than or equal to the width of the track which is captured by this line. Analogously, we define a function taking an expression for the x and the y-coordinate and returning an expression indicating whether the player crashed into a wall or an obstacle.

Here we have to check whether there exists an obstacle at the provided coordinates. Using MOMBA's logicAny function for existential quantification, this expression is easily constructed by iterating over all the obstacles of the map and constructing an expression for each obstacle. To create the edges of the automaton, we again leverage a combination of Python and MOMBA's model construction functionality.

We first define a dictionary mapping the three action types to their respective movement on the y-axis. We then iterate over this dictionary constructing an edge for each action type as follows.

We first construct expressions for the new position of the player under the assumption that the move is successful. We then create an edge starting at the ready location with two probabilistic destinations. The first destination captures the case where the action succeeds and the position of the player is updated accordingly. Here we use the earlier defined functions to construct expressions for updating whether the player won or crashed with that move.

The second destination captures the case where the action of the player has no effect. Here we only update the x-coordinate of the player and use the old y-coordinate to check whether the player won or crashed. We annotate the edge with the respective action type and guard it with an expression true if and only if the player neither won nor crashed.

Finally, in the last step we construct an automaton network from the given automaton. We construct an instance of the game automaton and add it to the network. Using Jarni synchronization vectors, we then specify that the network can take a

respective action if and only if the game automaton can take this action. Leveraging MOMBA, we now have a Python program constructing a formal model of our game based on an ASCII art representation of a map. In the same way, you can use MOMBA to easily construct formal models of all kinds based on whatever domain-specific scenario description or input language you have.

After constructing a model, an important part of applying formal methods in practice is to ensure that the model actually accurately models what should be modeled. To convince ourselves that our model does indeed correspond to the game, we can use MOMBA

to connect it to a testing framework or write an interactive simulation for playing the game. I will now demonstrate how to turn our model into such an interactive game by using MOMBA's explicit state space exploration engine. To use the exploration engine, we provide it with the automaton network we just defined.

In this case, the model is a discrete time model, so we create a discrete time state space explorer. The network has just one initial state, which you obtain via the initial states property of the explorer. We will now write a loop which prints the state of the game on the console and allows the

user to use the arrow keys to select an action until the game is won or the player crashed. To print the state of the game, we use the ASCII graphics Python library, which provides us with a screen to draw on. We first obtain the position of the player by inspecting the global variables and then loop over all the cells of

the map and print a respective character depending on whether the cell is empty, an obstacle, or occupied by the player. If there are no transitions in the present state, the game is finished, and we inform the player about whether she won or crashed by inspecting the local variables of the game automaton.

If there are transitions, we collect them into a dictionary to access them by action label. We then wait for the player to press a key. The player can press Q to quit the game. Depending on which key is pressed, we select a transition based on its action label.

Finally, we obtain the successor state by randomly picking a destination of the respective transition. Now, with just over 60 lines of Python code, we wrote an interactive console game based on the formal model and Mumbai State Space Exploration Engine.

So, let's play! Executing the Python script allows us to interactively explore the model and convince ourselves that this is indeed the game we aim to model. By pressing the arrow keys, we can navigate through the map while trying to avoid obstacles until we win or crash into a wall.

Note that the game is probabilistic, so our actions may not always have an effect. Having validated that our model accurately captures the game, we can now harvest the benefits of formal modeling by invoking analysis tools such as model checkers.

For instance, we may be interested in the maximum probability to win the game on a given track. That is, assuming that the player moves optimal, how certain is it to win the game? As actions are subject to probabilistic noise, winning is not certain on most tracks. To analyze the model and determine this probability, MoMA provides unified interfaces to analysis tools and particular model checkers.

In principle, any tool supporting Jaani or an input language to which Jaani can be translated can be used for analysis. Currently, MoMA provides built-in adapters to Storm and the models toolset.

I will now demonstrate how MoMA can be used to harvest the benefits of formal modeling by invoking these analysis tools. To check a property, we first need to obtain a checker. Here we use Storm and the models toolset. The respective GetChecker functions will try their best to also download and install the respective tools if they are not present.

This enables a quick start especially for beginners. After obtaining instances of the respective model checkers, we define the properties we want to check. In this case, we want to check the maximum probability for winning the game which is captured by the following property.

Again, MoMA has our back by providing the convenience function prop which allows us to define properties with a concise syntax. We also use the function hasOne we defined earlier for our model. Invoking the different model checkers is done by calling the check method with the automaton network and a dictionary of properties we like to check.

In this case, we collect the results for each of the model checkers in a dictionary and then print them to the console. Executing the script will provide us with the probability of winning under the assumption of playing optimally.

In this case, this probability is roughly 0.95. As you have seen, MoMA supports you throughout the whole process from model construction to analysis. It provides an easy-to-use, concise API for constructing models programmatically based on domain-specific scenario descriptions.

It allows you to validate the model by rapid prototyping of an interactive simulation and it also provides unified interfaces to analysis tools. MoMA makes use of Python's optional type hints, hence you can type check your code and get good autocompletion support in most IDEs. MoMA's state-space exploration engine is written in Rust and hence sufficiently fast even for large models.

It supports both discrete-time and continuous-time models. MoMA is open-source and available on GitHub. It supports all three major platforms, Linux, Windows and MacOS. To install in MoMA you can either use pip or a tool for dependency management such as pipenv or poetry.

For a fully reproducible environment I would recommend using pipenv, which pins the dependencies. This makes shipping an artifact or collaborating much easier. As MoMA is written in Python, you have the whole ecosystem of Python right at your fingertips.

In particular this includes Jupyter, a tool developed by the data science community to create reproducible computational workflows. Jupyter enables literate programming and allows you to share your work with the community in the form of interactive notebooks. Furthermore, to document your models and other code you can use Jupyter together with things.

To get an idea how this might look like, let's have a look at MoMA's documentation which combines Jupyter cells with documentation. MoMA's documentation comprises a user guide and an API reference. In the user guide you find the same example revolving around the jump and run game I just presented.

As you can see, we mix code and documentation and this code gets actually executed when the documentation is built. To this end we make use of Jupyter. You can also easily embed links, documenting functions and classes.

For instance, by clicking on context we get to the documentation of the modeling context class. Let me wrap up this video with a short summary. I have demonstrated how MoMA supports you throughout the whole process from model construction to analysis. I have shown how MoMA enables the programmatic construction of formal models based on domain-specific scenario descriptions,

how MoMA's explicit state-space exploration engine can be used to rapidly prototype an interactive simulation, and what MoMA provides to invoke and external tools. With MoMA you get an integrated and intuitive experience to achieve your goals with formal models.