In recent years, ensuring both task satisfaction and security in cyber-physical systems has become increasingly critical, particularly in the context of path planning for systems performing complex Linear Temporal Logic (LTL) tasks. While LTL-based controller synthesis has been widely studied, most existing approaches either address security only post-design or abstract the system as a discrete transition model. This thesis bridges this gap by presenting a unified framework for synthesizing secure-by-construction controllers for both single- agent and multi-agent systems, operating in continuous spaces under affine dynamics. The framework is initially developed for discrete systems and then extended to handle continuous workspaces using tools from formal methods, control theory, and optimization. Security constraints are integrated directly into the synthesis process, and formal correctness guarantees are provided. A definition of security is introduced, extending beyond initial-state, current-state, K-step, and infinite-step opacity. The proposed definition is more general, in the sense that satisfying it implies satisfaction of each of these opacity notions. Security is formalized by ensuring that a passive intruder, capable of observing system outputs but not influencing them, cannot infer sensitive information, such as whether an agent has visited a secret region. The proposed framework defines three distinct types of multi-agent security: (i) a generalization of single-agent opacity that ensures indistin- guishability across agents, (ii) a decoy-based approach, where certain agents conceal the actions of agents executing secret tasks, and (iii) a delay-aware formulation, which accounts for delays in the intruder’s observations. By integrating these security specifications into the control synthesis process, the framework guarantees both satisfaction of LTL tasks and the preservation of security for agents governed by affine dynamics. The correctness and real-world applicability of the proposed algorithms is validated through several single-agent and multi-agent examples.

Under de senaste åren har det blivit allt viktigare att säkerställa både uppgiftsuppfyllelse och säkerhet i cyberfysiska system, särskilt när det gäller vägplanering för system som utför komplexa uppgifter i linjär temporallogik (LTL). Även om LTL-baserad styrenhetssyntes har studerats i stor utsträckning, tar de flesta befintliga metoder antingen upp säkerhet först efter design eller abstraherar systemet som en diskret övergångsmodell. Denna avhandling överbryggar detta gap genom att presentera ett enhetligt ramverk för att syntetisera secure-by-construction-kontroller för både enagentsystem och multiagentsystem, som arbetar i kontinuerliga utrymmen under affin dynamik. Ramverket utvecklas initialt för diskreta system och utvidgas sedan för att hantera kontinuerliga arbetsytor med hjälp av verktyg från formella metoder, reglerteori och optimering. Säkerhetskrav integreras direkt i syntesprocessen och formella korrekthetsgarantier tillhandahålls. En definition av säkerhet introduceras, som sträcker sig bortom initial- tillstånd, aktuellt tillstånd, K-steg och oändlig stegsopacitet. Den föreslagna definitionen är mer generell, i den meningen att om den uppfylls innebär det att alla dessa opacitetsbegrepp uppfylls. Säkerhet formaliseras genom att säkerställa att en passiv inkräktare, som kan observera systemets utdata men inte påverka dem, inte kan härleda känslig information, till exempel om en agent har besökt ett hemligt område. Det föreslagna ramverket definierar tre olika typer av säkerhet för flera agenter: (i) en generalisering av opacitet för enskilda agenter som säkerställer oskiljbarhet mellan agenter, (ii) en decoy-baserad metod, där vissa agenter döljer handlingarna hos agenter som utför hemliga uppgifter, och (iii) en fördröjningsmedveten formulering som tar hänsyn till förseningar i inkräktarens observationer. Genom att integrera dessa säkerhetsspecifikationer i kontrollsyntesproces- sen garanterar ramverket både uppfyllandet av LTL-uppgifter och bevarandet av säkerheten för agenter som styrs av affin dynamik. De föreslagna algoritmernas korrekthet och tillämpbarhet i verkligheten valideras genom flera exempel med en eller flera agenter.