Towards Bridging Formal Methods and Human Interpretability

TL;DR

This paper investigates how various complexity metrics of Labeled Transition Systems (LTS) influence human understanding, identifying key metrics that correlate with comprehension and demonstrating their practical utility in improving interpretability.

Contribution

It introduces a set of human-centered complexity metrics for LTS, validates their correlation with human comprehension, and applies one metric to enhance formal design interpretability.

Findings

Albin complexity correlates strongly with human comprehension ($\tau=0.444$).

Using the Albin complexity metric reduced comprehension time by 39%.

Key metrics like state space size and cyclomatic complexity significantly impact understanding.

Abstract

Labeled Transition Systems (LTS) are integral to model checking and design repair tools. System engineers frequently examine LTS designs during model checking or design repair to debug, identify inconsistencies, and validate system behavior. Despite LTS's significance, no prior research has examined human comprehension of these designs. To address this, we draw on traditional software engineering and graph theory, identifying 7 key metrics: cyclomatic complexity, state space size, average branching factor, maximum depth, Albin complexity, modularity, and redundancy. We created a dataset of 148 LTS designs, sampling 48 for 324 paired comparisons, and ranked them using the Bradley-Terry model. Through Kendall's Tau correlation analysis, we found that Albin complexity ($\tau = 0.444$), state space size ($\tau = 0.420$), cyclomatic complexity ($\tau = 0.366$), and redundancy ($\tau = 0.315$) most accurately reflect human comprehension of LTS designs. To showcase the metrics' utility, we applied the Albin complexity metric within the Fortis design repair tool, ranking system redesigns. This ranking reduced annotators' comprehension time by 39\%, suggesting that metrics emphasizing human factors can enhance formal design interpretability.