Thomas Ferrère

Date: 17:00, Wednesday, July 1, 2015
Speaker: Thomas Ferrère
Venue: IST Austria

Day: Wednesday

In runtime verification or model checking, some error is witnessed by an execution violating the system specification. However, a faulty execution on its own may not provide sufficiently precise insight to the causes of the reported violation. We present a method for analyzing such causes for the specification languages of LTL and MTL, where execution models are taken as ultimately-periodic and finite variability continuous signals respectively. The diagnostics problem may be defined in 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 temporal case, that are semantically based on signal subsets, and guarantee the existence of prime implicants for arbitrary temporal properties. An inductive procedure for finding temporal implicants is obtained by the introduction of selection functions that appear in a process equivalent to Skolemization in first order logic. Through the model restrictions we impose for LTL and MTL we are able to generate concise implicants of a property, describing a small fragment of the input signal that causes violation of a formula.

Posted in RiSE Seminar