User: Guest  Login
Original title:
Proving Noninterference in Multi-Agent Systems 
Translated title:
Verifikation von Sicherheitseigenschaften in Multi-Agenten-Systemen 
Year:
2020 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Seidl, Helmut (Prof. Dr.) 
Referee:
Seidl, Helmut (Prof. Dr.); Esparza Estaun, Francisco Javier (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
Noninterference, Multi-agent Systems, First-order logic, First-order Transition Systems, First-order Safety Games, Inductive Invariants 
Translated keywords:
Multi-agenten Systeme, First-order Transitionssysteme, First-order Logik, Prädikatenlogik, Induktive Invarianten 
TUM classification:
DAT 500d 
Abstract:
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...    »
 
Translated abstract:
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...    »
 
Oral examination:
10.06.2020 
File size:
868277 bytes 
Pages:
175 
Last change:
03.11.2020