Mar 11, 2014: Jeroen Meijer: Improving Symbolic Reachability Analysis in LTSmin

March 11, 2014Improving Symbolic Reachability Analysis in LTSmin
Room: HalB 2FJeroen Meijer

To improve symbolic reachability analysis in the model checking toolset LTSmin, we present two major improvements to existing reachability algorithms. LTSmin uses a disjunctive partitioning scheme to efficiently analyse models of asynchronous systems. In these models transitions can be partitioned into groups, which modify only a small part of the state vector.

Currently, there are no well defined notions, for whether a transition group reads and/or writes to an element in the state vector, which can be used in symbolic algorithms. Therefore, we present new definitions for read and write dependencies and show how algorithms can exploit these. This improvement always results in faster state space generation and many models such as Petri nets highly benefit of these changes. We provide examples that were intractable for LTSmin before, but can now be computed in a matter of minutes.

A transition in a model specification is often of the form “if condition(x1,...,xn) => a. X(x1',...,xn')”. Our second improvement divides the condition into multiple conjuncts. These conjuncts can then be evaluated separately. Symbolic algorithms can exploit this information and prevent computing successors for large sets of states for only one conjunct evaluation. This greatly speeds up state space generation for models such as sokoban or dining philosophers. We provide examples that show a speedup ranging from twice as fast to hundreds of times faster.