Parse tree structure in LTL requirements diagnosis

Automated assistance in ensuring a product's reliability and functional correctness is certainly a powerful asset, but also requires us to express our expectations in a formal way as accessible to our algorithms and tools. In recent work, we showed for specifications in Pnueli's "Temporal Logic of Programs" LTL how to diagnose such a specification if we find that it does not catch our intent, i.e., when some behavior expected to satisfy it actually violates it (and vice versa). In this paper, we show how to improve this process in that we exploit structural data in the form of a specification's parse tree for our diagnostic reasoning. We discuss the achieved effects for the example of the well-known model-based diagnosis algorithm HS-DAG and report on corresponding experimental results that show our reasoning's attractiveness.