Constraint-Based Monitoring of Hyperproperties

TL;DR

This paper presents a novel runtime monitoring approach for hyperproperties using HyperLTL and Boolean constraints, enabling efficient detection of violations through satisfiability checks.

Contribution

It introduces a constraint-based monitoring method for hyperproperties, leveraging BDDs or SAT solvers, improving over automata-based techniques.

Findings

Efficient detection of hyperproperty violations at runtime.

Comparison shows advantages over existing automata-based tools.

Framework supports complex hyperproperties like non-interference.

Abstract

Verifying hyperproperties at runtime is a challenging problem as hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. It is necessary to store previously seen traces, because every new incoming trace needs to be compatible with every run of the system observed so far. Furthermore, the new incoming trace poses requirements on future traces. In our monitoring approach, we focus on those requirements by rewriting a hyperproperty in the temporal logic HyperLTL to a Boolean constraint system. A hyperproperty is then violated by multiple runs of the system if the constraint system becomes unsatisfiable. We compare our implementation, which utilizes either BDDs or a SAT solver to store and evaluate constraints, to the automata-based monitoring tool RVHyper.

Figures

Tables

Table 1. Table 1 : Average results of our implementation compared to RVHyper on traces generated from circuit instances. Every instance was run 10 10 10 times.

instance	# traces	length	time RVHyper	time SAT	time BDD
xor1	19	5	12ms	47ms	49ms
xor2	1000	5	16913ms	996ms	1666ms
counter1	961	20	9610ms	8274ms	303ms
counter2	1353	20	19041ms	13772ms	437ms
mux1	1000	5	14924ms	693ms	647ms
mux2	80	5	121ms	79ms	81ms

Equations

$$\{a\}$$

$$\{\}$$

$$\phi$$

$$\psi$$

