stackdump

Things I learned while programming as a Petri-net maximalist.

(Verse 1) Back in '39, a young genius did find, A way to chart processes, leaving none behind. Carl Petri, just thirteen, with a vision so keen, Mapped out the flow of systems, a mathematical dream.

(Chorus) Dancing through the nets, where tokens freely roam, In places and transitions, they find their way home. A bipartite graph, so elegantly composed, Petri nets, where complexity is neatly enclosed.

(Verse 2) From chemistry to computing, his idea took flight, A universal language, turning complexity to light. Arcs and places, transitions in between, A ballet of tokens, in a machine's serene dream.

(Bridge) Non-deterministic, yet so precise, Modeling concurrency, cutting through like a knife. Enabled transitions, a firing sequence so bright, Petri nets illuminate, the theoretical night.

(Verse 3) With every token's journey, a story unfolds, A dance of possibilities, as the future holds. From discrete events to continuous flow, Petri nets capture dynamics, as they go.

(Chorus) Dancing through the nets, where tokens freely roam, In places and transitions, they find their way home. A graphical notation, for processes so wide, Petri nets, our faithful guide, with Carl by our side.

(Outro) So here's to Carl Petri, and his brilliant insight, A mathematical model, to bring complexity to light. Through places and transitions, our systems we compose, With Petri nets, the path of clarity brightly glows.

1. Workflow Model

Definition: The Workflow model represents the structured sequence of processes or activities aimed at accomplishing a specific task or goal. It defines the flow of tasks, decisions, and information in organizational processes or systems.

Core Components:

  • Activities: Discrete tasks or operations within the workflow.
  • Transitions: The movement or progression from one activity to another.
  • Actors: Entities (either human or automated) responsible for performing the activities.
  • Data: Information that flows through the workflow, being input, manipulated, or output by activities.
  • Triggers: Events or conditions that initiate or influence the flow of activities.

Usage Context: Used in business process management, software development, and automation systems to streamline and optimize processes.

2. Petri-Net Model

Definition: A Petri-net is a mathematical modeling language used for the description and analysis of systems characterized by concurrency, parallelism, synchronization, and nondeterminism. It extends beyond simple workflow models by providing a graphical and mathematical representation of distributed systems.

Core Components:

  • Places: Represent conditions or states of the system.
  • Transitions: Symbolize events that can change the state of the system.
  • Tokens: Denote the presence or absence of certain conditions. The distribution of tokens across places represents the current state of the system.
  • Arcs: Connect places to transitions (and vice versa), dictating the flow of tokens and thus the allowable transitions based on the current state.

Usage Context: Widely used in the fields of computer science and systems engineering for modeling complex systems, analyzing performance, and verifying system properties.

3. Elementary Nets (EN) Model

Definition: Elementary Nets (EN) are a simplified version of Petri-nets focused on the fundamental aspects of system behavior, particularly the notions of causality and conflict without considering complex data or hierarchical structures.

Core Components:

  • Conditions: Similar to places in Petri-nets, conditions represent the state of the system but are more binary in nature, indicating whether a condition is true or false.
  • Events: Analogous to transitions, events denote changes between conditions. An event occurs if and only if all its preconditions are true, and its occurrence results in the postconditions becoming true.
  • Arcs: Define the relationship between conditions and events, indicating which conditions must be true for an event to occur and which conditions become true after an event occurs.

Usage Context: ENs are used for modeling and analyzing simple systems or processes where the focus is on the presence or absence of conditions and the basic causality relationships between events. They serve as a foundational concept for understanding more complex Petri-net variants and are useful in educational settings or initial system design phases.

Each of these models serves different but complementary roles in analyzing and designing systems, from simple workflows to complex systems characterized by concurrent and parallel processes.

Blockchain Tokens: The “Nails” of Digital Ledger Technology

  1. Simple and Direct Functionality: Blockchain tokens are like nails in the sense that they have a straightforward function – representing value or information in a blockchain network. Similar to nails, which are used to join materials in a direct and non-complex manner, blockchain tokens are used to represent assets or data in a transactional context without intrinsic mechanisms for handling complex interactions or conditions.

  2. Limited Composability: Nails are excellent for fastening but offer limited flexibility once driven into materials. Similarly, blockchain tokens, once issued or transacted, often lack inherent flexibility. They are typically bound to the rules of their specific blockchain protocol and do not naturally lend themselves to composability or interaction with other systems unless explicitly designed to do so.

  3. Robustness in Specific Roles: Just as nails are robust and effective for specific construction purposes, blockchain tokens are highly effective within the scope of their intended blockchain environment. They provide a reliable and tamper-proof means of representing value or data on a blockchain network.

