Computer Science – Logic in Computer Science
Scientific paper
2011-06-07
EPTCS 54, 2011, pp. 17-30
Computer Science
Logic in Computer Science
In Proceedings GandALF 2011, arXiv:1106.0814
Scientific paper
10.4204/EPTCS.54.2
Symbolic model checking by using BDDs has greatly improved the applicability of model checking. Nevertheless, BDD based symbolic model checking can still be very memory and time consuming. One main reason is the complex transition relation of systems. Sometimes, it is even not possible to generate the transition relation, due to its exhaustive memory requirements. To diminish this problem, the use of partitioned transition relations has been proposed. However, there are still systems which can not be verified at all. Furthermore, if the granularity of the partitions is too fine, the time required for verification may increase. In this paper we target the symbolic verification of asynchronous concurrent systems. For such systems we present an approach which uses similarities in the transition relation to get further memory reductions and runtime improvements. By applying our approach, even the verification of systems with an previously intractable transition relation becomes feasible.
No associations
LandOfFree
Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-25238