$$\begin{array}[]{ll}\Pi_{\mathit{fin}}\vDash_{\_}Ta_{\_}\pi&\text{if }a\in\Pi_{\mathit{fin}}(\pi)[0]\\ \Pi_{\mathit{fin}}\vDash_{\_}T\neg\varphi&\text{if }\Pi_{\mathit{fin}}\nvDash_{\_}T\varphi\\ \Pi_{\mathit{fin}}\vDash_{\_}T\varphi\lor\psi&\text{if }\Pi_{\mathit{fin}}\vDash_{\_}T\varphi\text{ or }\Pi_{\mathit{fin}}\vDash_{\_}T\psi\\ \Pi_{\mathit{fin}}\vDash_{\_}T\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi&\text{if }\forall t\in\Pi_{\mathit{fin}}\mathpunct{.}|t|>1\text{ and }\Pi_{\mathit{fin}}[1\rangle\vDash_{\_}T\varphi\\ \Pi_{\mathit{fin}}\vDash_{\_}T\varphi\operatorname{\mathcal{U}}\psi&\text{if }\exists i<\min\nolimits_{\_}{t\in\Pi_{\mathit{fin}}}|t|\mathpunct{.}\Pi_{\mathit{fin}}[i\rangle\vDash_{\_}T\psi\land\forall j<i\mathpunct{.}\Pi_{\mathit{fin}}[j\rangle\vDash_{\_}T\varphi\\ \Pi_{\mathit{fin}}\vDash_{\_}T\exists\pi\mathpunct{.}\varphi&\text{if there is some }t\in T\text{ such that }\Pi_{\mathit{fin}}[\pi\mapsto t]\vDash_{\_}T\varphi\\ \Pi_{\mathit{fin}}\vDash_{\_}T\forall\pi\mathpunct{.}\varphi&\text{if for all }t\in T\text{ such that }\Pi_{\mathit{fin}}[\pi\mapsto t]\vDash_{\_}T\varphi\end{array}$$

$$\begin{array}[]{ll}\mathcal{L}^{\pi}_{t}(\varphi)&\mathrel{\coloneqq}\left\{t^{\prime}\in\Sigma^{+}|\left\{\pi\mapsto t,\pi^{\prime}\mapsto t^{\prime}\right\}_{\_}\mathit{fin}\vDash\varphi\right\}\\ \mathcal{L}^{\pi^{\prime}}_{t}(\varphi)&\mathrel{\coloneqq}\left\{t^{\prime}\in\Sigma^{+}|\left\{\pi\mapsto t^{\prime},\pi^{\prime}\mapsto t\right\}_{\_}\mathit{fin}\vDash\varphi\right\}\\ \mathcal{L}_{t}(\varphi)&\mathrel{\coloneqq}\mathcal{L}^{\pi}_{t}(\varphi)\cap\mathcal{L}^{\pi^{\prime}}_{t}(\varphi)\\ \end{array}$$

$$\displaystyle\begin{array}[]{lcllcl}a_{\_}\pi|^{\pi}_{t}&\coloneqq&\begin{cases}\top&\text{if }a\in t[0]\\ \bot&\text{otherwise}\\ \end{cases}&\neg a_{\_}\pi|^{\pi}_{t}&\coloneqq&\begin{cases}\top&\text{if }a\notin t[0]\\ \bot&\text{otherwise}\\ \end{cases}\\ a_{\_}{\pi^{\prime}}|^{\pi}_{t}&\coloneqq&a&\neg a_{\_}{\pi^{\prime}}|^{\pi}_{t}&\coloneqq&\neg a\\ (\varphi\lor\psi)|^{\pi}_{t}&\coloneqq&\varphi|^{\pi}_{t}\lor\psi|^{\pi}_{t}&(\varphi\land\psi)|^{\pi}_{t}&\coloneqq&\varphi|^{\pi}_{t}\land\psi|^{\pi}_{t}\end{array}$$

$$\displaystyle\begin{array}[]{lcl}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)|^{\pi}_{t}&\coloneqq&\begin{cases}\bot&\text{if }|t|\leq 1\\ \operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi|^{\pi}_{t[1\rangle}&\text{otherwise}\\ \end{cases}\\ (\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)|^{\pi}_{t}&\coloneqq&\begin{cases}\top&\text{if }|t|\leq 1\\ \operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi|^{\pi}_{t[1\rangle}&\text{otherwise}\\ \end{cases}\\ (\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t}&\coloneqq&\begin{cases}\psi|^{\pi}_{t}&\text{if }|t|\leq 1\\ \psi|^{\pi}_{t}\lor(\varphi|^{\pi}_{t}\land\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t[1\rangle}))&\text{otherwise}\\ \end{cases}\\ (\varphi\operatorname{\mathcal{R}}\psi)|^{\pi}_{t}&\coloneqq&\begin{cases}\psi|^{\pi}_{t}&\text{if }|t|\leq 1\\ \psi|^{\pi}_{t}\land(\varphi|^{\pi}_{t}\lor\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((\varphi\operatorname{\mathcal{R}}\psi)|^{\pi}_{t[1\rangle}))&\text{otherwise}\\ \end{cases}\\ \end{array}$$

$$\displaystyle\begin{array}[]{lcllcl}a_{\_}\pi[\pi,e,i]&\coloneqq&\begin{cases}\top&\text{if }a\in e\\ \bot&\text{otherwise}\\ \end{cases}&(\neg a_{\_}\pi)[\pi,e,i]&\coloneqq&\begin{cases}\top&\text{if }a\notin e\\ \bot&\text{otherwise}\\ \end{cases}\\ a_{\_}{\pi^{\prime}}[\pi,e,i]&\coloneqq&a_{\_}i&(\neg a_{\_}{\pi^{\prime}})[\pi,e,i]&\coloneqq&\neg a_{\_}i\\ (\varphi\lor\psi)[\pi,e,i]&\coloneqq&\varphi[\pi,e,i]\lor\psi[\pi,e,i]&(\varphi\land\psi)[\pi,e,i]&\coloneqq&\varphi[\pi,e,i]\land\psi[\pi,e,i]\\ (\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)[\pi,e,i]&\coloneqq&v^{-}_{\varphi,i+1}&(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)[\pi,e,i]&\coloneqq&v^{+}_{\varphi,i+1}\end{array}$$

$$\displaystyle\begin{array}[]{lcl}(\varphi\operatorname{\mathcal{U}}\psi)[\pi,e,i]&\coloneqq&\psi[\pi,e,i]\lor(\varphi[\pi,e,i]\land v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,i+1})\\ (\varphi\operatorname{\mathcal{R}}\psi)[\pi,e,i]&\coloneqq&\psi[\pi,e,i]\land(\varphi[\pi,e,i]\lor v^{+}_{\varphi\operatorname{\mathcal{R}}\psi,i+1})\hskip 56.9055pt\mbox{}\end{array}$$

$$\begin{array}[]{ll}constr(v^{+}_{\varphi,i},\epsilon)&\mathrel{\coloneqq}\top\\ constr(v^{-}_{\varphi,i},\epsilon)&\mathrel{\coloneqq}\bot\\ constr(v_{\varphi,i},e\cdot t)&\mathrel{\coloneqq}\varphi[\pi,e,i]\land\bigwedge\limits_{\_}{v_{\psi,i+1}\in\varphi[\pi,e,i]}\Big{(}v_{\psi,i+1}\mathbin{\rightarrow}~{}constr(v_{\psi,i+1},t)\Big{)}\\ enc^{i}_{\text{AP}}(\epsilon)&\mathrel{\coloneqq}\top\\ enc^{i}_{\text{AP}}(e\cdot t)&\mathrel{\coloneqq}\bigwedge\limits_{\_}{a\in\text{AP}\cap e}a_{\_}i\quad\land\bigwedge\limits_{\_}{a\in\text{AP}\setminus e}\neg a_{\_}i\quad\land\quad enc^{i+1}_{\text{AP}}(t)\enspace,\end{array}$$

$$t^{\prime }\in \bigcap _{\_}t\in T{\mathcal{L}}_t(\phi )⟺en{c}_{\text{AP}}(t^{\prime })\models \underset{\_}{\bigwedge }t\in Tconstr(\hat{\phi },t).$$

Full text

1 Introduction

As today’s complex and large-scale systems are usually far beyond the scope of classic verification techniques like model checking or theorem proving, we are in the need of light-weight monitors for controlling the flow of information. By instrumenting efficient monitoring techniques in such systems that operate in an unpredictable privacy-critical environment, countermeasures will be enacted before irreparable information leaks happen. Information-flow policies, however, cannot be monitored with standard runtime verification techniques as they relate multiple runs of a system. For example, observational determinism [19, 21, 24] is a policy stating that altering non-observable input has no impact on the observable behavior. Hyperproperties [7] are a generalization of trace properties and are thus capable of expressing information-flow policies. HyperLTL [6] is a recently introduced temporal logic for hyperproperties, which extends Linear-time Temporal Logic (LTL) [20] with trace variables and explicit trace quantification. Observational determinism is expressed as the formula $\forall\pi,\pi^{\prime}\mathpunct{.}(\mathit{out}_{\_}{\pi}\leftrightarrow\mathit{out}_{\_}{\pi^{\prime}})\operatorname{\mathcal{W}}(\mathit{in}_{\_}{\pi}\nleftrightarrow\mathit{in}_{\_}{\pi^{\prime}})$, stating that all traces $\pi,\pi^{\prime}$ should agree on the output as long as they agree on the inputs.

In contrast to classic trace property monitoring, where a single run suffices to determine a violation, in runtime verification of HyperLTL formulas, we are concerned whether a set of runs through a system violates a given specification. In the common setting, those runs are given sequentially to the runtime monitor [1, 2, 12, 13], which determines if the given set of runs violates the specification. An alternative view on HyperLTL monitoring is that every new incoming trace poses requirements on future traces. For example, the event $\{\mathit{in},\mathit{out}\}$ in the observational determinism example above asserts that for every other trace, the output $\mathit{out}$ has to be enabled if $\mathit{in}$ is enabled. Approaches based on static automata constructions [1, 12, 13] perform very well on this type of specifications, although their scalability is intrinsically limited by certain parameters: The automaton construction becomes a bottleneck for more complex specifications, especially with respect to the number of atomic propositions. Furthermore, the computational workload grows steadily with the number of incoming traces, as every trace seen so far has to be checked against every new trace. Even optimizations [12], which minimize the amount of traces that must be stored, turn out to be too coarse grained as the following example shows. Consider the monitoring of the HyperLTL formula $\forall\pi,\pi^{\prime}.\operatorname{\leavevmode\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(a_{\_}\pi\rightarrow\neg b_{\_}{\pi^{\prime}})$, which states that globally if $a$ occurs on any trace $\pi$, then $b$ is not allowed to hold on any trace $\pi^{\prime}$, on the following incoming traces:

[TABLE]

In prior work [12], we observed that traces, which pose less requirements on future traces, can safely be discarded from the monitoring process. In the example above, the requirements of trace 1 are dominated by the requirements of trace 2, namely that $b$ is not allowed to hold on the first and second position of new incoming traces. Hence, trace 1 must not longer be stored in order to detect a violation. But with the proposed language inclusion check in [12], neither trace 2 nor trace 3 can be discarded, as they pose incomparable requirements. They have, however, overlapping constraints, that is, they both enforce $\neg b$ in the first step.

To further improve the conciseness of the stored traces information, we use rewriting, which is a more fine-grained monitoring approach. The basic idea is to track the requirements that future traces have to fulfill, instead of storing a set of traces. In the example above, we would track the requirement that $b$ is not allowed to hold on the first three positions of every freshly incoming trace. Rewriting has been applied successfully to trace properties, namely LTL formulas [17]. The idea is to partially evaluate a given LTL specification $\varphi$ on an incoming event by unrolling $\varphi$ according to the expansion laws of the temporal operators. The result of a single rewrite is again an LTL formula representing the updated specification, which the continuing execution has to satisfy. We use rewriting techniques to reduce $\forall^{2}$HyperLTL formulas to LTL constraints and check those constraints for inconsistencies corresponding to violations.

In this paper, we introduce a complete and provably correct rewriting-based monitoring approach for $\forall^{2}$HyperLTL formulas. Our algorithm rewrites a HyperLTL formula and a single event into a constraint composed of plain LTL and HyperLTL. For example, assume the event $\{\mathit{in},\mathit{out}\}$ while monitoring observational determinism formalized above. The first step of the rewriting applies the expansion laws for the temporal operators, which results in $(in_{\_}{\pi}\nleftrightarrow in_{\_}{\pi^{\prime}})\lor(out_{\_}{\pi}\leftrightarrow out_{\_}{\pi^{\prime}})\land\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((out_{\_}{\pi}\leftrightarrow out_{\_}{\pi^{\prime}})\operatorname{\mathcal{W}}(in_{\_}{\pi}\nleftrightarrow in_{\_}{\pi^{\prime}}))$. The event $\{in,out\}$ is rewritten for atomic propositions indexed by the trace variable $\pi$. This means replacing each occurrence of $in$ or $out$ in the current expansion step, i.e., before the $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ operator, with $\top$. Additionally, we strip the $\pi^{\prime}$ trace quantifier in the current expansion step from all other atomic propositions. This leaves us with $(\top\nleftrightarrow in)\lor(\top\leftrightarrow out)\land\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((out_{\_}{\pi}\leftrightarrow out_{\_}{\pi^{\prime}})\operatorname{\mathcal{W}}(in_{\_}{\pi}\nleftrightarrow in_{\_}{\pi^{\prime}}))$. After simplification we have $\neg in\lor out\land\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((out_{\_}{\pi}\leftrightarrow out_{\_}{\pi^{\prime}})\operatorname{\mathcal{W}}(in_{\_}{\pi}\nleftrightarrow in_{\_}{\pi^{\prime}}))$ as the new specification, which consists of a plain LTL part and a HyperLTL part. Based on this, we incrementally build a Boolean constraint system: we start by encoding the constraints corresponding to the LTL part and encode the HyperLTL part as variables. Those variables will then be incrementally defined when more elements of the trace become available. With this approach, we solely store the necessary information needed to detect violations of a given hyperproperty.

We evaluate two implementations of our approach, based on BDDs and SAT-solving, against RVHyper [13], a highly optimized automaton-based monitoring tool for temporal hyperproperties. Our experiments show that the rewriting approach performs equally well in general and better on a class of formulas which we call guarded invariants, i.e., formulas that define a certain invariant relation between two traces.

Related Work.

With the need to express temporal hyperproperties in a succinct and formal manner, the above mentioned temporal logics HyperLTL and HyperCTL* [6] have been proposed. The model-checking [6, 15, 14], satisfiability [9], and realizability problem [10] of HyperLTL  has been studied before.

Runtime verification of HyperLTL formulas was first considered for (co-)$k$-safety hyperproperties [1]. In the same paper, the notion of monitorability for HyperLTL was introduced. The authors have also identified syntactic classes of HyperLTL formulas that are monitorable and they proposed a monitoring algorithm based on a progression logic expressing trace interdependencies and the composition of an LTL${}_{\_}3$ monitor.

Another automata-based approach for monitoring HyperLTL formulas was proposed in [12]. Given a HyperLTL specification, the algorithm starts by creating a deterministic monitor automaton. For every incoming trace it is then checked that all combinations with the already seen traces are accepted by the automaton. In order to minimize the number of stored traces, a language-inclusion-based algorithm is proposed, which allows to prune traces with redundant information. Furthermore, a method to reduce the number of combination of traces which have to get checked by analyzing the specification for relations such as reflexivity, symmetry, and transitivity with a HyperLTL-SAT solver [9, 11], is proposed. The algorithm is implemented in the tool RVHyper [13], which was used to monitor information-flow policies and to detect spurious dependencies in hardware designs.

Another rewriting-based monitoring approach for HyperLTL is outlined in [5]. The idea is to identify a set of propositions of interest and aggregate constraints such that inconsistencies in the constraints indicate a violation of the HyperLTL formula. While the paper describes the building blocks for such a monitoring approach with a number of examples, we have, unfortunately, not been successful in applying the algorithm to other hyperproperties of interest, such as observational determinism.

In [3], the authors study the complexity of monitoring hyperproperties. They show that the form and size of the input, as well as the formula have a significant impact on the feasibility of the monitoring process. They differentiate between several input forms and study their complexity: a set of linear traces, tree-shaped Kripke structures, and acyclic Kripke structures. For acyclic structures and alternation-free HyperLTL formulas, the problems complexity gets as low as NC.

In [4], the authors discuss examples where static analysis can be combined with runtime verification techniques to monitor HyperLTL formulas beyond the alternation-free fragment. They discuss the challenges in monitoring formulas beyond this fragment and lay the foundations towards a general method.

2 Preliminaries

Let $\mathit{AP}$ be a finite set of atomic propositions and let $\Sigma=2^{\mathit{AP}}$ be the corresponding alphabet. An infinite trace $t\in\Sigma^{\omega}$ is an infinite sequence over the alphabet. A subset $T\subseteq\Sigma^{\omega}$ is called a trace property. A hyperproperty $H\subseteq 2^{(\Sigma^{\omega})}$ is a generalization of a trace property. A finite trace $t\in\Sigma^{+}$ is a finite sequence over $\Sigma$. In the case of finite traces, $|t|$ denotes the length of a trace. We use the following notation to access and manipulate traces: Let $t$ be a trace and $i$ be a natural number. $t[i]$ denotes the $i$-th element of $t$. Therefore, $t[0]$ represents the first element of the trace. Let $j$ be natural number. If $j\geq i$ and $i\geq|t|$, then $t[i,j]$ denotes the sequence $t[i]t[i+1]\cdots t[min(j,|t|-1)]$. Otherwise it denotes the empty trace $\epsilon$. $t[i\rangle$ denotes the suffix of $t$ starting at position $i$. For two finite traces $s$ and $t$, we denote their concatenation by $s\cdot t$.

HyperLTL Syntax.

HyperLTL [6] extends LTL with trace variables and trace quantifiers. Let $\mathcal{V}$ be a finite set of trace variables. The syntax of HyperLTL is given by the grammar

[TABLE]

where $a\in\mathit{AP}$ is an atomic proposition and $\pi\in\mathcal{V}$ is a trace variable. Atomic propositions are indexed by trace variables. The explicit trace quantification enables us to express properties like “on all traces $\varphi$ must hold”, expressed by $\forall\pi\mathpunct{.}\varphi$. Dually, we can express “there exists a trace such that $\varphi$ holds”, expressed by $\exists\pi\mathpunct{.}\varphi$. We use the standard derived operators release $\varphi\operatorname{\mathcal{R}}\psi\coloneqq\neg(\neg\varphi\operatorname{\mathcal{U}}\neg\psi)$, eventually $\operatorname{\leavevmode\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\coloneqq\mathit{true}\operatorname{\mathcal{U}}\varphi$, globally $\operatorname{\leavevmode\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\coloneqq\neg\operatorname{\leavevmode\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg\varphi$, and weak until $\varphi_{\_}1\operatorname{\mathcal{W}}\varphi_{\_}2\coloneqq(\varphi_{\_}1\operatorname{\mathcal{U}}\varphi_{\_}2)\vee\operatorname{\leavevmode\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi_{\_}1$. As we use the finite trace semantics, $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$ denotes the strong version of the next operator, i.e., if a trace ends before the satisfaction of $\varphi$ can be determined, the satisfaction relation, defined below, evaluates to false. To enable duality in the finite trace setting, we additionally use the weak next operator $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$ which evaluates to true if a trace ends before the satisfaction of $\varphi$ can be determined and is defined as $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\coloneqq\neg\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg\varphi$. We call $\psi$ of a HyperLTL formula $\vec{Q}.\psi$, with an arbitrary quantifier prefix $\vec{Q}$, the body of the formula. A HyperLTL formula $\vec{Q}.\psi$ is in the alternation-free fragment if either $\vec{Q}$ consists solely of universal quantifiers or solely of existential quantifiers. We also denote the respective alternation-free fragments as the $\forall^{n}$ fragment and the $\exists^{n}$ fragment, with $n$ being the number of quantifiers in the prefix.

Finite Trace Semantics.

We recap the finite trace semantics for HyperLTL [5] which is itself based on the finite trace semantics of LTL [18]. In the following, when using $\mathcal{L}(\varphi)$ we refer to the finite trace semantics of a HyperLTL formula $\varphi$. Let $\Pi_{\mathit{fin}}:\mathcal{V}\rightarrow\Sigma^{+}$ be a partial function mapping trace variables to finite traces. We define $\epsilon[0]$ as the empty set. $\Pi_{\mathit{fin}}[i\rangle$ denotes the trace assignment that is equal to $\Pi_{\mathit{fin}}(\pi)[i\rangle$ for all $\pi\in\mathrm{dom}(\Pi_{\mathit{fin}})$. By slight abuse of notation, we write $t\in\Pi_{\mathit{fin}}$ to access traces $t$ in the image of $\Pi_{\mathit{fin}}$. The satisfaction of a HyperLTL formula $\varphi$ over a finite trace assignment $\Pi_{\mathit{fin}}$ and a set of finite traces $T$, denoted by $\Pi_{\mathit{fin}}\vDash_{\_}T\varphi$, is defined as follows:

[TABLE]

Due to duality of $\operatorname{\mathcal{U}}$/$\operatorname{\mathcal{R}}$, $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$/$\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, $\exists$/$\forall$, and the standard Boolean operators, every HyperLTL formula $\varphi$ can be transformed into negation normal form (NNF), i.e., for every $\varphi$ there is some $\psi$ in negation normal form such that for all $\Pi_{\mathit{fin}}$ and $T$ it holds that $\Pi_{\mathit{fin}}\vDash_{\_}T\varphi$ if, and only if, $\Pi_{\mathit{fin}}\vDash_{\_}T\psi$. The standard LTL semantic, written $t\vDash_{\text{LTL}_{\mathit{fin}}}\varphi$, for some LTL formula $\varphi$ is equal to $\{\pi\mapsto t\}_{\_}\mathit{fin}\vDash_{\_}\emptyset\varphi^{\prime}$, where $\varphi^{\prime}$ is derived from $\varphi$ by replacing every proposition $p\in\mathit{AP}$ by $p_{\_}\pi$.

3 Rewriting HyperLTL

Given the body $\varphi$ of a $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$, and a finite trace $t\in\Sigma^{+}$, we define alternative language characterizations. These capture the intuitive idea that, if one fixes a finite trace $t$, the language of $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ includes exactly those traces $t^{\prime}$ that satisfy $\varphi$ in conjunction with $t$.

[TABLE]

We call $\hat{\varphi}\mathrel{\coloneqq}\varphi\land\varphi[\pi^{\prime}/\pi,\pi/\pi^{\prime}]$ the symmetric closure of $\varphi$, where $\varphi[\pi^{\prime}/\pi,\pi/\pi^{\prime}]$ represents the expression $\varphi$ in which the trace variables $\pi,\pi^{\prime}$ are swapped. The language of the symmetric closure, when fixing one trace variable, is equivalent to the language of $\varphi$.

Lemma 1

Given the body $\varphi$ of a $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$, and a finite trace $t\in\Sigma^{+}$, it holds that $\mathcal{L}^{\pi}_{t}(\hat{\varphi})=\mathcal{L}_{t}(\varphi)$.

Proof

$\mathcal{L}^{\pi}_{t}(\hat{\varphi})=\left\{t^{\prime}\in\Sigma^{+}|\left\{\pi\mapsto t,\pi^{\prime}\mapsto t^{\prime}\right\}_{\_}\mathit{fin}\vDash\hat{\varphi}\right\}$

\begin{array}[]{ll}&\hskip 25.40266pt=\left\{t^{\prime}\in\Sigma^{+}|\left\{\pi\mapsto t,\pi^{\prime}\mapsto t^{\prime}\right\}_{\_}\mathit{fin}\vDash\varphi\land\varphi[\pi^{\prime}/\pi,\pi/\pi^{\prime}]\right\}\\ &\hskip 25.40266pt=\left\{t^{\prime}\in\Sigma^{+}|\left\{\pi\mapsto t,\pi^{\prime}\mapsto t^{\prime}\right\}_{\_}\mathit{fin}\vDash\varphi,\left\{\pi\mapsto t,\pi^{\prime}\mapsto t^{\prime}\right\}_{\_}\mathit{fin}\vDash\varphi[\pi^{\prime}/\pi,\pi/\pi^{\prime}]\right\}\\ &\hskip 25.40266pt=\left\{t^{\prime}\in\Sigma^{+}|\left\{\pi\mapsto t,\pi^{\prime}\mapsto t^{\prime}\right\}_{\_}\mathit{fin}\vDash\varphi,\left\{\pi\mapsto t^{\prime},\pi^{\prime}\mapsto t\right\}_{\_}\mathit{fin}\vDash\varphi\right\}=\mathcal{L}_{t}(\varphi)\end{array}

We exploit this to rewrite a $\forall^{2}$HyperLTL formula into an LTL formula. We define the projection $\varphi|^{\pi}_{t}$ of the body $\varphi$ of a $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ in NNF and a finite trace $t\in\Sigma^{+}$ to an LTL formula recursively on the structure of $\varphi$:

[TABLE]

Theorem 3.1

Given a $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ and any two finite traces $t,t^{\prime}\in\Sigma^{+}$ it holds that $t^{\prime}\in\mathcal{L}^{\pi}_{t}(\varphi)\text{ if, and only if }t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t}$.

Proof

By induction on the size of $t$. Induction Base ($t=e$, where $e\in\Sigma$): Let $t^{\prime}\in\Sigma^{+}$ be arbitrarily chosen. We distinguish by structural induction the following cases over the formula $\varphi$. We begin with the base cases.

• •

$a_{\_}{\pi}$: we know by definition that $a_{\_}{\pi}|^{\pi}_{t}$ equals $\top$ if $a\in t[0]$ and $\bot$ otherwise, so it follows that $t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}a_{\_}{\pi}|^{\pi}_{t}\Leftrightarrow a\in t[0]\Leftrightarrow t^{\prime}\in\mathcal{L}^{\pi}_{t}(a_{\_}{\pi})$.

• •

$a_{\_}{\pi^{\prime}}$: $t^{\prime}\in\mathcal{L}^{\pi}_{t}(a_{\_}{\pi^{\prime}})\Leftrightarrow a\in t^{\prime}[0]\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}a\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}a_{\_}{\pi^{\prime}}|^{\pi}_{t}.$

• •

$\neg a_{\_}{\pi}$ and $\neg a_{\_}{\pi^{\prime}}$ are proven analogously.

The structural induction hypothesis states that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\in\mathcal{L}^{\pi}_{t}(\psi)\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}$ (SIH1) , where $\psi$ is a strict subformula of $\varphi$.

• •

$\varphi\lor\psi$: $t^{\prime}\in\mathcal{L}^{\pi}_{t}(\varphi\lor\psi)\Leftrightarrow(t^{\prime}\in\mathcal{L}^{\pi}_{t}(\varphi))\lor(t^{\prime}\in\mathcal{L}^{\pi}_{t}(\psi))\xLeftrightarrow{\text{SIH1}}(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t})\lor(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t})\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\lor\psi)|^{\pi}_{t}.$

• •

$\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$: $t^{\prime}\in\mathcal{L}^{\pi}_{t}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)\xLeftrightarrow{|t|=1}\bot\xLeftrightarrow{|t|=1}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)|^{\pi}_{t}$.

• •

$\varphi\operatorname{\mathcal{U}}\psi$: $t^{\prime}\in\mathcal{L}^{\pi}_{t}(\varphi\operatorname{\mathcal{U}}\psi)\xLeftrightarrow{|t|=1}t^{\prime}\in\mathcal{L}^{\pi}_{t}(\psi)\xLeftrightarrow{\text{SIH1}}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}\xLeftrightarrow{|t|=1}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t}.$

