As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Reactive synthesis is a technology for the automatic construction of reactive systems from logical specifications. In these lecture notes, we study different algorithms for the reactive synthesis problem of linear-time temporal logic (LTL). The classic game-based synthesis algorithm is input-sensitive in the sense that its performance is asymptotically optimal in the size of the specification, but it produces implementations that may be larger than necessary. We contrast this algorithm with output-sensitive algorithms for reactive synthesis, i.e., algorithms that are optimized towards the size or structural complexity of the synthesized system. We study the bounded synthesis algorithm, which produces an implementation with a minimal number of states, and the bounded cycle synthesis algorithm, which additionally guarantees that the number of cycles of the implementation is minimal.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.