Temporal Stream Logic modulo Theories
share
Temporal Stream Logic (TSL) is a temporal logic that extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive enough. In TSL, functions and predicates are uninterpreted. In this paper, we investigate the satisfiability problem of TSL both with respect to the standard underlying theory of uninterpreted functions and with respect to other theories such as Presburger arithmetic. We present an algorithm for checking the satisfiability of a TSL formula in the theory of uninterpreted functions and evaluate it on different benchmarks: It scales well and is able to validate assumptions in a real-world system design. The algorithm is not guaranteed to terminate. In fact, we show that TSL satisfiability is highly undecidable in the theories of uninterpreted functions, equality, and Presburger arithmetic, proving that no complete algorithm exists. However, we identify three fragments of TSL for which the satisfiability problem is (semi-)decidable in the theory of uninterpreted functions.
READ FULL TEXT