A Web Interface for Petri Nets with Transits and Petri Games

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 (The web interface is deployed at http://adam.informatik.uni-oldenburg.de.) 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.

Towards an Optimal Generation of Zones Graph Relating Timed Bisimulation Relation and Distribution

The timed automata are extensively used in different fields of formal validation in particular the model checking one. In this paper the authors are interested by a class of TA called durational actions timed automata (daTA) and the zones graph which represents an exact finite state abstraction based on what called Zones. The authors present a novel approach to construct a zone graph, based on the maximality semantics called maximality-based zone graph (MZG) by a local construction approach and they define timed maximality bisimulation relation for real-time model based on the maximality semantics. The authors propose a new method for distributed state space generation of maximality-based zone graph based on DHT structure. They also describe an implementation of this construction (DTaMaZG tool). The experiments given at the end of this article has shown good results especially when comparing with other works that have already proceed in the distributed generation of MLTS (Maximality based Labeled Transition Systems).