PESTS: Partial Evaluator of Simple Transition Systems
Gabriele Costa, David Basin, Chiara Bodei, Pierpaolo Degano, Letterio Galletta · Zenodo (CERN European Organization for Nuclear Research) · 2018
In the TACAS paper, it is proved that natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. In addition, there it was presented a quotienting algorithm and introduced a tool for the partial model checking of finite-state systems that can be used as an alternative to natural projection. In connection with the TACAS paper, we present here the tool suite for the partial evaluation, called PESTS (Partial Evaluator of Simple Transition Systems), used there. We applied the prototype to some case studies. In particular, PESTS can be used to address the following different problems: 1. reducing the verification of a parallel composition to that of a single component; 2. synthesizing a submodule that respects a global specification: Submodule Construction Problem (SCP); 3. synthesizing a controller for a given component: Controller Synthesis Problem (CSP).