Monadic Structures in Petri Nets: The “Screws” of Computational Modeling

  1. Encapsulating Complexity: Monadic structures in Petri nets can be likened to screws. They are capable of encapsulating complex sequences of interactions and state changes within a system. This encapsulation allows for handling more intricate processes than simple token representation, similar to how screws are used for more complex and adjustable connections in construction.

  2. High Composability: Just as screws offer adjustable and reconfigurable connections, monadic structures in Petri nets provide high composability. They allow for the chaining of operations, management of side effects, and facilitation of complex workflows, which can be adjusted and reconfigured as needed.

  3. Versatility and Integration: Screws are versatile tools in construction, capable of being integrated into various materials and structures. Similarly, monadic token structures in Petri nets are versatile in computational modeling, capable of representing a wide range of processes and interactions, and integrating with various system components.

Conclusion: Understanding Their Distinct Roles

In summary, blockchain tokens (“nails”) offer straightforward, robust functionality within the specific context of a blockchain network but lack inherent composability. On the other hand, monadic structures in Petri nets (“screws”) encapsulate complexity and offer high composability, making them suited for modeling intricate and adjustable systems. Understanding the distinct roles and capabilities of these structures is key in leveraging their strengths effectively in their respective domains – blockchain technology and computational modeling.

Petri Nets from Simple to Compound Machines

In the world of computational modeling and data structures, Petri nets hold a unique place. They can be as straightforward as a lever or as intricate as a Swiss watch, depending on how they're used. Let's explore this fascinating versatility through a mechanical analogy: comparing simple machines, like planes, to compound machines, like screws.

Petri Nets as Simple Machines: The Plane Analogy

Imagine a plane – not the aircraft, but the simple tool used in carpentry to shave wood. It's straightforward, effective, and has a singular purpose. In the world of Petri nets, their simplest use mirrors this simplicity. When employed as basic data structures, Petri nets model the flow and distribution of tokens across a network of places and transitions. They are clear, direct, and focused, akin to how a plane smoothly shaves a wooden surface, leaving behind a uniform pattern.

This simplicity makes them perfect for direct state representation and transitions in systems, much like how a plane directly applies force for a specific task. In educational and theoretical settings, this use of Petri nets helps students and professionals alike grasp the fundamentals of computational processes and state management in a straightforward, uncomplicated manner.

Petri Nets as Compound Machines: The Screw Analogy

Now, let's shift gears to a more complex tool: the screw. A screw is a marvel of engineering, combining the features of an inclined plane and a cylinder to perform complex tasks. It turns rotational motion into linear force and can fasten materials together with remarkable efficiency. This compound functionality is where Petri nets, used in more complex scenarios, shine.

When modeling intricate systems, such as Conway's Game of Life or the strategic depths of chess, Petri nets evolve. They become networks of interrelated places, transitions, and arcs, each representing different states, conditions, and changes. This complex usage mirrors how a screw works, combining various elements and mechanisms to achieve a multifaceted outcome.

In these applications, Petri nets transcend direct state representation. They become tools for abstracting and simulating dynamic systems, capturing relationships, and contingent behaviors that are far from straightforward. This complexity allows for modeling real-world phenomena with an impressive depth, much like how a screw can hold together components in a machine, unseen but integral.

Conclusion: The Versatility of Petri Nets

The beauty of Petri nets lies in their adaptability. In their simplest form, they are as transparent and direct as a carpenter's plane. In more complex applications, they transform into intricate tools, similar to the multifunctional screw in a craftsman's toolkit. This versatility makes Petri nets an invaluable resource in both educational and professional settings for those delving into the realms of computational models and data structures.

Whether you're a student starting in computer science or a seasoned professional tackling complex systems, understanding the dual nature of Petri nets – from simple to compound – offers insights into their potential and applications in various domains. It's a journey from the simplicity of direct representation to the complexity of abstract modeling, a journey well worth taking.

With the increasing popularity of blockchain technology and the adoption of smart contracts, ensuring the correctness and security of these contracts has become crucial. Traditional software development methodologies may not be sufficient to address the unique challenges posed by smart contracts. In this blog post, we will explore how a model-driven approach, combined with formal methods, can provide a powerful framework for validating Solidity smart contracts.

Model-Driven Development and Smart Contracts

Model-driven development (MDD) is an approach that emphasizes the use of models to drive the software development process. In MDD, a model serves as a high-level abstraction of the system being developed, capturing its structure, behavior, and constraints. These models are then transformed into executable code through automated processes.

When applied to smart contract development, MDD can help in creating correct-by-construction contract interfaces. By modeling the contract's behavior and properties using a formalism such as Petri nets, we can leverage formal methods to verify various properties of the contract and ensure its correctness.

Petri Nets and Formal Methods

Petri nets are a mathematical modeling technique used to describe and analyze systems with concurrent processes. They consist of places, transitions, and arcs that represent the flow of tokens between them. Petri nets provide a visual and formal representation of the system's behavior, making them well-suited for modeling smart contracts.

Formal methods, on the other hand, are mathematical techniques used to reason about the correctness and behavior of software systems. They involve formal specification, verification, and validation of properties using rigorous mathematical models. By applying formal methods to smart contracts modeled using Petri nets, we can formally verify various properties of the contract, such as safety, liveness, and absence of certain undesirable behaviors.

