Model Checking Temporal Stream Logic and Hyper-Temporal Stream Logic
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 speciﬁcation 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 inﬁnite data domain. Both TSL and HyperTSL were originally deﬁned for synthesis – to the best of our knowledge, there is no algorithm explicitly designed for model checking yet. We ﬁrst study the decidable case of (Hyper)TSL model checking of ﬁnite-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 quantiﬁer alternation that are more eﬃcient than model checking an equivalent HyperLTL formula. Next, we study (Hyper)TSL model checking of inﬁnite-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 ﬁnding 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, ﬁrst inﬁnite-state software model checking algorithm for ﬁnding counterexamples for ∀∗∃∗ and witnesses for ∃∗∀∗ HyperLTL formulas.