Relational and graph queries over a transition system

Explicit model-checking is a brute force traversal of all possible model states that permits to assert if a property is satisfied or not. If the property is violated, the model-checker produces a counterexample trace. However, once the existence of a problem is proved, the designer is left with a counterexample trace that only exhibits the problem [1]. The designer needs to interpret traces and this interpretation is challenging for several reasons such as the trace size or the low-level of information. We believe that querying traces will help the problem interpretation because it supports visualization and diagnosis tools. We designed KriQL, a query language working on traces and the underlying labelled transition system. This paper evaluates different KriQL implementations, mainly the use of relational and graph databases for the management of the transition system. We present results obtained through the analysis of a Cruise-Control System, a realistic case study from the automotive industry.