## 6 Exact Monitoring under Imperfect Information Given Uncertain Linear Dynamics
We finally add one of the two conjuncts (a) \(\
eg\phi\_t^{\prime}\) or (b) \(\phi\_t^{\prime}\) alternatively to the resultant constraint system and check both variants for their satisfiability using an SMT-LA solver. For the example from Figure 2, that encoding (shown in iSAT [21] syntax; a complete overview over the iSAT syntax is available from [[https://projects.informatik.uni-freiburg.de/attachments/download/189/isat3_manual-0.02-20140409.pdf](https://projects.informatik.uni-freiburg.de/attachments/download/189/isat3_manual-0.02-20140409.pdf)]([https://projects.informatik.uni-freiburg.de/attachments/download/189/isat3_manual-0.02-20140409.pdf](https://projects.informatik.uni-freiburg.de/attachments/download/189/isat3_manual-0.02-20140409.pdf)), accessed on 14 March 2022) reads as follows for variant 7(b) (an equivalent encoding in the SMT-Lib format can be found in Appendix A):  
DECL -- Ground-truth state variables float [-100,100] x1, x2, x3, x4, x5; float [-100,100] y1, y2, y3, y4, y5;  
-- Actual measurements define my1 = 0.1; define my5 = 0.1;  
-- Uncertainties in measurements float [-0.5,0.5] oy, ey1, ey5;-- Uncertainties in system dynamics float [-0.1,0.1] uy1, uy2, uy3, uy4;  
-- Helper variables for BMC encoding  
boole p1, p2, p3, p4, p5, q1;  
defines s = 0.707106781; -- 1/sqrt(2)  
EXPR -- Uncertain linear system dynamics x2 = s*x1 - s*y1; y2 = s*x1 + s*y1 + uy1; x3 = s*x2 - s*y2; y3 = s*x2 + s*y2 + uy2; x4 = s*x3 - s*y3; y4 = s*x3 + s*y3 + uy3; x5 = s*x4 - s*y4; y5 = s*x4 + s*y4 + uy4;  
-- Relations between measurements and states -- reflecting an absolute error of +-0.5 both as offset and random y1 + 0.5*oy + 0.5*ey1 = my1; y5 + 0.5*oy + 0.5*ey5 = my5;  
-- BMC encoding of monitoring condition -- p_ represents satisfaction of y >= 0.2 at time instant _ p1 <-> y1 >= 0.2; p2 <-> y2 >= 0.2; p3 <-> y3 >= 0.2; p4 <-> y4 >= 0.2; p5 <-> y5 >= 0.2;  
-- q_ represents validity of G <=5 p at time instant _ q1 <-> p1 and p2 and p3 and p4 and p5;  
-- Goal, namely satisfaction of q at time 1 q1;  
Note that the above encoding employs the slightly optimized BMC encoding  
\[\psi\_k\Leftrightarrow\bigwedge_{i=k}^{k+d}\psi^{\prime}\_i\]  
for subformulae \(\psi=\mathbf{G}_{\leq d}\psi^{\prime}\) at each \(k\in\{t-\text{duration}(\phi),\ldots,t-\text{duration}(\psi)\}\). The above constraint system is unsatisfiable, confirming the verdict \(\bot\) for the monitoring condition \(\phi=\mathbf{G}_{\leq d}\psi\geq 0.2\) at time \(t^{\prime}=1\). Its unsatisfiability can automatically be decided by any satisfiability modulo theory (SMT) solver addressing SMT-LA, i.e., Boolean combinations of linear inequalities. Likewise, its variant encoding the relative error model from Equation (2) can be decided by any SMT solver solving Boolean combinations of polynomial constraints. Such solvers do in general rely on solving a Boolean abstraction of the SMT formula, where all theory atoms (linear or polynomial inequalities in our case) are replaced by Boolean literals by a CDCL (conflict-driven clause learning) propositional satisfiablity (SAT) solver [22; 23] in order to resolve the Boolean structure. As this SAT solving incrementally instantiates the Boolean literals in the abstraction, a conjunctive constraints system in the theory underlying the SMT problem (e.g., linear arithmetic) is incrementally built by collecting the theory constraints that have been abbreviated by the Boolean literals. These conjunctive systems of theory constraints are then solved by a subordinate theory solver, which blocks further expansion of the partial truth assignment to the literals in the Boolean abstraction when the associated theory-related constraint system becomes unsatisfiable. The reasons for unsatisfiability are usually reported back to the SAT solver in form of a corresponding conflict clause over the abstracting Boolean literals, where the conflict clause reflects a minimal (or, in cases of undecidability of high computational cost, small) infeasible core of the unsatisfiable theory constraint system.