Academic
Publications
How Hard is Smart Play-Out? On the Complexity of Veriflcation-Driven Execution

How Hard is Smart Play-Out? On the Complexity of Veriflcation-Driven Execution,David Harel,Hillel Kugler,Shahar Maoz,Itai Segall

How Hard is Smart Play-Out? On the Complexity of Veriflcation-Driven Execution   (Citations: 1)
BibTex | RIS | RefWorks Download
Smart play-out is a method for executing declarative scenario-based requirements, which utilizes powerful model-checking or planning al- gorithms to run the scenarios and avoid some of the violations that can be caused by na˜‡ve execution. In this paper, we investigate the complexity of smart play-out. Speciflcally, 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.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...In [8] we prove smart play-out to be PSPACE-hard for the general case, and NP-hard if multiple copies of the same chart are not allowed...

    David Harelet al. Accelerating Smart Play-Out

Sort by: