Symbolic Bounded Synthesis

9 years 7 months ago
Symbolic Bounded Synthesis
Abstract. Synthesis of finite state systems from full linear time temporal logic (LTL) specifications is gaining more and more attention as several recent achievements have significantly improved its practical applicability. Many works in this area are based on the Safraless synthesis approach. Here, the computation is usually performed either in an explicit way or using symbolic data structures other than binary decision diagrams (BDDs). In this paper, we close this gap and consider Safraless synthesis using BDDs as state space representation. The key to this combination is the application of novel optimisation techniques which decrease the number of state bits in such a representation significantly. We evaluate our approach on several practical benchmarks, including a new load balancing case study. Our experiments show an improvement of several orders of magnitude over previous approaches.
Rüdiger Ehlers
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Rüdiger Ehlers
Comments (0)