Statebox Language Primer

This is an early working version of the Statebox language primer which describes the related mathematical formalisms and capabilities of the language.

The advantages of modelling out a process using Statebox tooling, namely Petri nets, are the following:

Formalisms Used in Statebox

Below is a brief summary of the different mathematical concepts used in the Statebox language, necessary for a thorough understanding of how the language functions.

Petri net

Wikipedia: “A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions (i.e. events that may occur, represented by bars) and places (i.e. conditions, represented by circles). The directed arcs describe which places are pre- and/or postconditions for which transitions (signified by arrows). Some sources[1] state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.”

Statebox has a special “flavor” of Petri nets as described in the monograph. A notable difference is that Statebox nets allow one to mathematically reason about “firing transitions” in a net, as opposed to only static analysis which is typically practiced in the use and study of Petri nets. This is achieved via the use of Category Theory to ensure, amongst other things, compositionality, structure and behaviour of the nets.

Transitions

Transitions in a net are transformations which process resources in the form of tokens living in their input place(s), and turn them into other resources in the form of tokens in their output place(s).

Transitions process tokens as pointed out above by firing. A transition firing carries a net from one state to another. In the context of a Statebox net, a message with the required data and signed by the correct key (corresponding to a user with privileges for a particular role) is processed by the Statebox engine to represent the firing of the corresponding transition, carrying the net from one state to (one of the possible) next ones.

Places

Places can be considered “bags” which denote the type of resource they are holding. Resources of that type are represented as tokens living in that place. For instance, a place of type $A$ holding 3 tokens can be thought of as a bag holding 3 resources of type $A$. Given a place, inbound and outbound edges to/from transitions represent ways to put in/take out tokens from a place.

Tokens

Tokens represent the resources that a net can process. They live in places that denote their type and are transformed into other resources by transitions, which carry them into other places.

State

The state of a net is given by the distribution of its tokens in the various places. Every time a transition fires, moving tokens around, the net is carried to a new state.

Category Theory

Wikipedia: “Category theory formalizes mathematical structure and its concepts in terms of a labeled directed graph called a category, whose nodes are called objects, and whose labelled directed edges are called arrows (or morphisms). A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. The language of category theory has been used to formalize concepts of other high-level abstractions such as sets, rings, and groups.”

The Statebox Language

This section outlines the capabilities of the language, how it ties to the formalisms mentioned in the previous section and how it is implemented.

Implementation Requirements

Once the process is modelled, then in order to implement & run it, we need to further ensure that:

Process Instantiation

The instantiation of a process is achieved by firing a transition against the genesis block which is simply a representation of a given process (as a Petri net). Once the first transition against this genesis block is fired, a new process is created, with a unique ID, pointing back to the genesis block using a hash. The following transitions are fired against the last recorded transaction for that particular net instances which results in a structure similar to a blockchain in that every transaction is a hash of the new state of the net which points to the previous transaction.

Folds

Wikipedia: “In functional programming, fold (also termed reduce, accumulate, aggregate, compress, or inject) refers to a family of higher-order functions that analyze a recursive data structure and through use of a given combining operation, recombine the results of recursively processing its constituent parts, building up a return value.”

Folds in the Statebox system can occur in two ways:

Read only is not a problem, but guarded input is problematic because we cannot have Turing completeness here (or undecidability of checking some property, which is usually the result of having TC or even something much weaker). Simply speaking, we want to be sure that the computation for cheking some property always terminates. This is non-trivial to achieve in the general case.

Bounded Nets

When there is a limit for the number of tokens in one place, the nets are refered to as bounded nets. If the limit is ‘k’ for all places, then the net is called k-bounded. This means that the net has a finite reachability graph.


Subscribe to our email list to stay up to date!