Implementation of Decision Procedure of Stepwise Satisfiability of 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. This paper implements stepwise satisfiability decision procedure with tableau method and proof system. Stepwise satisfiability is one of the necessary conditions of realizability of reactive system specifications. The proposed procedure decides stepwise satisfiability of reactive system specifications.