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 .
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.
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.
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.
In the following we list submitted artifacts of ostrich.
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.
If you have questions regarding ostrich, please contact Christoph, Mikhail, or Javier.
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).