Question: Non-default Issy Option

[phheim]

Hi Luca, Hi Shaun,

While getting sweap from 42fa3e8 to run (see #5), I looked at the Makefile.

There, I saw that you use Issy with --pruning 2, which is a non-default option and should therefore only be used in specific cases. Is there a particular reason why you are using Issy with that option?

Best,
Philippe

[lou1306]

Hi Philippe,
In [1], Table 3 showed that pruning gave substantially better results on TSL-MT benchmarks and marginally better on both the new Issy benchmarks and the "hard" problems from [2]. This was the primary reason why we enabled pruning.

We might also have been biased by our previous comparative evaluation [3], where tslmt2rpg (with pruning) fared significantly better than rpgsolve (without). Even though we know Issy is a new implementation, we took that as a clue that our benchmarks might be easier to tackle when monitor pruning is enabled.

---

[1] Philippe Heim and Rayna Dimitrova. 2025. Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems. In 37th International Conference on Computer Aided Verification (CAV) (LNCS), July 23, 2025. Springer, Zagreb, Croatia, 298–312. https://doi.org/10.1007/978-3-031-98685-7_14
[2] Philippe Heim and Rayna Dimitrova. 2025. Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis. Proc. ACM Program. Lang. 9, POPL (2025), 1536–1567. https://doi.org/10.1145/3704888
[3] Shaun Azzopardi, Luca Di Stefano, Nir Piterman, and Gerardo Schneider. 2025. Full LTL Synthesis over Infinite-State Arenas. In 37th International Conference on Computer Aided Verification (CAV) (LNCS), July 23, 2025. Springer, Zagreb, Croatia, 274–297. https://doi.org/10.1007/978-3-031-98685-7_13

[shaunazzopardi]

Also, then let us know the best performing configuration please, and we'll make sure to update any results to use that version.

[phheim]

Ah, okay, I see. There are several benchmarks where pruning used to be necessary, where, by now, the normal solving algorithm is quicker than the pruning itself. That is why in our latest evaluations we do not use pruning. There are, of course, still benchmarks where pruning helps.

In any case, my recommendation is to use Issy in its default mode, except if you want to probe for a specific technique. We try to maintain as the default what we think will, on average, be "the best".