• •

$\varphi\wedge\psi$, $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$ and $\varphi\operatorname{\mathcal{R}}\psi$ are proven analogously.

Induction Step ($t=e\cdot t^{*}$, where $e\in\Sigma,t^{*}\in\Sigma^{+}$): The induction hypothesis states that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\in\mathcal{L}^{\pi}_{t^{*}}(\varphi)\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t^{*}}$ (IH). We make use of structural induction over $\varphi$. All cases without temporal operators are covered as their proofs above were independent of $|t|$. The structural induction hypothesis states for all strict subformulas $\psi$ that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\in\mathcal{L}^{\pi}_{t}(\psi)\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}$ (SIH2).

• •

$\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$: $t^{\prime}\in\mathcal{L}^{\pi}_{t^{*}}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)\xLeftrightarrow{|t^{*}|\geq 2}t^{\prime}[1\rangle\in\mathcal{L}^{\pi}_{t}(\varphi)\xLeftrightarrow{\text{IH}}t^{\prime}[1\rangle\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t}\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\varphi|^{\pi}_{t})\xLeftrightarrow{t^{*}=e\cdot t}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)|^{\pi}_{t^{*}}.$

• •

$\varphi\operatorname{\mathcal{U}}\psi$: $t^{\prime}\in\mathcal{L}^{\pi}_{t^{*}}(\varphi\operatorname{\mathcal{U}}\psi)\xLeftrightarrow{|t^{*}|\geq 2}(t^{\prime}\in\mathcal{L}^{\pi}_{t^{*}}(\psi))\lor(t^{\prime}\in\mathcal{L}^{\pi}_{t^{*}}(\varphi))\land(t^{\prime}[1\rangle\in\mathcal{L}^{\pi}_{t}(\varphi\operatorname{\mathcal{U}}\psi))\xLeftrightarrow{\text{SIH2+IH}}(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t^{*}})\lor(t^{\prime}\vDash\varphi|^{\pi}_{t^{*}})\land(t^{\prime}[1\rangle\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t})\Leftrightarrow(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t^{*}})\lor(t^{\prime}\vDash\varphi|^{\pi}_{t^{*}})\land(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t}))\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t^{*}}.$

