Synthesis for defeating adversaries with limited capabilities




Raju, Dhananjay

Journal Title

Journal ISSN

Volume Title



Reactive synthesis is a potent technique enabling the automatic generation of correct-by-construction implementations of systems based on formal specifications (Bloem et al.,2018; Ehlers et al., 2015; Majumdar et al., 2019). This approach ensures that the synthesized system satisfies its specifications, regardless of the environment’s behavior, making it a more robust alternative to planning. However, reactive synthesis may fail when no system can fulfill the specification against all potential environment behaviors, such as cases where the environment prevents the system from achieving its objectives (Kress-Gazit et al., 2018). To mitigate this issue, researchers often introduce assumptions to constrain the environment’s behavior, ensuring the synthesized system operates correctly when these assumptions hold. This method, however, introduces another challenge, as the synthesized implementations might be motivated to work against the satisfaction of these assumptions (Bloemet al., 2015; Majumdar et al., 2019). An alternative viewpoint treats the interaction between the environment and the system as a strategic game, where an equilibrium between both players’ strategies is computed to guarantee that neither has an incentive to deviate. However,this approach necessitates knowledge of the environment’s objectives to facilitate strategic reasoning. In traditional reactive synthesis, environments can exhibit arbitrary behavior within their limits, with observed behavior providing no useful information. This prompts the question of whether an alternative definition for the synthesis problem could enable the formal synthesis of a correct-by-construction system in environments with unknown behaviors. Drawing inspiration from real-world adversaries, we limit the environment’s behavior. Quantifying the environment’s capabilities is crucial for solving this problem effectively, as without such constraints, the environment could act antagonistically, as in classical reactive synthesis. Concurrently, we aim to develop a controller that consistently functions correctly against the environment’s simple behaviors. In this thesis, we address the issue by restricting the environment’s behavior through limitations on a) behavioral complexity, b) observational capability, or c) the ability to modify operational space.


LCSH Subject Headings