Analyse eines Protokolls

Der Analyzer arbeitet prinzipiell wie in 2 beschrieben, jedoch werden bei dem unifizieren der Folgerung mit der Zustandsbeschreibung die event-Anweisungen mit einbezogen. Dadurch kann bei der Angabe des unsicheren Zustandes events angegeben werden, die passiert sein mussten oder Bedingungen.