Name
Abstract | ||
|---|---|---|
Focus games have been shown to yield game-theoretical characterisations for the satisfiability and the model checking problem for various temporal logics. One of the players is given a tool - the focus - that enables him to show the regeneration of temporal operators characterised as least or greatest fixpoints. His strategy usually is build upon a priority list of formulas and, thus, is not positional. This paper defines foci games for satisfiability of LTL formulas. Strategies in these games are trivially positional since they parallelise all of the focus player's choices, thus resulting in a 1-player game in effect. The games are shown to be correct and to yield smaller (counter-)models than the focus games. Finally, foci games for model checking LTL are defined as well. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.entcs.2004.07.007 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
temporal logic,foci game,various temporal logic,model checking,1-player game,ltl satisfiability,tool support,verification,game-theoretical characterisations,temporal operator,focus game,greatest fixpoints,model checking problem,ltl formula,foci approach,focus player,satisfiability | Discrete mathematics,Model checking,Computer science,Satisfiability,Theoretical computer science,Operator (computer programming),Temporal logic | Journal |
Volume | Issue | ISSN |
119 | 1 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
2 | 0.55 | 12 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christian Dax | 1 | 42 | 3.86 |
| Martin Lange | 2 | 44 | 4.03 |