The intersection of the two non-deterministic Büchi automata is empty if the model satisfies the property.
Der Schnitt der beiden nicht-deterministischen Büchi-Automaten ist leer, wenn das Modell die Eigenschaften erfüllt.