George Boolos showed that GLP remains sound and complete with analysis (second-order arithmetic) in the  role of the base theory "T". GLP has been shown to be incomplete with respect to any class of Kripke frames. A natural topological semantics of GLP interprets  modalities as derivative operators of a polytopological space. Such spaces are called  GLP-spaces whenever they satisfy all the axioms of GLP. GLP is complete w.r.t. the class  of all GLP-spaces. The problem of being a theorem of GLP is PSPACE-complete. So is the same problem restricted to only  variable-free formulas of GLP. GLP, under the name GP, was introduced by Giorgi Japaridze in his PhD thesis  "Modal Logical Means of Investigating Provability" (Moscow State University, 1986) and  published two years later along with (a) the completeness theorem for GLP with respect to its provability interpretation (Beklemishev subsequently came up with a simpler proof of the same theorem) and (b) a proof that Kripke frames for GLP do not exist. Beklemishev also conducted a more extensive  study of Kripke models for GLP. Topological models for GLP were studied by Beklemishev, Bezhanishvili, Icard and Gabelaia. The decidability of GLP in polynomial space was proven by I. Shapirovsky, and the PSPACE-hardness of its variable-free fragment  was proven by F.Pakhomov. Among the most notable applications of GLP has been its use in proof-theoretically analyzing Peano arithmetic,  elaborating a canonical way for recovering ordinal notation system up to 0 from the corresponding algebra, and  constructing simple combinatorial independent statements (Beklemishev ). An extensive survey of GLP in the context of provability logics in general was given by George Boolos in his book “The Logic of Provability”.