Feng, Shiguang; Carapelle, Claudia; Gil, Oliver Fernández; Quaas, Karin MTL and TPTL for one-counter machines. Expressiveness, model checking, and satisfiability. (English) Zbl 1433.68215 ACM Trans. Comput. Log. 21, No. 2, Article No. 12, 34 p. (2020). MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 03B25 Decidability of theories and sets of sentences 03B44 Temporal logic Keywords:Ehrenfeucht-Fraïssé games; Freeze LTL; one-counter machines; data words; metric temporal logic; timed propositional temporal logic PDFBibTeX XMLCite \textit{S. Feng} et al., ACM Trans. Comput. Log. 21, No. 2, Article No. 12, 34 p. (2020; Zbl 1433.68215) Full Text: DOI