  In this work we provide algorithmic solutions to five fundamental problems
concerning the verification, synthesis and correction of concurrent systems
that can be modeled by bounded p/t-nets. We express concurrency via partial
orders and assume that behavioral specifications are given via monadic second
order logic. A c-partial-order is a partial order whose Hasse diagram can be
covered by c paths. For a finite set T of transitions, we let P(c,T,\phi)
denote the set of all T-labelled c-partial-orders satisfying \phi. If N=(P,T)
is a p/t-net we let P(N,c) denote the set of all c-partially-ordered runs of N.
A (b, r)-bounded p/t-net is a b-bounded p/t-net in which each place appears
repeated at most r times. We solve the following problems:
  1. Verification: given an MSO formula \phi and a bounded p/t-net N determine
whether P(N,c)\subseteq P(c,T,\phi), whether P(c,T,\phi)\subseteq P(N,c), or
whether P(N,c)\cap P(c,T,\phi)=\emptyset.
  2. Synthesis from MSO Specifications: given an MSO formula \phi, synthesize a
semantically minimal (b,r)-bounded p/t-net N satisfying P(c,T,\phi)\subseteq
P(N, c).
  3. Semantically Safest Subsystem: given an MSO formula \phi defining a set of
safe partial orders, and a b-bounded p/t-net N, possibly containing unsafe
behaviors, synthesize the safest (b,r)-bounded p/t-net N' whose behavior lies
in between P(N,c)\cap P(c,T,\phi) and P(N,c).
  4. Behavioral Repair: given two MSO formulas \phi and \psi, and a b-bounded
p/t-net N, synthesize a semantically minimal (b,r)-bounded p/t net N' whose
behavior lies in between P(N,c) \cap P(c,T,\phi) and P(c,T,\psi).
  5. Synthesis from Contracts: given an MSO formula \phi^yes specifying a set
of good behaviors and an MSO formula \phi^no specifying a set of bad behaviors,
synthesize a semantically minimal (b,r)-bounded p/t-net N such that
P(c,T,\phi^yes) \subseteq P(N,c) but P(c,T,\phi^no ) \cap P(N,c)=\emptyset.
