Extracting Environmental Constraints in Reactive System Specifications

Reactive systems ideally never terminate and maintain some interaction with their environment. Temporal logic is one of the methods for formal specification description of reactive systems. For a reactive system specification, we do not always obtain a program that satisfies it because the reactive system program must satisfy the specification no matter how the environment of the reactive system behaves. This problem is known as realizability or feasibility. The complexity of deciding realizability of specifications that are described in linear temporal logic is double or triple exponential time of the length of specifications and realizability decision is impractical. To check reactive system specifications, Strong satisfiability is one of the necessary conditions of realizability of reactive system specifications. If a reactive system specification is not strong satisfiable, it is necessary to revise the specification. This paper proposes the method of revising reactive system specifications that are not strong satisfiable. This method extracts environmental constraints that are included in reactive system specifications.