|author:||S.H. van Schouwenburg|
|title:||Automatic Parallelization of Automata|
|keywords:||Parallelization, Model Checking, DVE, ETF, LTSmin, Independent Set Algorithm|
There exist many modeling languages for model checking, each with their own verification tools. There have been efforts to get some better interoperability among modeling languages, and LTSmin is one such attempt.
LTSmin is a toolset which contains tools to abstract mod- els in a high level modeling language into a Labelled Tran- sition System (LTS). This is done by doing a state space generation. That state space can be stored in ETF (Enumerated Table Format).
Since the model checking is then done on the state space instead of the original model, the question is how much in- formation this state space contains compared to the orig- inal high level language. In this work, we investigate this by transforming high level models in DVE (Distributed Verification Environment) format into ETF and then convert that ETF back into a DVE model. We then perform benchmarks to see how much performance we have lost (or gained).
Model checking on DVE performs best on a model with parallel processes, as opposed to a monolithic single process model. So the transitions in the state space must be divided over separate parallel processes. Each process can only write to its own variables, but can read from all of them. So we need an algorithm which identifies variables in the state space that can have their own process. It must be done in such a way that no transition alters more than one of such variable, or that transition will not fit in any process.
One way of doing this is by using an independent set algorithm (ISA) to identify (mark) the variables. We have investigated whether a weighted independent set algorithm performs better than an unweighted algorithm.
We have benchmarked different models and compared the originals with the plain (non-parallel), weighted and unweighted generated models. The main conclusions are that generated models never approach the efficiency of the originals and that the parallel versions usually perform significantly better than the plain versions.