• •

$\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$ and $\varphi\operatorname{\mathcal{R}}\psi$ are proven analogously.

4 Constraint-based Monitoring

For monitoring, we need to define an incremental rewriting that accurately models the semantics of $\varphi|^{\pi}_{t}$ while still being able to detect violations early. To this end, we define an operation $\varphi[\pi,e,i]$, where $e\in\Sigma$ is an event and $i$ is the current position in the trace. $\varphi[\pi,e,i]$ transforms $\varphi$ into a propositional formula, where the variables are either indexed atomic propositions $p_{\_}i$ for $p\in\mathit{AP}$, or a variable $v^{-}_{\varphi^{\prime},i+1}$ and $v^{+}_{\varphi^{\prime},i+1}$ that act as placeholders until new information about the trace comes in. Whenever the next event $e^{\prime}$ occurs, the variables are defined with the result of $\varphi^{\prime}[\pi,e^{\prime},i+1]$. If the trace ends, the variables are set to true and false for $v^{+}$ and $v^{-}$, respectively. We define $\varphi[\pi,e,i]$ of a $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ in NNF, event $e\in\Sigma$, and $i\geq 0$ recursively on the structure of the body $\varphi$:

[TABLE]

We encode a $\forall^{2}$HyperLTL formula and finite traces into a constraint system, which, as we will show, is satisfiable if and only if the given traces satisfy the formula w.r.t. the finite semantics of HyperLTL. We write $v_{\varphi,i}$ to denote either $v^{-}_{\varphi,i}$ or $v^{+}_{\varphi,i}$. For $e\in\Sigma$ and $t\in\Sigma^{*}$, we define

