Trace Diagnostics Using Temporal Implicants

Runtime verification and model checking are two important methods for assessing correctness of systems. In both techniques, detecting an error is witnessed by an execution that violates the system specification. However, a faulty execution on its own may not provide sufficiently precise insight to the causes of the reported violation. Additional, often manual effort is required to properly diagnose the system. In this paper we present a method for analyzing such causes. The specifications we consider are expressed in LTL (Linear Temporal Logic) and MTL (Metric Temporal Logic), and the execution models are taken as ultimately-periodic words, and finite variability continuous signals respectively. The diagnostics problem is defined for the propositional case as the search for a small implicant of a formula which is satisfied by a given valuation, or equivalently a subset of that valuation sufficient to render the formula true. We propose a suitable notion of implicants in the tem...

• Type: Journal
• Year: 2015
• Where: ATVA
• Authors: Thomas Ferrère, Oded Maler, Dejan Nickovic
• Keywords: ATVA 2015, Hardware