search menu icon-carat-right cmu-wordmark

Statistical Model Checking for Swarms

This SEI poster created for the 2016 Research Review illustrates input attribution.

Software Engineering Institute


Statistical Model Checking (SMC) provides an estimate on the probability 𝑃[ℳ⊨Φ] that a predicate Φ in a model ℳ is satisfied; but does not address why a particular result was obtained. The goal of Input Attribution (IA) is to use machine learning techniques to synthesize an explanation for an SMC result in terms of the inputs. IA for SMC can be thought of as analogous to the counter-example in traditional model checking.