[TABLE]

where we use $v_{\psi,i+1}\in\varphi[\pi,e,i]$ to denote variables $v_{\psi,i+1}$ occurring in the propositional formula $\varphi[\pi,e,i]$. $\mathit{enc}$ is used to transform a trace into a propositional formula, e.g., $enc^{0}_{\{a,b\}}(\{a\}\{a,b\})\allowbreak=a_{\_}0\land\neg b_{\_}0\land a_{\_}1\land b_{\_}1$. For $n=0$ we omit the annotation, i.e., we write $enc_{\text{AP}}(t)$ instead of $enc^{0}_{\text{AP}}(t)$. Also we omit the index AP if it is clear from the context. By slight abuse of notation, we use $constr^{n}(\varphi,t)$ for some quantifier free HyperLTL formula $\varphi$ to denote $constr(v_{\varphi,n},t)$ if ${|t|}>0$. For a trace $t^{\prime}\in\Sigma^{+}$, we use the notation $enc(t^{\prime})\vDash constr(\varphi,t)\text{, which evaluates to {true} if, and only if }enc(t^{\prime})\land constr(\varphi,t)\text{ is satisfiable}.$

4.1 Algorithm

Figure 1 depicts our constraint-based algorithm. Note that this algorithm can be used in an offline and online fashion. Before we give algorithmic details, consider again, the observational determinism example from the introduction, which is expressed as $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}(out_{\_}{\pi}\leftrightarrow out_{\_}{\pi^{\prime}})\operatorname{\mathcal{W}}(in_{\_}{\pi}\nleftrightarrow in_{\_}{\pi^{\prime}})$. The basic idea of the algorithm is to transform the HyperLTL formula to a formula consisting partially of LTL, which expresses the requirements of the incoming trace in the current step, and partially of HyperLTL. Assuming the event $\{in,out\}$, we transform the observational determinism formula to the following formula: $\neg in\lor out\land\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((out_{\_}{\pi}\leftrightarrow out_{\_}{\pi^{\prime}})\operatorname{\mathcal{W}}(in_{\_}{\pi}\nleftrightarrow in_{\_}{\pi^{\prime}}))$.

A Boolean constraint system is then build incrementally: we start encoding the constraints corresponding to the LTL part (in front of the next-operator) and encode the HyperLTL part (after the next-operator) as variables that are defined when more events of the trace come in. We continue by explaining the algorithm in detail. In Figure 1, we construct $\psi$ as the negation normal form of the symmetric closure of the original formula. We build two constraint systems: $C$ containing constraints of previous traces and $C_{\_}t$ (built incrementally) containing the constraints for the current trace $t$. Consequently, we initialize $C$ with $\top$ and $C_{\_}t$ with $v_{\psi,0}$ (lines 1 and 1). If the trace ends, we define the remaining $v$ variables according to their polarities and add $C_{\_}t$ to $C$. For each new event $e_{\_}i$ in the trace $t$, and each “open” constraint in $C_{\_}t$ corresponding to step $i$, i.e., $v_{\phi,i}\in C_{\_}t$, we rewrite the formula $\phi$ (line 1) and define $v_{\phi,i}$ with the rewriting result, which, potentially introduced new open constraints $v_{\phi^{\prime},i+1}$ for the next step $i+1$. The constraint encoding of the current trace is aggregated in constraint $t_{\_}\mathit{enc}$ (Figure 1). If the constraint system given the encoding of the current trace turns out to be unsatisfiable, a violation to the specification is detected, which is then returned.

In the following, we sketch two algorithmic improvements. First, instead of storing the constraints corresponding to traces individually, we use a new data structure, which is a tree maintaining nodes of formulas, their corresponding variables and also child nodes. Such a node corresponds to already seen rewrites. The initial node captures the (transformed) specification (similar to line 1) and it is also the root of the tree structure, representing all the generated constraints which replaces $C$ in Fig. 1. Whenever a trace deviates in its rewrite result a new child or branch is added to the tree. If a rewrite result is already present in the node tree structure there is no need to create any new constraints nor new variables. This is crucial in case we observe many equal traces or traces behaving effectively the same. In case no new constraints were added to the constraint system, we omit a superfluous check for satisfiability.

