Uniform Strategies
Résumé
We consider turn-based game arenas for which we investigate uniformity properties of strategies. These properties involve bundles of plays, that arise from some semantical motive. Typically, we can represent constraints on allowed strategies, such as being observation-based. We propose a formal language to specify uniformity properties and demonstrate its relevance by rephrasing various known problems from the literature. Note that the ability to correlate different plays cannot be achieved by any branching-time logic if not equipped with an additional modality, so-called R in this contribution. We also study an automated procedure to synthesize strategies subject to a uniformity property, which strictly extends existing results based on, say standard temporal logics. We exhibit a generic solution for the synthesis problem provided the bundles of plays rely on any binary relation definable by a finite state transducer. This solution yields a non-elementary procedure.
Nous considérons des arènes de jeux pour lesquelles nous étudions des propriétés d'uniformité des stratégies. Ces propriétés font intervenir des ensembles de parties, qui émer- gent d'une quelconque motivation sémantique. Typiquement, nous pouvons représenter des con- traintes sur les stratégies autorisées, comme par exemple être observationnelles. Nous proposons un language formel pour spécifier les propriétés d'uniformité et démontrons sa pertinence en re- formulant divers problèmes connus de la littérature. Noter que la capacité à corréler différentes parties ne peut être obtenue par aucune logique du temps arborescent à moins de l'équiper d'une modalité supplémentaire, appelée R dans cette contribution. Nous étudions aussi une procé- dure de synthèse automatique de stratégies soumises à une propriété d'uniformité, qui étend strictement les résultats existants basés sur la logique temporelle standard. Nous proposons une solution générique pour le problème de la synthèse dans le cas où les ensembles de parties sont caractérisés par une relation binaire définissable par un transducteur fini. Cette solution donne une procédure non-élémentaire.
Origine : Fichiers produits par l'(les) auteur(s)