Symbolic Synthesis of Non-Negative Multi-Weighted Games with Temporal Objectives
Authors
Nielsen, Søren Moss ; Jensen, Lasse Steen ; Kaufmann, Isabella
Term
4. term
Education
Publication year
2017
Abstract
Denne afhandling undersøger automatisk controllersyntese i tospiller-spil med ikke-negative, multi-vægtede overgange og temporale mål. Vi introducerer n-vægtede Kripke-strukturer og en vægtet udvidelse af CTL (WCTL) til at specificere forgrenet tid med sammenligninger og aritmetik over flere diskrete vægtdimensioner. Vi viser, at modeltjek af WCTL over multi-vægtede Kripke-strukturer er uafgørligt med tre vægte, og definerer en afgørlig sublogik, Constant Bound WCTL (cb-WCTL). Med fokus på reachability-objektiver præsenterer vi algoritmer, der bruger en symbolsk repræsentation af akkumulerede vægte (zoner) til at syntetisere finit-hukommelsesstrategier: for mål med kun øvre grænser er problemet afgørligt i pseudo-polynomiel tid, og med både nedre og øvre grænser er det NP-hårdt men afgørligt i eksponentiel tid. Vi beviser korrekthed af de symbolske operationer, identificerer hvornår finit hukommelse er tilstrækkelig, og diskuterer begrænsninger for nestede cb-WCTL-operatorer og mulige udvidelser. Tilgangen illustreres med et spilbaseret eksempel på en forsikringsagent.
This thesis studies automatic controller synthesis in two-player games with non-negative, multi-weighted transitions and temporal objectives. We introduce n-weighted Kripke structures and a weighted extension of CTL (WCTL) to specify branching-time properties with comparisons and arithmetic over multiple discrete weight dimensions. We show that model checking WCTL over multi-weighted Kripke structures is undecidable with three weights and define a decidable sub-logic, Constant Bound WCTL (cb-WCTL). Focusing on reachability objectives, we present algorithms that use a symbolic representation of accumulated weights (zones) to synthesize finite-memory strategies: for objectives with only upper bounds the problem is decidable in pseudo-polynomial time, and with both lower and upper bounds it is NP-hard but decidable in exponential time. We prove correctness of the symbolic operations, establish when finite memory suffices, and discuss limitations for nested cb-WCTL operators and potential extensions. The approach is illustrated with a game-based insurance example.
[This summary has been generated with the help of AI directly from the project (PDF)]
Documents
Other projects by the authors
Nielsen, Søren Moss:
Jensen, Lasse Steen:
Kaufmann, Isabella: