One of the goals of Domain Driven Design is attempt to construct an UbiquitousLanguage that thoroughly describes a system.

By using a Petri-Net as a mental model during an Event Storming session contributors can document event designs using a specification that is both verifiable and executable.

Here we describe a technique for directly applying Petri-Net Markup Language (PNML) as an executable specification for domain events, but first we will briefly introduce some of the principles at play.

- In simple terms an algorithm is computable if a person can sit down with pencil and paper to solve the problem
- That is to say there exists a general method of defining and attacking the problem.

Petri-Nets are known to be a good method of defining a 'concurrency-based model' of computation.

Wielding PNML as a formal specification for a domain model lets us build systems that has have verifiable runtime output.

Simply put: the aim of this technique is to name PNML elements: 'states' and 'transitions' -- in a way that creates a Ubiquitous Language that describes domain events.

Any Petri-Net can be convertible into a vector addition system (with state) VASS.

This vector system is useful as a state-machine API whereby we can validate events flowing through the system.

Additionally, using PNML in this manner constricts the degrees of freedom we use to construct a language,
because of this limitation we can assure that the constructed language is a *Regular Language* that is not Turing complete.

Kleene's theorem illustrates how Regular Languages and State Machines are two sides of the same coin.

```
A [regular language](https://en.wikipedia.org/wiki/Regular_language)
can be defined as a language recognized by a finite automaton.
```

Another way of describing this technique is:

- PNML serves as an action language for
- defining a formal state-transition system
- that resulting system and provides a method to express that logic as a finite automaton

This technique complements Domain Driven Design principles and further refines the practice of event-storming into a formal method.

Using PNML defined algorithms as state machines allows for localized actors to draw very concise context boundaries around event handlers.

Furthermore, by reducing the 'statefullness' of an application to mere vector addition, we can construct large systems that are easier to understand and validate.

See example languages describing fizz-buzz & a game Tic-Tac-Toe: Using Petri-Nets to construct a language