Second, we use conjunct splitting to utilize the node tree optimization even more. We illustrate the basic idea on an example. Consider $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ with $\varphi=\operatorname{\leavevmode\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}((a_{\_}\pi\leftrightarrow a_{\_}\pi^{\prime})\lor(b_{\_}\pi\leftrightarrow b_{\_}\pi^{\prime}))$, which demands that on all executions on each position at least on of propositions $a$ or $b$ agree in its evaluation. Consider the two traces $t_{\_}1=\{a\}\{a\}\{a\}$, $t_{\_}2=\{a\}\{a,b\}\{a\}$ that satisfy the specification. As both traces feature the same first event, they also share the same rewrite result for the first position. Interestingly, on the second position, we get $(a\lor\neg b)\land s_{\_}\varphi$ for $t_{\_}1$ and $(a\lor b)\land s_{\_}\varphi$ for $t_{\_}2$ as the rewrite results. While these constraints are no longer equal, by the nature of invariants, both feature the same subterm on the right hand side of the conjunction. We split the resulting constraint on its syntactic structure, such that we would no longer have to introduce a branch in the tree.

4.2 Correctness

In this technical subsection, we will formally prove correctness of our algorithm by showing that our incremental construction of the Boolean constraints is equisatisfiable to the HyperLTL rewriting presented in Section 3. We begin by showing that satisfiability is preserved when shifting the indices, as stated by the following lemma.

Lemma 2

For any $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ over atomic propositions AP, any finite traces $t,t^{\prime}\in\Sigma^{+}$ and $n\geq 0$ it holds that $enc_{\text{AP}}(t^{\prime})\vDash constr(\varphi,t)\Leftrightarrow enc^{n}_{\text{AP}}(t^{\prime})\vDash constr^{n}(\varphi,t)$.

Proof

By renaming of the positional indices.

In the following lemma and corollary, we show that the semantics of the next operators matches the finite LTL semantics.

Lemma 3

For any $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ over atomic propositions AP and any finite traces $t,t^{\prime}\in\Sigma^{+}$ it holds that $enc(t^{\prime})\vDash constr(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi,t)\Leftrightarrow enc(t^{\prime})\vDash constr(v^{-}_{\varphi,1},t[1\rangle)\Leftrightarrow enc(t^{\prime}[1\rangle)\vDash constr(v^{-}_{\varphi,0},t[1\rangle).$

Proof

Let $\varphi$, $t,t^{\prime}$ be given. It holds that $constr(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi,t)=constr(v^{-}_{\varphi,1},t[1\rangle)$ by definition. As $constr(v^{-}_{\varphi,1},t[1\rangle)$ by construction does not contain any variables with positional index [math], we only need to check satisfiablity with respect to $enc(t^{\prime}[1\rangle)$. Thus $enc(t^{\prime})\vDash constr(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi,t)\Leftrightarrow enc(t^{\prime})\vDash constr(v^{-}_{\psi,1},t[1\rangle)\Leftrightarrow enc^{1}(t^{\prime}[1\rangle)\vDash constr(v^{-}_{\varphi,1},t[1\rangle)\xLeftrightarrow{\text{Lem}\ref{lem:encshift}}enc(t^{\prime}[1\rangle)\vDash constr(v^{-}_{\varphi,0},t[1\rangle)$.

Corollary 1

For any $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ over atomic propositions AP and any finite traces $t,t^{\prime}\in\Sigma^{+}$ it holds that $enc(t^{\prime})\vDash constr(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi,t)\Leftrightarrow enc(t^{\prime})\vDash constr(v^{+}_{\varphi,1},t[1\rangle)\Leftrightarrow enc(t^{\prime}[1\rangle)\vDash constr(v^{+}_{\varphi,0},t[1\rangle).$

We will now state the correctness theorem, namely that our algorithm preserves the HyperLTL rewriting semantics.

Theorem 4.1

For every $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ in negation normal form over atomic propositions AP and any finite trace $t\in\Sigma^{+}$ it holds that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t}\Leftrightarrow enc_{\text{AP}}(t^{\prime})\vDash constr(\varphi,t).$

Proof

By induction over the size of $t$. Induction Base ($t=e$, where $e\in\Sigma$): We choose $t^{\prime}\in\Sigma^{+}$ arbitrarily. We distinguish by structural induction the following cases over the formula $\varphi$:

• •

$a_{\_}{\pi}$: $constr(a_{\_}{\pi},e)=(a_{\_}\pi)[\pi,e,0]=\top\text{ if, and only if, }a\in e$. Thus $enc(t^{\prime})\vDash constr(a_{\_}{\pi},e)\Leftrightarrow a\in e\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}a_{\_}{\pi}|^{\pi}_{e}$.

• •

$a_{\_}{\pi^{\prime}}$: $constr(a_{\_}{\pi^{\prime}},e)=(a_{\_}{\pi^{\prime}})[\pi,e,0]=a_{\_}0$ Thus $enc(t^{\prime})\vDash constr(a_{\_}{\pi^{\prime}},e)\Leftrightarrow enc(t^{\prime})\vDash a_{\_}0\xLeftrightarrow{\text{def }enc}a\in t^{\prime}[0]\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}a\xLeftrightarrow{\text{def }|^{\pi}}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}a_{\_}{\pi^{\prime}}|^{\pi}_{e}$.

• •

$\neg a_{\_}{\pi}$ and $\neg a_{\_}{\pi^{\prime}}$ are proven analogously.

The structural induction hypothesis states that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}\Leftrightarrow enc(t^{\prime})\vDash constr(\psi,t)$ (SIH1), where $\psi$ is a strict subformula of $\varphi$.

• •

$\varphi\lor\psi$: $t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\lor\psi)|^{\pi}_{e}\Leftrightarrow(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{e})\lor(t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{e})\xLeftrightarrow{\text{SIH1}}(enc(t^{\prime})\vDash constr(\varphi,e))\lor(enc(t^{\prime})\vDash constr(\psi,e))\Leftrightarrow(enc(t^{\prime})\vDash\varphi[\pi,e,0])\lor(enc(t^{\prime})\vDash\psi[\pi,e,0])\Leftrightarrow enc(t^{\prime})\vDash\varphi[\pi,e,0]\lor\psi[\pi,e,0]\xLeftrightarrow{\text{def }enc}enc(t^{\prime})\vDash(\varphi\lor\psi)[\pi,e,0]\Leftrightarrow enc(t^{\prime})\vDash constr(\varphi\lor\psi,e).$

• •

$\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$: $constr(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi,e)=(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)[\pi,e,0]=v^{-}_{\varphi,0}\land(v^{-}_{\varphi,0}\mathbin{\rightarrow}~{}constr(v^{-}_{\varphi,0},\epsilon))=\bot$. Thus $t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)|^{\pi}_{e}=\bot\Leftrightarrow enc(t^{\prime})\vDash\bot$.

• •

$\varphi\operatorname{\mathcal{U}}\psi$: $constr(\varphi\operatorname{\mathcal{U}}\psi,e)=(\varphi\operatorname{\mathcal{U}}\psi)[\pi,e,0]=\psi[\pi,e,0]\lor(\varphi[\pi,e,0]\land constr(v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,0},\epsilon))=\psi[\pi,e,0]=constr(\psi,e)$. Thus $t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{e}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{e}\xLeftrightarrow{\text{SIH1}}enc(t^{\prime})\vDash constr(\psi,e)$.

• •

$\varphi\land\psi$, $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$, and $\varphi\operatorname{\mathcal{R}}\psi$ are proven analogously.

Induction Step ($t=e\cdot t^{*}$, where $e\in\Sigma$ and $t^{*}\in\Sigma^{+}$): The induction hypothesis states that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t^{*}}\Leftrightarrow enc(t^{\prime})\vDash constr(\varphi,t^{*})$ (IH). We make use of structural induction over $\varphi$. All base cases are covered as their proofs above are independent of $|t|$. The structural induction hypothesis states for all strict subformulas $\psi$ that $\forall t^{\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}\Leftrightarrow enc(t^{\prime})\vDash constr(\psi,t)$.

• •

$\varphi\lor\psi$:

\begin{array}[]{ll}&t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\lor\psi)|^{\pi}_{t}\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t}~{}\lor~{}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}\\ \xLeftrightarrow{\text{SIH1}}&enc(t^{\prime})\vDash constr(\varphi,t)~{}\lor~{}enc(t^{\prime})\vDash constr(\psi,t)\\ \xLeftrightarrow{t=e\cdot t^{*}}&enc(t^{\prime})\vDash(\varphi[\pi,e,0]\land\bigwedge\limits_{\_}{v_{\varphi^{\prime},1}\in\varphi[\pi,e,0]}v_{\varphi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\varphi^{\prime},1},t^{*}))\\ &\lor~{}enc(t^{\prime})\vDash(\psi[\pi,e,0]\land\bigwedge\limits_{\_}{v_{\psi^{\prime},1}\in\varphi[\pi,e,0]}v_{\psi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\psi^{\prime},1},t^{*}))\\ \xLeftrightarrow{{\dagger}}&enc(t^{\prime})\vDash(\varphi[\pi,e,0]\lor\psi[\pi,e,0])\\ &\land\bigwedge\limits_{\_}{v_{\varphi^{\prime},1}\in\varphi[\pi,e,0]}v_{\varphi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\varphi^{\prime},1},t^{*})\end{array}

