An Effective Way of Storing and Accessing Very Large Transition Matrices Using Multi-core CPU and GPU Architectures

The topic of probabilistic model checking algorithms of Markov processes makes the problem of storing and processing of very large transition matrices crucial. While the symbolic approach utilises very effective storage and access methods, like Multi-terminal Binary Decision Diagrams, the traditional explicit method of representing and solving the model using sparse matrices has many advantages, especially when we concired the flexibility of computing of different properties. We show and examine a compact representation of a very large transition matrix in the sparse form. The technique employs an effective method of compression, storage, and accessing of the matrix and is suitable for use in mutli-core CPU and GPU environments. Such large transition matrices consume a lot of space and cannot be considered as typical types of data for storage in database systems. Nevertheless, their storage and efficient access to them could be beneficial for solving of Markov models, so constructing specialised compression methods is obviously the way to go.