Accelerating Smart Play-Out

Smart play-out is a method for executing declarative scenario-based specifications, which utilizes powerful computation methods to compute safe supersteps, thus helping to avoid violations that may be caused by naive execution. Major challenges for smart play-out are performance and scalability. In this work we show how to accelerate smart play-out by adapting and applying ideas inspired by formal verification and compiler optimization. Specifically, we present an algorithm that can reduce the size of the specification considered for smart play-out, while maintaining soundness and completeness. Experimental results show significant performance improvements and thus open the way to the application of smart play-out to large scenario-based programs.