\begin{array}[]{ll}&\land\bigwedge\limits_{\_}{v_{\psi^{\prime},1}\in\varphi[\pi,e,0]}v_{\psi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\psi^{\prime},1},t^{*})\\ \Leftrightarrow&enc(t^{\prime})\vDash(\varphi\lor\psi)[\pi,e,0]\\ &\land\bigwedge\limits_{\_}{v_{\phi,1}\in(\varphi\lor\psi)[\pi,e,0]}v_{\phi,1}\mathbin{\rightarrow}~{}constr(v_{\phi,1},t^{*})\\ \xLeftrightarrow{t=e\cdot t^{*}}&enc(t^{\prime})\vDash constr(\varphi\lor\psi,t)\\ \end{array}

${\dagger}$: $\Leftarrow$: trivial, $\Rightarrow$: Assume a model $M_{\_}\varphi$ for $enc(t^{\prime})\vDash\varphi[\pi,e,0]\land A$. By construction, constraints by $\varphi$ do not share variable with constraints by $\psi$. We extend the model by assigning $v_{\psi^{\prime},1}$ with $\bot$, for all $v_{\psi^{\prime},1}\in\psi[\pi,e,0]$ and assigning the rest of the variables in $\psi[\pi,e,0]$ arbitrarily.

• •

$\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$: $t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)|^{\pi}_{t}\Leftrightarrow t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi|^{\pi}_{t^{*}}\Leftrightarrow t^{\prime}[1\rangle\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t^{*}}\xLeftrightarrow{\text{IH}}enc(t^{\prime}[1\rangle)\vDash constr(\varphi,t^{*})\xLeftrightarrow{\text{Lem}\ref{lem:encshiftnext}}enc(t^{\prime})\vDash constr(\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi,t){}.$

• •

$\varphi\operatorname{\mathcal{U}}\psi$:

\begin{array}[]{ll}&t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t}\\ \Leftrightarrow&t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\psi|^{\pi}_{t}~{}\lor~{}\left[t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\varphi|^{\pi}_{t}~{}\land~{}t^{\prime}[1\rangle\vDash_{\text{LTL}_{\mathit{fin}}}(\varphi\operatorname{\mathcal{U}}\psi)|^{\pi}_{t^{*}}\right]\\ \xLeftrightarrow{\text{SIH1+IH},\text{L}\ref{lem:encshiftnext}}&enc(t^{\prime})\vDash constr(\psi,t)\\ &\lor\left[enc(t^{\prime})\vDash constr(\varphi,t)~{}\land~{}enc(t^{\prime})\vDash constr(v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1},t^{*})\right]\\ \Leftrightarrow&enc(t^{\prime})\vDash(\psi[\pi,e,0]\land\bigwedge\limits_{\_}{v_{\psi^{\prime},1}\in\psi[\pi,e,0]}v_{\psi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\psi^{\prime},1},t^{*}))\\ &\lor~{}\left(\begin{array}[]{ll}enc(t^{\prime})&\vDash(\varphi[\pi,e,0]\land\bigwedge\limits_{\_}{v_{\varphi^{\prime},1}\in\varphi[\pi,e,0]}v_{\varphi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\varphi^{\prime},1},t^{*}))\\ \land~{}enc(t^{\prime})&\vDash(v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1}\land v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1}\mathbin{\rightarrow}~{}constr(v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1},t^{*}))\end{array}\right)\\ \xLeftrightarrow{\text{same as }{\dagger}}&enc(t^{\prime})\vDash(\psi[\pi,e,0]\lor(\varphi[\pi,e,0]\land v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1}))\\ &\land\bigwedge\limits_{\_}{v_{\psi^{\prime},1}\in\psi[\pi,e,0]}v_{\psi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\psi,1},t^{*})\\ &\land\bigwedge\limits_{\_}{v_{\varphi^{\prime},1}\in\varphi[\pi,e,0]}v_{\varphi^{\prime},1}\mathbin{\rightarrow}~{}constr(v_{\varphi^{\prime},1},t^{*})\\ &\land~{}v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1}\mathbin{\rightarrow}~{}constr(v^{-}_{\varphi\operatorname{\mathcal{U}}\psi,1},t^{*})\\ \Leftrightarrow&enc(t^{\prime})\vDash\varphi\operatorname{\mathcal{U}}\psi[\pi,e,0]\\ &\land\bigwedge\limits_{\_}{{v_{\phi,1}}\in\varphi\operatorname{\mathcal{U}}\psi[\pi,e,0]}v_{\phi,1}\mathbin{\rightarrow}~{}constr(v_{\phi,1},t^{*})\\ \Leftrightarrow&enc(t^{\prime})\vDash constr(\varphi\operatorname{\mathcal{U}}\psi,t)\\ \end{array}

• •

