Satya Prakash Nayak

• The synthesis of logical controllers that guarantee desired specifications is a central problem in the design of cyber-physical systems (CPS). In practice, such guarantees rely on assumptions about how the controller interacts with its environment. These assumptions restrict environment behavior to make synthesis feasible, but in existing approaches they are often overly restrictive, leading to conservative designs and limiting the range of behaviors that systems can safely accommodate. This thesis rethinks the role of assumptions in logical controller synthesis by emphasizing their \emph{permissiveness}---the ability to capture a wide range of admissible environment behaviors. We study permissive assumptions in two key settings: (a) interactions among multiple discrete components in distributed systems, and (b) interactions between high-level logical controllers and low-level physical dynamics in hybrid systems. In both settings, we develop theoretical and algorithmic foundations for computing and exploiting permissive assumptions to enable new design paradigms for logical controller synthesis. For distributed systems, we define permissiveness as capturing all cooperative behaviors of other components that enable a controller to satisfy its specification. We present an algorithm for computing such assumptions in monolithic systems and extend it to distributed systems via a negotiation-based framework that iteratively constructs permissive assume-guarantee contracts for each component. These contracts enable decentralized synthesis and are applied to human-robot interaction, allowing robots to cooperate with humans whenever possible and request cooperation only when necessary. For hybrid systems, we utilize permissive assumptions on the plant model---the abstract representation of physical dynamics---to address three key challenges. To enable seamless adaptation of controllers to changing logical contexts, i.e., changes in high-level goals or tasks, we introduce a novel synthesis framework that utilizes \emph{persistent live groups}, a class of assumptions capturing liveness properties of continuous dynamics. To improve scalability to large or uncertain plant models, we develop \emph{universal controllers} where decisions are conditioned on branching-time assumptions called \emph{prophecies}, which are learned from representative models and efficiently verified at runtime on unseen plant models. Finally, to enhance robustness under uncertainty or partial violations of assumptions on the plant model, we introduce a robust semantics for branching-time temporal logics, enabling formal reasoning about controller behavior under such violations. Overall, this work enables correctness-by-construction synthesis while avoiding unnecessary conservatism, resulting in CPS that are more robust, scalable, and responsive.
• Die Synthese logischer Regelungsoftware, die das gewünscht Verhalten eines technischen Systems sicherstellt, ist ein zentrales Problem beim Entwurf von cyber physikalischen Systemen. Meist basieren die resultierenden Verhaltensgarantien dann auf Annahmen darüber, wie das System mit seiner Umgebung interagiert. Bestehende Ansätze beruhen jedoch oft auf sehr restriktiven Annahmen, was zu konservativen Regelungsverhalten führt und das Umgebungsverhalten begrenzt was Systeme sicher tolerieren können. Diese Arbeit entwickelt einen neunen Ansatz zum logischen Reglerentwurf, indem sie die Permissivität von Annahmen -- das heißt die Fähigkeit ein breites Spektrum zulässiger Umgebungsverhalten zu modellieren -- in den Vordergrund stellt. Konkret betrachten wir permissive Annamhen in zwei zentralen Bereichen: (a) Interaktionen zwischen mehreren diskreten Komponenten in verteilten Systemen und (b) Interaktionen zwischen übergeordneten logischen Reglern und der physikalischen Dynamik in hybriden Systemen. In beiden Anwendungsbereichen entwickeln wir theoretische und algorithmische Grundlagen für die Berechnung und Nutzung permissive Annahmen, um neue modellbasierte Entwurfsverfahren für logische Regelungssoftware zur Verfügung zu stellen. Für verteilte Systeme definieren wir Permissivität als die Fähigkeit alle kooperativen Verhaltensweisen anderer Komponenten abzubilden die einen Reglerentwurf möglich machen. Wir präsentieren einen Algorithmus zur Berechnung solcher Annahmen in monolithischen Systemen und erweitern ihn auf verteilte Systeme mittels eines verhandlungsbasierten Ansatzes, das iterativ permissive Annahme-Garantie-Verträge für jede Komponente erstellt. Diese Verträge ermöglichen dezentrale Synthese und wurden von uns in der Mensch-Roboter-Interaktion angewendet. Für hybride Systeme nutzen wir permissive Annahmen über das Streckenmodell---d.h. die abstrakte logische Repräsentation der physikalischen Streckendynamik---um drei zentrale Herausforderungen zu bewältigen. Um eine natlose Anpassung von REgelungssoftware an sich ändernde logische Kontexte, zu ermöglichen, führen wir einen neuartigen Synthese-Ansatz ein, das neuartige permissive Annahmen nutzt um Letztendlichkeitseigentschaften der Streckendynamik zu erfassen. Um die Skalierbarkeit auf große oder nicht genau bekannte Streckenmodelle zu erweitern, entwickeln wir so genannte \emph{universelle Regler} deren Entscheidungen auf \emph{Prophezeiungen} basieren, die mithilfe repräsentativer kleiner Modelle gelernt wurden. Um die Robustheit gegenüber Unsicherheiten oder teilweisen Verletzungen der Annahmen über das Streckenmodell zu erhöhen, führen wir eine robuste Semantik für Verzweigungszeitlogiken ein.