Realizability and verification of MSC graphs

Our second set of results concerns verification of MSC-graphs. While checking properties of a graph G, besides verifying all the scenarios in the set L(G) of MSCs specified by G, it is desirable to verify all the scenarios in the set Lw(G)-the closure of G, that contains the implied scenarios that any distributed implementation of G must include. For checking whether a given MSC M is a possible behavior, checking M∈L(G) is NP-complete, but checking M∈Lw(G) has a quadratic solution. For temporal logic specifications, considering the closure makes the verification problem harder: while checking LTL properties of L(G) is PSPACE-complete for bounded graphs G, checking even simple “local” properties of Lw(G) is undecidable.