We consider First-Order Linear Temporal Logic (FO-LTL) over linear time. Inspired by the success of formal approaches based upon finite-model finders, such as Alloy, we focus on finding models with finite first-order domains for FO-LTL formulas, while retaining an infinite time domain. More precisely, we investigate the complexity of the following problem: given a formula φ and an integer n, is there a model of φ with domain of cardinality at most n? We show that depending on the logic considered (FO or FO-LTL) and on the precise encoding of the problem, the problem is either NP-complete, NEXPTIME-complete, PSPACEcomplete or EXPSPACE-complete. In a second part, we exhibit cases where the Finite Model Property can be lifted from fragments of FO to their FO-LTL extension.
CITATION STYLE
Kuperberg, D., Brunel, J., & Chemouil, D. (2016). On finite domains in first-order linear temporal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9938 LNCS, pp. 211–226). Springer Verlag. https://doi.org/10.1007/978-3-319-46520-3_14
Mendeley helps you to discover research relevant for your work.