 A variation of LTL with useful applications for specifying and reasoning about concurrent systems is Lamport’s (1994) temporal logic of actions TLA. Other applications of temporal logics in computer science include: temporal databases, real-time processes and systems, hardware verification, etc. Further information on such applications can be found in e.g. Pnueli (1977); Emerson and Clarke (1982); Moszkowski (1983); Galton (1987); Emerson (1990); Alur and Henzinger (1992); Lamport (1994); Vardi and Wolper (1994); Bolc and Szalas (1995); Gabbay et al. (2000); Baier and Katoen (2008); Kröger and Merz (2008); Fisher (2011); Demri et al. (2016).