We propose the
claim, which is a new construct for specifying the correctness properties that either finite or infinite
sequences of transitions
) that should
occur. In semantics, it is neither similar to
assertion, nor a simple combination of them. Furthermore, the theoretical foundation for checking
claims, namely the Asynchronous-Composition Büchi Automaton Control System (AC-BAC System), is proposed. The major contributions of the
claim include: a powerful construct for formalizing properties related to transitions and their labels, and a way for reducing the state space at the design stage.