ames on graphs provide an effective way to model and formalize interesting problems in the context of correct-by-construction cyber-physical systems (CPS) design. In such applications, a control software tries to keep the system running while fulfilling its task at hand, under presence of a physical environment (e.g., uncontrollable task assignment, transient operating conditions, and controllable agents with their own tasks). While games on graphs have proved their worth in synthesis under adversarial environment, they have not been of great help under changing conditions and potentially helpful agents. Such games inherently assume that the environment is always antagonistic, and the system needs \emph{one} strategy to win against such an environment. However, in practice, it is rarely the case that the environment is adversarial (in fact, it might even be possible to control the environment agents), and that the operating conditions remain static to allow one strategy to be sufficient. The key missing link in the remedy of the mentioned problems is the notion of permissiveness of the agents involved in the game being played, which is an exigent concept in design of control software that is robust to changes and can work in tandem with other agents in its vicinity.
With the goal to automatically obtain resilient and team-playing controllers to solve tasks in the cyber-physical world, in our work, we present novel ways to produce permissive controllers that are capable of automatic negotiations with other controllers. To this end, in our work, we formalize the notions of a permissive assumption on the environment and permissive strategies for the system. We then use novel permissive templates to describe both for a game. With that in place we give incremental algorithms to compose objectives, to build fault-tolerant controllers, and to automatically negotiate with other agents to complete different tasks.
In addition to the publications listed below, we have also used permissive templates for a novel abstraction-based control technique for non-linear dynamical systems.
Group Members Involved:
Collaborators:
- Kaushik Mallik (IST Austria)
Tools:
- PeSTel : A tool for computing Permissive Strategy Templates for (generalized) parity games [ GitHub ]
- SImPA : A tool for computing Sufficient, Implementable and Permissive Assumptions for parity games [ GitLab ]
Publications:
- ® A. Anand, A.-K. Schmuck, and S. P. Nayak. Contract-Based Distributed Logical Controller Synthesis. 2024. HSCC’24 (PDF, Extended Version, HSCC’23 poster) (HSCC’23 best poster award)
- * S. P. Nayak, A.-K. Schmuck. Most General Winning Secure Equilibria Synthesis in Graph Games. 2024. TACAS’24 (PDF, extended version)
- * A. Anand, S. P. Nayak, and A.-K. Schmuck. Contract-Based Distributed Logical Controller Synthesis. 2024. HSCC’24 (to appear, Arxiv preprint, HSCC’23 poster) (HSCC’23 best poster award)
- * A. Anand, S. P. Nayak, and A.-K. Schmuck. Synthesizing Permissive Winning Strategy Templates for Parity Games. 2023. CAV’23. (PDF, extended version)
- * A. Anand, K. Mallik, S. P. Nayak, and A.-K. Schmuck. Computing Adequately Permissive Assumptions for Synthesis. 2023. TACAS’23. (PDF, extended version)
all publications list authors either in alphabetic (indicated by a pink *) or in randomized (indicated by a purple ®) order, with their publicly verifiable record of the randomization available here.