Model Checking Temporal Stream Logic and Hyper-Temporal Stream Logic
Janine Lohse
In this thesis, we develop model checking algorithms for both Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL). TSL extends Linear Temporal Logic (LTL) with predicates over inputs and memory cells, and with update terms that specify how the value of a memory cell should change. Similar to the extension of LTL to HyperLTL, HyperTSL further extends TSL for the specification of hyperproperties, that is, properties relating multiple system executions. Unlike HyperLTL, HyperTSL can express many important security properties like noninterference even if there is an infinite data domain. Both TSL and HyperTSL were originally defined for synthesis – to the best of our knowledge, there is no algorithm explicitly designed for model checking yet. We first study the decidable case of (Hyper)TSL model checking of finite-state systems. We show that in this case, (Hyper)TSL is not more expressive than (Hyper)LTL by giving a translation algorithm. Still, many properties can be expressed more compactly using (Hyper)TSL. Thus, we also develop direct model checking algorithms for TSL and HyperTSL with at most one quantifier alternation that are more efficient than model checking an equivalent HyperLTL formula. Next, we study (Hyper)TSL model checking of infinite-state systems, which is called software model checking. We extend a known LTL software model checking algorithm to TSL and, by applying the technique of self-composition, to alternation-free Hyper-TSL. We further extend this algorithm to an algorithm for finding counterexamples for ∀∗∃∗ HyperTSL formulas (or, dually, witnesses of ∃∗∀∗ HyperTSL formulas) that is sound but not complete. This also gives the, to the best of our knowledge, first infinite-state software model checking algorithm for finding counterexamples for ∀∗∃∗ and witnesses for ∃∗∀∗ HyperLTL formulas.
Bachelor Thesis.