In this thesis, we show how to specify and verify safety as well as secrecy in workflow systems with arbitrarily many participating agents. We rely on First-order Transition Systems as a formal model and formalize their properties in First-order HyperLTL. We provide approaches to automatically verify rich classes of First-order transition systems and prove the problem undecidable for the general case. Beyond verification, we extend our algorithms to synthesis questions on First-order Safety Games.      «

In this thesis, we show how to specify and verify safety as well as secrecy in workflow systems with arbitrarily many participating agents. We rely on First-order Transition Systems as a formal model and formalize their properties in First-order HyperLTL. We provide approaches to automatically verify rich classes of First-order transition systems and prove the problem undecidable for the general case. Beyond verification, we extend our algorithms to synthesis questions on First-order Safety Game...     »

Wir modellieren Sicherheits- sowie Geheimhaltungseigenschaften von Workflow-Systemen mit einer unbeschränkten Anzahl von beteiligten Agenten. Als formales Modell nutzen wir prädikatenlogische Transitionssysteme und formalisieren deren Eigenschaften in First-order HyperLTL. Wir entwickeln Methoden um Klassen von Transitionssystemen vollautomatisch zu verifizieren und zeigen Unentscheidbarkeit für Systeme ausserhalb dieser Klassen. Darüber hinaus entwickeln wir Synthese-methoden für prädikatenlogische Systeme.      «

Wir modellieren Sicherheits- sowie Geheimhaltungseigenschaften von Workflow-Systemen mit einer unbeschränkten Anzahl von beteiligten Agenten. Als formales Modell nutzen wir prädikatenlogische Transitionssysteme und formalisieren deren Eigenschaften in First-order HyperLTL. Wir entwickeln Methoden um Klassen von Transitionssystemen vollautomatisch zu verifizieren und zeigen Unentscheidbarkeit für Systeme ausserhalb dieser Klassen. Darüber hinaus entwickeln wir Synthese-methoden für prädikatenlogi...     »