2016/10/22 by Yannick Lebrun, Lebrun, Yannick, Raphaël Khoury +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.1610.07080
openalex publication_date 2016/10/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper we give automata-based representation of LTL-FO+ properties. LTL-FO+ is an extension of LTL that includes first-order quantification over bounded variable, thus greatly increasing the expressivity of the language. An automata representation of this formalism allows greater ease in writing and understanding properties, as well as in performing manipulations, such as negation or emptiness checking. The automata representation of an LTL-FO+ formula has finite size regardless of the domain of quantified variables, and the number of states that is linear in the size of the property.