Efficient derivation of environmental constraints for reactive system specifications

Specifications of reactive systems that interact with their environment must satisfy realizability: the property that the system can produce outputs satisfying the specification for any possible sequence of inputs from the environment. If a specification is not realizable, it must be revised. Environmental constraints usefully guide such revisions. An environmental constraint is a hidden assumption about environmental inputs that was unintentionally introduced during specification. Previous studies developed methods that derived environmental constraints, but these were not efficient. The principal bottleneck is construction of anω-automaton that represents all counterexample input patterns (input patterns for which no output can satisfy the specification). Here, we address this problem by proposing a new method that incrementally constructs the environmental constraint formula. We do not build anω-automaton such as that described above. Rather, our method efficiently identifies counterexample input patterns one-by-one and then progressively builds the constraint formula. We report experimental results showing that our approach outperforms previous methods in terms of efficiency.