Paper on An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking Accepted for ATVA 2019
The paper "An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking", authored by Martin Kölbl and Stefan Leue has been accepted for the 17th International Symposium on Automated Technology for Verification and Analysis ATVA 2019, to be held in Taipei in October 2019.
Abstract: Causality Checking has been proposed as a finite state space exploration technique which computes ordered sequences of events that are considered to cause the violation of a reachability property. A crucial point in the implementation of Causality Checking is the computation and storage of all minimal counterexamples found during state space exploration. We refer to the set of all minimal counterexamples as a causal trace set. However, the Duplicate State Prefix Matching (DSPM) Algorithm that is currently used in Causality Checking only under-approximates the causal trace set. As we argue, without the approximation the DSPM algorithm is inefficient. We propose the, to the best of our knowledge, first efficient algorithm that precisely computes a causal trace set, avoiding approximation, called Causal Trace Backward Search (CTBS). We compare the DSPM and CTBS algorithms with respect to their worst case complexities, and by applying them to several case studies.