Counting STaRS · Counting STrategies and Reactive Synthesis

Lines connect the coordinator with its partners.

Project objective

We are surrounded by reactive systems, such as traffic-light systems, which interact continuously with the environment. A controller for reactive systems tells the system how to react to changes in the environment. A controller also needs to satisfy an objective modeling the requirements of the system. For safety-critical systems, the consequences of designing incorrect controllers can be fatal. This motivates the synthesis of provably correct controllers for reactive systems. A popular formal methods approach for reactive synthesis relies on game-theoretic tools. The interaction between the controller and the environment is modeled as a two-player game, and designing a controller amounts to computing a winning strategy for the controller. The memory requirement of the winning strategy is crucial, as smaller memory corresponds to simpler controllers. Several objectives, such as parity or mean-payoff, do not require additional memory in winning strategies. In general, objectives for which winning strategies require finite memory is well understood theoretically and several tools support synthesis for such objectives. However, strategies for multi-objective games, which model requirements more realistically, may require an exponential or infinite amount of memory, such as for multi energy and multi mean-payoff games. While infinite-memory strategies may seem unreasonable for implementation, data structures like counters are widely used to model variable ranging over an unbounded domain in programming. Simple data structures, such as counters can also be used for succinct and explainable representations of a subclass of exponential-memory and infinite-memory strategies. This project will undertake a systematic study of objectives for which counter-based strategies suffice and study the feasibility of counter-based strategies for synthesis.

Original text from CORDIS.

Participants

• UNIVERSITE DE MONS · MonsCoordinatorBelgium

Links

• View on CORDIS
• DOI: 10.3030/101285726