$\varphi\land\psi$, $\operatorname{\leavevmode\leavevmode\hbox to7.41pt{\vbox to9.92pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{7.5347pt}\pgfsys@lineto{-1.39905pt}{7.93867pt}\pgfsys@curveto{-1.10196pt}{8.31003pt}{-0.5885pt}{8.33847pt}{-0.25223pt}{8.0022pt}\pgfsys@lineto{0.25223pt}{7.49776pt}\pgfsys@curveto{0.5885pt}{7.16148pt}{1.10196pt}{7.18993pt}{1.39905pt}{7.56128pt}\pgfsys@lineto{1.72221pt}{7.96526pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$, and $\varphi\operatorname{\mathcal{R}}\psi$ are proven analogously.

Corollary 2

For any $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ in negation normal form over atomic propositions AP and any finite traces $t,t^{\prime}\in\Sigma^{+}$ it holds that $t^{\prime}\in\mathcal{L}_{t}(\varphi)\Leftrightarrow enc_{\text{AP}}(t^{\prime})\vDash constr(\hat{\varphi},t)$.

Proof

$t^{\prime}\in\mathcal{L}_{t}(\varphi)\xLeftrightarrow{\text{Thm}\ref{thm:ltlfin-compat}}t^{\prime}\vDash_{\text{LTL}_{\mathit{fin}}}\hat{\varphi}|^{\pi}_{t}\xLeftrightarrow{\text{Lem}\ref{thm:equisat-ltlfin-sat}}enc(t^{\prime})\vDash constr(\hat{\varphi},t).$

Lemma 4

For any $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ in negation normal form over atomic propositions AP and any finite traces $t,t^{\prime}\in\Sigma^{+}$ it holds that $enc_{\text{AP}}(t^{\prime})\nvDash constr(\varphi,t)\Rightarrow\forall t^{\prime\prime}\in\Sigma^{+}\mathpunct{.}t^{\prime}\leq t^{\prime\prime}\mathbin{\rightarrow}~{}enc_{\text{AP}}(t^{\prime\prime})\nvDash constr(\varphi,t)$.

Proof

We proof this via contradiction. We choose $t,t^{\prime}$ as well as $\varphi$ arbitrarily, but in a way such that $enc(t^{\prime})\nvDash constr(\varphi,t)$ holds. Assume that there exists a continuation of $t^{\prime}$, that we call $t^{\prime\prime}$, for which $enc(t^{\prime\prime})\vDash constr(\varphi,t)$ holds. So there has to exist a model assigning truth values to the variables in $constr(\varphi,t)$, such that the constraint system is consistent. From this model we extract all assigned truths values for positional variables for position $|t^{\prime}|$ to $|t^{\prime\prime}|-1$. As $t^{\prime}$ is a prefix of $t^{\prime\prime}$, we can use these truth values to construct a valid model for $enc(t^{\prime})\vDash constr(\varphi,t)$, which is a contradiction.

Corollary 3

For any $\forall^{2}$HyperLTL formula $\forall\pi,\pi^{\prime}\mathpunct{.}\varphi$ in negation normal form over atomic propositions AP and any finite set of finite traces $T\in\mathcal{P}(\Sigma^{+})$ and finite trace $t^{\prime}\in\Sigma^{+}$ it holds that

[TABLE]

Proof

It holds that $\forall t,t^{\prime}\in\Sigma^{+}\mathpunct{.}t\neq t^{\prime}\mathbin{\rightarrow}~{}constr(\varphi,t)\neq constr(\varphi,t^{\prime})$. Follows with same reasoning as in earlier proofs combined with 2.

5 Experimental Evaluation

We implemented two versions of the algorithm presented in this paper. The first implementation encodes the constraint system as a Boolean satisfiability problem (SAT), whereas the second one represents it as a (reduced ordered) binary decision diagram (BDD). The formula rewriting is implemented in a Maude [8] script. The constraint system is solved by either CryptoMiniSat [23] or CUDD [22]. All benchmarks were executed on an Intel Core i5-6200U CPU @2.30GHz with 8GB of RAM. The set of benchmarks chosen for our evaluation is composed out of two benchmarks presented in earlier publications [12, 13] plus instances of guarded invariants at which our implementations excels.

Non-interference.

Non-interference [16, 19] is an important information flow policy demanding that an observer of a system cannot infer any high security input of a system by observing only low security input and output. Reformulated we could also say that all low security outputs $\vec{o}^{low}$ have to be equal on all system executions as long as the low security inputs $\vec{i}^{low}$ of those executions are the same: $\forall\pi,\pi^{\prime}\mathpunct{.}({\vec{o}^{low}_{\_}\pi}\leftrightarrow{\vec{o}^{low}_{\_}{\pi^{\prime}}})\operatorname{\mathcal{W}}({\vec{i}^{low}_{\_}\pi}\nleftrightarrow{\vec{i}^{low}_{\_}{\pi^{\prime}}}).$ This class of benchmarks was used to evaluated RVHyper [13], an automata-based runtime verification tool for HyperLTL formulas. We repeated the experiments and depict the results in Fig. 2. We choose a trace length of $50$ and monitored non-interference on $1000$ randomly generated traces, where we distinguish between a $64$ bit input (left) and an $128$ bit input (right). For $64$ bit input, our BDD implementation performs comparably well to RVHyper, which statically constructs a monitor automaton. For $128$ bit input, RVHyper was not able to construct the automaton in reasonable time. Our implementation, however, shows promising results for this benchmark class that puts the automata-based construction to its limit.

Detecting Spurious Dependencies in Hardware Designs.

The problem whether input signals influence output signals in hardware designs, was considered in [13]. Formally, we specify this property as the following HyperLTL  formula: $\forall\pi_{\_}1\forall\pi_{\_}2\mathpunct{.}(\vec{o}_{\_}{\pi_{\_}1}\leftrightarrow\vec{o}_{\_}{\pi_{\_}2})\operatorname{\mathcal{W}}(\overline{\vec{i}}_{\_}{\pi_{\_}1}\nleftrightarrow\overline{\vec{i}}_{\_}{\pi_{\_}2}),$ where $\overline{\vec{i}}$ denotes all inputs except $\vec{i}$. Intuitively, the formula asserts that for every two pairs of execution traces $(\pi_{\_}1,\pi_{\_}2)$ the value of $\vec{o}$ has to be the same until there is a difference between $\pi_{\_}1$ and $\pi_{\_}2$ in the input vector $\overline{\vec{i}}$, i.e., the inputs on which $\vec{o}$ may depend. We consider the same hardware and specifications as in [13]. The results are depicted in Table 1.

Again, the BDD implementation handles this set of benchmarks well.

The biggest difference can be seen between the runtimes for counter2. This is explained by the fact that this benchmark demands the highest number of observed traces, and therefore the impact of the quadratic runtime costs in the number of traces dominates the result. We can, in fact, clearly observe this correlation between the number of traces and the runtime on RVHyper’s performance over all benchmarks. On the other hand our constraint-based implementations do not show this behavior.

Guarded Invariants.

We consider a new class of benchmarks, called guarded invariants, which express a certain invariant relation between two traces, which are, additionally, guarded by a precondition. Fig. 3 shows the results of monitoring an arbitrary invariant $P:\Sigma\rightarrow\mathbb{B}$ of the following form: $\forall\pi,\pi^{\prime}\mathpunct{.}\operatorname{\leavevmode\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\vee_{\_}{i\in I}i_{\_}{\pi}\nleftrightarrow i_{\_}{\pi^{\prime}})\rightarrow\operatorname{\leavevmode\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(P(\pi)\leftrightarrow P(\pi^{\prime}))$. Our approach significantly outperforms RVHyper on this benchmark class, as the conjunct splitting optimization, described in Section 4.1, synergizes well with SAT-solver implementations.

Atomic Proposition Scalability.

While RVHyper is inherently limited in its scalability concerning formula size as the construction of the deterministic monitor automaton gets increasingly hard, the rewrite-based solution is not affected by this limitation. To put it to the test we have ran the SAT-based implementation on guarded invariant formulas with up to 100 different atomic propositions. Formulas have the form: $\forall\pi,\pi^{\prime}\mathpunct{.}(\wedge_{\_}{i=1}^{n_{\_}{in}}(in_{\_}{i,\pi}\leftrightarrow in_{\_}{i,\pi^{\prime}}))\rightarrow\operatorname{\leavevmode\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\vee_{\_}{j=1}^{n_{\_}{out}}(out_{\_}{j,\pi}\leftrightarrow out_{\_}{j,\pi^{\prime}})),$ where $n_{\_}{in},n_{\_}{out}$ represents the number of input and output atomic propositions, respectively. Results can be seen in Fig. 4. Note that RVHyper already fails to build monitor automata for $|n_{\_}{in}+n_{\_}{out}|>10$.

6 Conclusion

We pursued the success story of rewrite-based monitors for trace properties by applying the technique to the runtime verification problem of Hyperproperties. We presented an algorithm that, given a $\forall^{2}$HyperLTL formula, incrementally constructs constraints that represent requirements on future traces, instead of storing traces during runtime. Our evaluation shows that our approach scales in parameters where existing automata-based approaches reach their limits.

Acknowledgments.

We thank Bernd Finkbeiner for his valuable feedback on earlier versions of this paper.