Developing algorithms for asynchronous distributed systems is an
error-prone task. This is mainly due to the multiple individual and
concurrent components, each progressing at its own rate between the
synchronizations. In a model checking approach the global behavior and
the implementation of each component's local controller are checked
against a given specification to verify the system's correctness. In a
synthesis approach, implementations are automatically generated from a
given specification and are therefore correct-by-construction.

Petri nets are a well-established and well-suited formalism to model
distributed systems with multiple autonomous and concurrent entities. In
this work we enrich the Petri net model by refining its flow relation.
This model, called Petri net with transits, allows to separately define
the local data flow of the components and the global control flow of the
system. A corresponding temporal logic, namely Flow-CTL*, is introduced
to reason about those parts. Flow-CTL* allows for selecting specific
runs of the control part of the system (e.g., fair and maximal runs) by
means of LTL and checking the data flow of these runs by means of CTL*.
The model checking problem can be solved in single-, double-, and
triple-exponential time for the fragments Flow-LTL, Flow-CTL, and
Flow-CTL*, respectively.

For the synthesis approach we build upon Petri games. A Petri game is a
Petri net extension which provides a game semantics for the concurrent
entities with causal memory. This enables the automatic creation of
correct local controllers from safety specifications. We extend Petri
games to enable the user to additionally model the data flow.
Furthermore, we enhance the specification language to reason about the
existential and universal safety, reachabillity, Büchi, and co-Büchi
behavior of the data flow of the distributed system. This synthesis
problem can be solved in single-exponential time.

Tool support is provided for both, the model checking and the synthesis
approach.