Name
Abstract | ||
|---|---|---|
Introduce a simple game-theoretic approach to satisfiability checking of temporal logic, for LTL (linear time logic) and CTL (computation tree logic), which has the same complexity as using automata. The mechanisms involved are both explicit and transparent, and underpin a novel approach to developing complete axiom systems for temporal logic. The axiom systems are naturally factored into what happens locally and what happens in the limit. The completeness proofs utilise the game-theoretic construction for satisfiability: if a finite set of formulas is consistent then there is a winning strategy (and therefore construction of an explicit model is avoided) |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1109/LICS.2001.932511 | Boston, MA |
Keywords | Field | DocType |
novel approach,simple game theoretic approach,temporal logic,explicit model,complete axiom system,winning strategy,completeness proof,game theoretic construction,focus games,finite set,axiom system,computability,logic,computation tree logic,impedance,testing,complexity,satisfiability,automata,completeness,computational complexity,ctl,informatics,game theory,calculus | Computation tree logic,Discrete mathematics,Computational logic,Combinatorics,Temporal logic of actions,Interval temporal logic,Computer science,Multimodal logic,Linear temporal logic,Temporal logic,Intermediate logic | Conference |
ISSN | ISBN | Citations |
1043-6871 | 0-7695-1281-X | 22 |
PageRank | References | Authors |
1.14 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Lange | 1 | 22 | 1.14 |
| Colin Stirling | 2 | 934 | 102.50 |