CISPA
Browse
cispa_all_3606.pdf (320.66 kB)

Temporal Stream Logic modulo Theories

Download (320.66 kB)
conference contribution
posted on 2023-11-29, 18:20 authored by Bernd FinkbeinerBernd Finkbeiner, Philippe HeimPhilippe Heim, Noemi Passing
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 neither semi-decidable nor co-semi-decidable. Nevertheless, we identify three fragments of TSL for which the satisfiability problem is (semi-)decidable in the theory of uninterpreted functions. Despite the undecidability, we present an algorithm – which is not guaranteed to terminate – for checking the satisfiability of a TSL formula in the theory of uninterpreted functions and evaluate it: It scales well and is able to validate assumptions in a real-world system design.

History

Preferred Citation

Bernd Finkbeiner, Philippe Heim and Noemi Passing. Temporal Stream Logic modulo Theories. In: European Joint Conference on Theory and Practice of Software (ETAPS) (ETAPS). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

European Joint Conference on Theory and Practice of Software (ETAPS) (ETAPS)

Legacy Posted Date

2022-04-26

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3606, title = "Temporal Stream Logic modulo Theories", author = "Finkbeiner, Bernd and Heim, Philippe and Passing, Noemi", booktitle="{European Joint Conference on Theory and Practice of Software (ETAPS) (ETAPS)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC