Extending Automated FLTL Test Oracles with Diagnostic Support Testing is a versatile and in practice also dominant technique when it comes to verifying whether a system meets our expectations. After executing a test case, we use test oracles to judge whether the execution should be considered to have failed or passed. Fully automated oracles considering properties in temporal logics like FLTL allow us to derive such a verdict in a fully automated process. In this manuscript, we will show how to extend such an oracle with diagnostic support. In particular, drawing on modelbased diagnosis (MBD), we will isolate exactly which parts of the property were violated for a failed test case. Such data are orthogonal to MBD focusing on the system itself and where we isolate faulty system components. With our diagnoses, we thus provide valuable information for the subsequent debugging and repair process in respect of how the test execution violated the property. We show that a corresponding polynomially sized SAT model for deriving our diagnoses can be derived easily.

On Verifying Timed Hyperproperties We study the satisfiability and modelchecking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: asynchronous and synchronous. While the satisfiability problem can be decided similarly to HyperLTL regardless of the choice of semantics, we show that the modelchecking problem, unless the specification is alternationfree, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.