ostrich

Parameterized verification is a hard problem. Inspired by reachability analysis of Petri nets via structural invariants we approach the analysis of parameterized systems by capturing structural invariants in the decidable logic WS1S .

Idea

We consider Petri nets which are parameterized w.r.t. their size. That means, once we fix N to be the size of our parameterized system we obtain one specific Petri net which we call the instance of size N. Any parameterized Petri net specifies a finite set of place names, and the places of any instance are all tuples of the values {0, ..., N-1} and these place names.

Conceptually, if we have monadic variables (one for each place name) and an interpretation which assigns to these monadic variables subsets of {0, ..., N-1}, then these monadic variables collectively define a subset of the places of the instance of size N.

Transitions can now be defined by a WS1S formula which relates two sets of places (the preset and the postset respectively); i.e., any two sets of places induce an interpretation of the free variables of the transition formula. Those sets which induce a satisfying interpretation of the transition formula are a transition of this instance.

Crucial to our approach is that we can reason about the structure of all instances in WS1S. Moreover, we can quantify sets of places in WS1S. Using this ostrich implements a semi-decision procedure for such parameterized systems by reasoning about invariants of the parameterized systems which are specified by sets of places and how these can be changed by the transitions.

By employing MONA as solver for WS1S in its backend, ostrich can prove safety properties of various parameterized systems.

Example

We consider a version of the dining philosophers where one philosopher takes her forks the other way around than all others:

              
{
  "states": ["waiting", "hungry", "eating", "free", "busy"],
  "cover": [["waiting", "hungry", "eating"],
            ["free", "busy"]],
  "topology": "headed ring",
  "initial": {
    "others": ["waiting", "free"]
  },
  "transitions": [
    {
      "rendezvous": {
        "guard": "0 < p",
        "p": [
          {
            "preset": ["waiting", "free"],
            "postset": ["hungry", "busy"]
          }
        ]
      }
    }, {
      "rendezvous": {
        "guard": "0 < p & p >> q",
        "p": [
          {
            "preset": ["hungry"],
            "postset": ["eating"]
          }
        ],
        "q": [
          {
            "preset": ["free"],
            "postset": ["busy"]
          }
        ]
      }
    }, {
      "rendezvous": {
        "0": [
          {
            "preset": ["waiting"],
            "postset": ["hungry"]
          }
        ],
        "1": [
            {
            "preset": ["free"],
            "postset": ["busy"]
          }
        ]
      }
    }, {
      "rendezvous": {
        "0": [
          {
            "preset": ["hungry", "free"],
            "postset": ["eating", "busy"]
          }
        ]
      }
    }, {
      "rendezvous": {
        "guard": "p >> q",
        "p": [
            {
            "preset": ["eating", "busy"],
            "postset": ["waiting", "free"]
          }
        ],
        "q": [
            {
            "preset": ["busy"],
            "postset": ["free"]
          }
        ]
      }
    }
  ]
}
              
            

Conceptually, we consider the underlying sets of places to work as communicating automata for every index. The partition of states described in cover corresponds to the states of these automata.

Code

ostrich is written in Python. The code is maintained on the GitLab of the TUM.

Since ostrich is subject to ongoing research the codebase is unstable. Please refer to the artifacts for stable snapshots.

Artifacts

In the following we list submitted artifacts of ostrich.

• TACAS'20
• Petri nets'21

Publications

• Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, Christoph Welzel . Structural Invariants for the Verification of Systems with Parameterized Architectures . TACAS'20

• Javier Esparza, Mikhail Raskin, Christoph Welzel . Computing Parameterized Invariants of Parameterized Petri Nets . Preprint accepted at Petri nets'21.

Contact

If you have questions regarding ostrich, please contact Christoph, Mikhail, or Javier.

Acknowledgements

This project has received funding from the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).