A Web Interface for Petri Nets with Transits and Petri Games

TL;DR

This paper introduces a web-based visual tool for defining and analyzing Petri nets with transits and Petri games, facilitating error detection, model checking, and controller synthesis for distributed systems.

Contribution

It provides an intuitive, visual web interface for modeling Petri nets with transits and Petri games, integrating model checking and synthesis directly on a server.

Findings

Enables visual, step-by-step modeling of Petri nets with transits and Petri games.

Supports real-time simulation and analysis of models and counterexamples.

Facilitates error detection and validation in distributed system models.

Abstract

Developing algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome when performed textually. In this paper, we present a web interface that allows an intuitive, visual definition of Petri nets with transits and Petri games. The corresponding model checking and synthesis problems are solved directly on a server. In the interface, implementations, counterexamples, and all intermediate steps can be analyzed and simulated. Stepwise simulations and interactive state space generation support the user in detecting modeling errors.