Um die Schwierigkeiten einer korrekten und gründlichen Durchführung der Gefahrenbestimmung zu verringern, kann man versuchen, sie auf eine formale Darstellung des zu untersuchenden Systems aufzusetzen. Ein Beispiel hierfür wäre die Darstellung des Systems als endlichem Automaten und die Gefahrenbestimmung anhand dieses Automaten [Lev95, S. 346ff], die im folgenden diskutiert werden soll.
Grundsätzlich läßt sich jedes technische System als Zustandsautomat darstellen. In den meisten Fällen wäre die naturgetreue Modellierung in dieser Form jedoch nicht ein Automat mit einer endlichen Zahl von Zuständen und Zustandsübergängen, weil in den meisten Systemen kontinuierliche Variablen auftreten; im obigen Beispiel zur Ursachen-Folgen-Analyse etwa der Druck. Jedoch kann man in fast allen Fällen von der Menge aller Zustände abstrahieren, wenn es um die Gefahrenbestimmung geht und stattdessen nur die Menge der qualitativ verschiedenen Zustände betrachten. Diese ist immer endlich; im Beispiel wäre dies für den Druck (Bestandteil des Zustands) nur die Unterscheidung, ob er akzeptabel oder zu hoch ist und für die Druckänderung (Zustandsübergänge), ob der Druck steigt, fällt oder konstant ist. Eine solche Betrachtung abstrahiert also aus einer großen Zahl von echten Systemzuständen in einen einzigen abstrakten Zustand in einer solchen Weise, daß dabei keine gefahrenrelevante Information verlorengeht. Zu beachten ist, daß nicht nur die Zustände ausreichend erfaßt werden müssen, sondern auch die Zustandsübergänge.
Es ist nicht immer klar, welche Zustände sinnvollerweise für die Gefahrenbestimmung als qualitativ verschieden betrachtet werden sollten. Erfahrung erlaubt jedoch eine Auswahl, die nur wenige Zustände unterscheidet und dennoch alle Gefahren zu identifizieren erlaubt. Es können leider keine allgemeingültigen Regeln hierfür angegeben werden.
Liegt das System in Form eines endlichen Automaten vor, so müssen zunächst alle diejenigen Zustände identifiziert werden, die eine Gefahr bedeuten. Diese bilden dann den Mittelpunkt der Analyse: Im Prinzip kann man nun vom Startzustand des Systems aus mittels Vorwärtssuche alle erreichbaren Zustände untersuchen und ermitteln, welche gefährlichen Zustände darunter sind. Leider ist wegen der großen Zahl von Zuständen und Übergängen dieses Vorgehen schon für relativ einfache Systeme unrealistisch. Es gibt eine alternative Vorgehensweise, nämlich von gefährlichen Zuständen aus zu beginnen und mittels Rückwärtssuche zu prüfen, welche davon vom System erreichbar sind. Auch diese Methode scheitert jedoch an der enorm großen Zahl von Zustandspfaden.
Eine praktikable Lösung besteht oft darin, mit der Rückwärtssuche nur jeweils soweit fortzufahren, bis man einen Weg erkennen kann, wie das Modell (also auch das System) geändert werden muß, damit der gefährliche Zustand unerreichbar wird. Der Nachteil dieses Vorgehens besteht darin, daß man eventuell unnötige Änderungen am Modell vornimmt, weil der Zustand ohnehin unerreichbar war; dies kann man jedoch normalerweise gut in Kauf nehmen.
Die beschriebene Vorgehensweise hat drei Hauptschwierigkeiten, nämlich die Größe des Automaten, die Größe des Suchraums und die Frage nach der Korrektheit.
Die ersten beiden Probleme wurden oben bereits angesprochen. Der Versuch, ein System im ganzen als Automat zu erfassen, führt selbst in einfachen Fällen und unter Ausnutzung aller Abstraktionsmöglichkeiten zu so großen Automaten, daß deren Aufstellung, geschweige denn vollständige Untersuchung praktisch unmöglich wird. Deshalb läßt sich der Ansatz nur für Ausschnitte aus dem Systemverhalten durchführen oder unter bewußter Verwendung von Übervereinfachung, d.h. unter Inkaufnahme des Verlustes gefahrenrelevanter Information durch übermäßiges Zusammenfassen von Zuständen oder Übergängen.
Das dritte Problem teilt der Ansatz mit allen Verfahren, die auf einem abstrakten Modell des Systems arbeiten (z.B. Programmverifikation): Es kann grundsätzlich nicht sichergestellt werden, daß das Modell korrekt ist. Deshalb ist es möglich (und in der Realität sogar wahrscheinlich), daß auch nach einer vollständigen Gefahrenbestimmung am formalen Modell noch unerkannte Gefahren im wirklichen System vorhanden sein werden. Wie in allen anderen Fällen von formalen Methoden kann man auch hier versuchen, dem Problem durch Validation zu entgehen. Im vorliegenden Fall bedeutet das die Simulation des Systems anhand des formalen Modells und Prüfung, ob sich die Simulation so verhält, wie man es vom System erwarten würde. Ihre Grenzen findet dieses Vorgehen dort, wo das Verhalten des zu modellierenden Systems nicht bekannt ist.
Dieser prinzipielle Mangel bedeutet jedoch keineswegs, daß der Einsatz formaler Methoden eine schlechte Idee wäre. Das Gegenteil ist der Fall, denn alle geschilderten Schwierigkeiten hat man prinzipiell auch dann, wenn man informell vorgeht, nur bemerkt man sie dann oftmals nicht -- auch dies hat der vorliegende Fall mit anderen Anwendungen formaler Methoden gemein. Eine Gefahrenbestimmung mit endlichen Automaten ermöglicht eine gezieltere und bewußtere Auslassung von Bereichen in der Analyse als es ad-hoc-Methoden erlauben.