Permissive Strategy Templates (PeSTels)

In this project we target the automated synthesis of strategy templates as robust certified interfaces for interacting autonomous (cyber-physical) systems.

Strategy templates are similar to classical strategies typically computed by reactive software synthesis but contain a huge set of relevant strategies in a succinct and simple data structure. This permissiveness allows efficient adaptations to new specifications as
well as robustness to unexpected actuation failures during runtime. In addition to these favorable engineering properties of strategy templates for cyber-physical systems (CPS), their permissiveness, efficient computability, and adaptability enables their use for the automated synthesis of certified interfaces among different interacting CPS. This paper
discusses the foundations and applications of this novel control-inspired distributed reactive synthesis framework for different cooperation and partial-observation settings common for interacting CPS.

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 and for accelerating heuristics for solving infinite program games.

Overview Paper:

  • ®A. Anand, S.P. Nayak, A.-K. Schmuck. Strategy Templates – Robust Certified Interfaces for Interacting Systems. 2024. ATVA’24 (invited paper) (PDF)

Core Group Members Involved:

Tools:

  • CoSMo : Contracted Strategy Mask Negotiation in two-objective parity games [GitHub]
  • 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.