Temporal Stream Logic modulo Theories (Full Version)
Bernd Finkbeiner, Philippe Heim, Noemi Passing

TL;DR
This paper extends Temporal Stream Logic with first-order theories, explores its satisfiability complexity, and proposes a semi-decision procedure that scales well for real-world system validation.
Contribution
It introduces first-order theories into TSL, analyzes satisfiability complexities, and develops a practical semi-decision algorithm for system design validation.
Findings
TSL satisfiability is highly undecidable in general.
Identifies decidable fragments of TSL for uninterpreted functions.
Proposes a scalable semi-decision algorithm that performs well in practice.
Abstract
Temporal stream logic (TSL) 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 the semantics of TSL, functions and predicates are left uninterpreted. In this paper, we extend TSL with first-order theories, enabling us to specify systems using interpreted functions and predicates such as incrementation or equality. We investigate the satisfiability problem of TSL modulo the standard underlying theory of uninterpreted functions as well as with respect to Presburger arithmetic and the theory of equality: For all three theories, TSL satisfiability is highly undecidable. Nevertheless, we identify three fragments of TSL for which the satisfiability problem is (semi-)decidable in the theory of uninterpreted functions. Despite the high undecidability, we present an algorithm - which…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Formal Methods in Verification · Semantic Web and Ontologies
