Wieger Wesselink: Symbolic Reachability using LDDs

Event Details

The mCRL2 toolset contains several applications in which computing the set of reachable states of a transition relation plays a role. For example in state space generation and in solving a PBES. List decision diagrams (LDDs) can be used to store sets of states and transitions in a compact manner. This has been demonstrated by Jaco van de Pol and Stefan Blom in 2008, and these ideas have been implemented in the LTSMin toolset. We are currently applying these ideas in the mCRL2 toolset as well, using the LDD functionality of the Sylvan library made by Tom van Dijk. In this talk I will explain the main ideas behind it, and describe a reachability algorithm that uses LDDs.