The Solidity Smart Contract Example

Let's take a look at a Solidity smart contract that demonstrates the application of a model-driven approach using Petri nets and formal methods for contract validation. The contract represents a Tic-Tac-Toe game and includes a metamodeling technique to create a correct-by-construction contract interface.

See the full solidity contract on Github.

In this example, the TicTacToeModel contract represents the Petri net model of the Tic-Tac-Toe game. It inherits from the MetamodelUint8 contract, which provides functions for building the Petri net model using the metamodeling technique. The TicTacToe contract is the actual implementation of the Tic-Tac-Toe game and includes functions for game moves and resetting the game.

Leveraging Formal Methods for Validation

To validate the Tic-Tac-Toe smart contract, we can use formal methods to verify properties such as:

  1. Safety: Ensuring that the game state remains within a set of desired states and that certain conditions are never violated.

  2. Liveness: Ensuring that the game progresses and eventually reaches a terminal state (win, draw, or loss).

  3. Role-based Access: Verifying that the players' moves are restricted to their respective turns and roles.

By formally specifying these properties and applying model-checking techniques, we can automatically analyze the Petri net model and verify whether the smart contract satisfies these properties. This provides a high level of confidence in the correctness and security of the contract, minimizing the risk of vulnerabilities and bugs.

Conclusion

In this blog post, we explored how a model-driven approach combined with formal methods can be used to validate Solidity smart contracts. By leveraging Petri nets as a modeling technique and applying formal methods for verification, we can ensure the correctness, safety, and liveness of smart contracts. This approach enhances the trustworthiness of smart contracts and reduces the risk of vulnerabilities and exploits.

As the blockchain ecosystem continues to evolve, adopting rigorous validation techniques like model-driven development and formal methods becomes increasingly important. By embracing these practices, developers can build more reliable and secure smart contracts, driving the widespread adoption of blockchain technology.

Note: The code provided in this blog post is a simplified example for illustrative purposes. When applying a model-driven approach and formal methods to real-world smart contracts, additional considerations and complexities may arise.

Petri nets are a mathematical tool used to model and analyze systems that involve concurrency, synchronization, and resource sharing. They are useful in a variety of fields, including computer science, engineering, and biology.

One way to view Petri nets is to think of them as a way of accounting for the number of possible ways a user can interact with a system over time. Recall that a Petri net consists of a set of places and a set of transitions. Each place represents a resource or state of the system, while each transition represents a change or event that can occur in the system. A Petri net describes the rules for how these changes can occur and how resources can be shared between transitions.

Consider this Petri-Net composed of actions only.

The gamepad model provides a ‘virtual gamepad’ with buttons. Just like a gamepad in the real world, this model doesn’t have a ‘state’ of it’s own, thus this Petri-net also has no places or connections between actions.

Consider a simple move from a Head-to-Head fighting game. When a player is mashing buttons randomly, sometimes you get lucky and construct a combination move. For example an Upper-Cut could be [ Down, Up, A ]

By adding some state to the model, (and transitions and guards) we can refine the Petri-Net to detect our combo move.

In the above diagram, we have declared ‘noop’ i.e. ‘no-operations’ state, and rules to disallow any other buttons that we do not use in this sequence.

Additionally, we add two interstitial states that enforce that we perform the moves in the proper order.

When we use Petri nets for programming, a programmer can represent the program's states in an explicit manner. This allows the developer and users alike to visualize the flow of the program and the dependencies between different parts of the program. By breaking down the program into smaller components, the programmer can better understand the behavior of the system and how different parts of the program interact with each other.

Now let’s consider a more elaborate move sequence: The Konami Code

(NOTE: when playing with two players, we have added […‘select’, ‘start’]

Petri nets provides a way for programmers to decompose the state of a program and reason about its behavior in a structured and systematic way.

For example, we can think about the overall complexity of these two models, by comparing the code used to generate them.

First let’s see our general solution for any string of non-repeating moves:

Now compare with this code written specifically to model the konami code:

The first sequence is much easier to compose, since we need only to string the required moves together. The Konami code essentially has to be composed directly as a ‘program’ itself. The simpler model is easer to compose, and to generalize for all non-repeating sequences.

There is also a trade-off at play: We could compose the Konami code in a similar manner, but we would have to expand the model to have a state for every move in the sequence.

Conclusion

Petri nets can be thought of as a form of programming synthesis because they provide a way to describe a program's behavior without specifying its implementation. Instead of directly writing code, a programmer can use Petri nets to model the system's state and transitions. This can be useful in situations where the programmer needs to quickly prototype or explore different design choices.

By comparing these examples, we have demonstrated that Petri-nets can model deterministic and non-deterministic automata depending on how state is used. Furthermore, we have seen that the more a programmer can refine and constrain models, the less complex, and more general our code can become. Ultimately, there is always a trade-off cost between interoperability, code size, and memory usage. Explicitly modeling these properties gives the programmer a very sharp tool for reasoning about them up front.

See a live-demo of these models, or view the source models on github.