Linear-time Temporal Logic with Event Freezing Functions

TL;DR

This paper introduces a new temporal logic with event freezing functions that enhances the formal specification of system properties, supporting various time models and SMT-based verification, aiming for a balance of simplicity and expressiveness.

Contribution

It proposes a novel extension of First-Order Linear-time Temporal Logic with Past, adding 'at next' and 'at last' operators for better formalization of component-based system properties.

Findings

Supports discrete, dense, and super-dense time models.

Enables encoding of metric temporal operators with counting.

Provides SMT-based model checking implementation.

Abstract

Formal properties represent a cornerstone of the system-correctness proofs based on formal verification techniques such as model checking. Formalizing requirements into temporal properties may be very complex and error prone, due not only to the ambiguity of the textual requirements but also to the complexity of the formal language. Finding a property specification language that balances simplicity, expressiveness, and tool support remains an open problem in many real-world contexts. In this paper, we propose a new temporal logic, which extends First-Order Linear-time Temporal Logic with Past adding two operators "at next" and "at last", which take in input a term and a formula and represent the value of the term at the next state in the future or last state in the past in which the formula holds. We consider different models of time (including discrete, dense, and super-dense time) and Satisfiability Modulo Theories (SMT) of the first-order formulas. The "at next" and "at last" functions can be seen as a generalization of Event-Clock operators and can encode some Metric Temporal operators also with counting. They are useful to formalize properties of component-based models because they allow to express constraints on the data exchanged with messages at different instants of time. We provide a simple encoding into equisatisfiable formulas without the extra functional symbols. We implement a prototype tool support based on SMT-based model checking.