Synthesis of Trigger Properties
===============================

In automated synthesis, we transform a specification into a system
that is guaranteed to satisfy the specification. In spite of the rich
theory developed for temporal synthesis, little of this theory has
been reduced to practice. This is in contrast with model-checking
theory, which has led to industrial development and use of formal
verification tools. We address this problem here by considering a
certain class of PSL properties; this class covers most of the
properties used in practice by system designers. We refer to this
class as the class of trigger properties.

We show that the synthesis problem for trigger properties is more
amenable to implementation than that of general PSL properties.
While the problem is still 2EXPTIME-complete, it can be solved using
techniques that are significantly simpler than the techniques used in
general temporal synthesis. Not only can we avoid the use of Safra's
determinization, but we can also avoid the use of progress
ranks. Rather, the techniques used are based on classical subset
constructions.  This makes our approach amenable also to symbolic 
implementation, as well as an incremental implementation, in which the 
specification evolves over time.