Simple LTL Model Checking on Finite and Infinite Traces over Concrete Domains

There exist different semantics for Linear Temporal Logic (LTL) in terms of finiteness of the considered traces. Although several ones can be useful depending on the verification context, no verification framework handle their diversity in a simple way. Another limitation of current LTL verification tools is the treatment of concrete domains (bounded and infinite integers, real numbers, etc.). We present an approach to LTL model checking on both finite and infinite traces with concrete domains. Our method is based on an SMT solver and on Bounded Model Checking (BMC). We also present some experiments and compare our tool with NuSMV and nuXmv.