Många problem i formella metoder kan formaliseras som tvåspelarspel. För flera tillämpningar — programsyntes, till exempel — förutom att bestämma vilken spelare som vinner spelet, är vi intresserade av att beräkna en vinnande strategi för den spelaren. I detta dokument studeras strategisyntesproblemen för spel som definieras inom teorin om linjär rationell aritmetik. Två typer av spel beaktas. Ett tillfredsställande spel, som beskrivs av en kvantifierad formel, spelas av två spelare som turas om att ögonblickligen kvantifierar. Målet för varje spelare är att bevisa (eller motbevisa) tillfredsställelse av formeln. Ett lättillgängligt spel, som beskrivs av ett par formler som definierar de juridiska dragen för varje spelare, spelas av två spelare som turas om att välja positioner —rationella vektorer av någon fast dimension. Målet för varje spelare är att nå en position där den motsatta spelaren inte har några lagliga drag (eller att spela spelet för alltid). Vi ger en komplett algoritm för att syntetisera vinnande strategier för satisfiability spel och en ljud (men nödvändigtvis ofullständig) algoritm för att syntetisera vinnande strategier för nåbarhet spel.  Logiska spel är tvåspelarspel där spelets regler definieras av logiska formler. Computing vinnande strategier för logiska spel har flera tillämpningar i formella metoder, särskilt i verifiering och syntes av program. I detta dokument presenteras algoritmer för beräkning av vinnande strategier för linjära aritmetiska spel, där spelets rörelser definieras genom linjära (rationella eller heltal) aritmetiska formler. I detta dokument behandlas två klasser av linjära aritmetiska spel, nämligen tillfredsställande spel och tillgänglighetsspel. Vi fokuserar på logiska spel modulo teorin om linjär rationell aritmetik, både på grund av den genomgripande användningen av denna teori i formella metoder och det faktum att det är relativt väl förstådd. En kvantifierad formel kan betraktas som ett tillfredsställande spel mellan två spelare SAT och UNSAT: SAT kontrollerar de existentiella kvantifieringarna och syftar till att bevisa att formeln är tillfredsställande, medan UNSAT kontrollerar de universella kvantifieringarna och syftar till att bevisa formeln otillfredsställande [Hintikka 1982]. En vinnande strategi för SAT är en algoritm för att välja värden för existentiellt kvantifierade variabler baserat på de tidigare val som gjorts av UNSAT-spelaren, så att efter alla val har gjorts för båda spelarna, formeln utvärderar till sant. Dubbelt, en vinnande strategi för UNSAT spelaren är en algoritm för att välja värden av universellt kvantifierade variabler för att göra formeln utvärdera till falskt. Tillämpningar av tillfredsställande spel inkluderar:
En tredje inställning med en decibel syntes resultat över obundna domäner är arbete med strategisyntes för linjär aritmetisk tillfredsställelse spel REF.
Strategy synthesis for linear arithmetic games
{'venue': 'PACMPL', 'journal': None, 'mag_field_of_study': ['Computer Science']}