AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

In this work, we propose to extend First-Order Linear-time Temporal
Logic with Past by adding two operators "at next" and "at last", which
take in input a term and a formula and return the value of the term at
the next state in the future or last state in the past in which the
formula holds. The new logic, named LTL-EF, can be interpreted with
different models of time (including discrete, dense, and super-dense
time) and with different first-order theories (à la Satisfiability
Modulo Theories (SMT)). We show that the new operators can encode a
useful fragment of (first-order) Metric Temporal Logic with counting. We
provide rewriting procedures to reduce the satisfiability problem to the
discrete-time case (to leverage on the mature state-of-the-art
corresponding verification techniques) and to remove the extra
functional symbols. We implemented these techniques in the nuXmv model
checker, enabling the analysis of LTL-EF with SMT-based model checking
algorithms. We show the feasibility of the approach by experimenting
with several non-trivial valid and satisfiable formulas.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only