Ausnutzen von Symmetrien Wenn ein zu verifizierendes System eine Komponentenredundanz enthält, können Symmetrien durch sogenannte „Permutationsgruppen“ ausgenutzt werden (diese enthalten den Transitionsgraphen).
Wenn das Ergebnis einer Wertepermutation vorliegt, kann diese für die restlichen redundanten Komponenten kopiert werden. Gerade bei Bausteilen im Hardwarebereich kann diese Optimierung ausgenutzt werden (z.B. Registerfiles, die an mehreren Stellen im System zur Speicherung von Werten verwendet werden)
Induktionsbeweise Das Optimierungsverfahren Induktion ermöglicht die Verifikation für ganze Familien von endlichen Zustandsautomaten durchgeführt werden. In vielen Systemen sind bestimmte Komponenten ähnlich (z.B. ein Schaltkreis, der zwei Integerzahlen der Größe n addiert). Nun muss der Nachweis erbracht werden, dass jedes System bestimmte temporallogische Formel erfüllt. In vielen Fällen ist dies unentscheidbar. Allerdings ist es häufig möglich, einen invarianten Prozess zu definieren, der das Verhalten eines Mitglieds der Familie repräsentiert.
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren