Search for: All records

In this paper, we consider the verification of approximate infinite-step opacity for discrete-time control sys-tems. Relying on finite abstraction techniques for solving this problem requires discretization of the state and input sets, which requires significant computational resources. Here, we propose a discretization-free approach in which we formulate opacity as a safety property over an appropriately constructed augmented system, and seek to verify it by finding suitable barrier certificates. Within our proposed scheme, lack of opacity is also verified by posing it as a reachability property over the augmented system. The main result of this paper offers a discretization-free approach to verify (lack of) infinite-step opacity in discrete-time control systems. We also discuss other notions of opacity, and their relations to one another. We particularly study the conditions under which verifying one form of opacity for a system also implies other forms. Finally, we illustrate our theoretical results on two numerical examples, where we utilize sum-of-squares programming to search for polynomial barrier certificates. In these examples, we verify the infinite-step, and current-step opacity for a vehicle by checking whether its position is concealed from possible outside intruders. 

Recent success in reinforcement learning (RL) has brought renewed attention to the design of reward functions by which agent behavior is reinforced or deterred. Manually designing reward functions is tedious and error-prone. An alternative approach is to specify a formal, unambiguous logic requirement, which is automatically translated into a reward function to be learned from. Omega-regular languages, of which Linear Temporal Logic (LTL) is a subset, are a natural choice for specifying such requirements due to their use in verification and synthesis. However, current techniques based on omega-regular languages learn in an episodic manner whereby the environment is periodically reset to an initial state during learning. In some settings, this assumption is challenging or impossible to satisfy. Instead, in the continuing setting the agent explores the environment without resets over a single lifetime. This is a more natural setting for reasoning about omega-regular specifications defined over infinite traces of agent behavior. Optimizing the average reward instead of the usual discounted reward is more natural in this case due to the infinite-horizon objective that poses challenges to the convergence of discounted RL solutions. We restrict our attention to the omega-regular languages which correspond to absolute liveness specifications. These specifications cannot be invalidated by any finite prefix of agent behavior, in accordance with the spirit of a continuing problem. We propose a translation from absolute liveness omega-regular languages to an average reward objective for RL. Our reduction can be done on-the-fly, without full knowledge of the environment, thereby enabling the use of model-free RL algorithms. Additionally, we propose a reward structure that enables RL without episodic resetting in communicating MDPs, unlike previous approaches. We demonstrate empirically with various benchmarks that our proposed method of using average reward RL for continuing tasks defined by omega-regular specifications is more effective than competing approaches that leverage discounted RL.