Stepwise satisfiability checking procedure for reactive system specifications by tableau method and proof system

Abstract

Open reactive 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 description of open reactive systems. For an open reactive system specification, we do not always obtain a program satisfying it because the open reactive system program must satisfy the specification no matter how the environment of the open reactive system behaves. This problem is known as realizability and the complexity of realizability check is double or triple exponential time of the length of specification formula and realizability checking of specifications is impractical. This paper implements stepwise satisfiability checking procedure with tableau method and proof system. Stepwise satisfiability is one of the necessary conditions of realizability of reactive system specifications. The implemented procedure uses proof system that is introduced in this paper. This proof system can accelerate the decision procedure, but since it is imcomplete it cannot itself decide the realizability property of specifications. The experiment of this paper shows that the implemented procedure can decide the realizability property of several specifications. © 2012 Springer-Verlag.