How Hard is Smart Play-Out? On the Complexity of Verification-Driven Execution

Smart play-out is a method for executing declarative scenario-based requirements, which utilizes powerful model-checking or planning algorithms to run the scenarios and avoid some of the violations that can be caused by naive execution. In this paper, we investigate the complexity of smart play-out. Specifically, we use a reduction from QBF in order to show that smart play-out for a most basic subset of the scenario-based language of LSC is PSPACE-hard. The main advantage of our proof compared to a previous one by Bontemps and Schobbens is that ours is explicit, and takes advantage of the visual features of the LSC language. We also show that for a subset of the language, in which no multiple running copies are allowed, the problem is NP-hard.