Several Strategies of Reactive System Program Synthesis

摘要

Reactive systems, such as operating systems or elevator control systems, are systems that ideally never terminate and are intended to maintain some interaction with their environment. Temporal logic is one of the methods for formal specification descriptions of reactive systems. By describing the formal specifications of reactive systems we can check the consistency of the specifications and whether they contain defects. By using a synthesis algorithm we also obtain reactive system programs from the formal specifications and prevent programming bugs. Therefore, it is important to describe reactive system formal specifications to reactive system programs. However, this algorithm synthesizes several reactive system programs from the formal specifications and it is supposed that some programs are good and some are bad. Thus, we have to choose the good programs for this specification among these reactive system programs. In this paper, we propose several strategies reactive system program synthesis to choose the efficient or good reactive system program among synthesized programs.