A synthesis method for zero-sum mean-payoff asynchronous probabilistic games.

Area of Science:

• Computer Science
• Artificial Intelligence
• Formal Methods

Background:

• Traditional reactive synthesis focuses on qualitative objectives (e.g., Linear Temporal Logic specifications).
• Quantitative synthesis problems, like mean-payoff objectives, have gained significant attention.
• System designers increasingly require synthesized systems to meet resource constraints and performance metrics.

Purpose of the Study:

• To address the combined quantitative and qualitative objectives in reactive synthesis.
• To propose a framework for synthesizing systems that optimize expected mean payoffs while satisfying Linear Temporal Logic winning conditions.
• To investigate the synthesis problem for Generalized Reactivity(1) (GR(1)) formulas within a probabilistic environment.

Main Methods:

• Introduction of zero-sum mean-payoff asynchronous probabilistic games.
• Development of two symbolic algorithms with polynomial time complexity for calculating expected mean payoffs.
• Utilization of uniform random strategies within the proposed algorithms.
• Integration of system winning probabilities to refine payoff calculations.

Main Results:

• The proposed algorithms efficiently calculate expected mean payoffs for systems with combined objectives.
• The algorithms demonstrate convergence and controlled volatility in experimental evaluations.
• A method is established to compute expected mean payoffs considering the probability of system success.

Conclusions:

• The presented work offers a significant advancement in reactive synthesis by integrating quantitative and qualitative goals.
• The developed algorithms provide efficient solutions for complex synthesis problems with probabilistic elements.
• Experimental validation confirms the practical applicability and performance of the proposed algorithms.