Index page

[mgieseking]

Improve the introductory page with some general texts and large links to the two approaches and the tutorials (see #36 )

[mgieseking]

Text for the model checking approach:

AdamMC: A Flow-LTL Model Checker for the Analysis of Distributed Asynchronous Models

AdamMC is a model checker for asynchronous distributed systems modeled with Petri nets with transits and specifications given in Flow-LTL.

Petri nets with transits extend standard Petri nets with a transit relation to model the local data flow in asynchronous distributed systems in addition to the global control flow. Flow-LTL is a specification language for Petri nets with transits and allows to specify linear properties on both the global and the local view of the system. Especially, it is possible to globally select with LTL desired runs of the system (e.g., only fair and maximal runs) and check the local data flow of only those selected runs against LTL.

Internally the problem is reduced to a verification problem of circuits which is checked by ABC with its large toolbox of hardware verification algorithms. Software defined networks are due to the separation of data and control plane a natural application domain for Petri nets with transits and Flow-LTL.

Features:

• Modeling, visualization, and simulation of Petri nets with transits
• Model checking Petri nets with transits against Flow-LTL
• Model checking 1-bounded Petri nets against LTL with places and transitions as atomic propositions
• Visualization and simulation of counter examples

Documentation:

• https://github.com/adamtool/webinterface/tree/master/doc/mc

Releated Publications:

• Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL. CAV (2) 2020: 64-76 (full version)
• Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: Model Checking Data Flows in Concurrent Network Updates. ATVA 2019: 515-533 (full version)

[mgieseking]

AdamSYNT: Causality-Based Synthesis of Distributed Asynchronous Systems

AdamSYNT is a synthesizer for asynchronous distributed systems modeled with Petri games.

Petri games extend Petri nets with a game semantics. The tokens of the net are the players in the game. Players remember their own causal past and do not know nothing about the others as long as they do not communicate (participating on a joint transition). During a communication all information is passed to all participating players. For local safety winning conditions, the synthesis problem for Petri games with a bounded number of controllable components and one uncontrollable components is solved, i.e., a local controller for each component is created iff a solution exists.

Internally, the problem is reduced to a two-player game over a finite graph with complete information and BDD solving algorithms are used to obtain a strategy.

Features:

• Modeling, visualization, and simulation of Petri games
• Synthesis of Petri games with one environment and a bounded number of system players with a local safety objective
• Exploring the corresponding two-player game for finding modeling bugs
• Visualization and simulation of the strategies

Documentation:

• https://github.com/adamtool/webinterface/tree/master/doc/synt

Releated Publications:

• Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog: Adam: Causality-Based Synthesis of Distributed Systems. CAV (1) 2015: 433-439
• Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: Symbolic vs. Bounded Synthesis for Petri Games. SYNT@CAV 2017: 23-43
• Bernd Finkbeiner, Ernst-Rüdiger Olderog: Petri games: Synthesis of distributed systems with causal memory. Inf. Comput. 253: 181-203 (2017)

[annyanich]

Thanks :) I have put it on the homepage as of 0658c9122e60a8cb4bae7d44f88698006f8a8f5b. Here is a screenshot:

[mgieseking]

I added the links to the documentations for the approaches by editing the comments above.

[annyanich]

All right, I put them in there :)