A new model for model checking: cycle-weighted Kripke structure

This paper proposes a new model, named cycle-weighted Kripke structure (CWKS), based on the traditional Kripke structure. It adds two integer weights to some transitions of the Kripke structure, restricting when these transitions can occur. These weights mainly specify the occurrences of some cycles in a Kripke structure, giving a range of how many times these cycles may be executed repeatedly. This new model can efficiently describe some quantitative discrete-time characters of reactive and concurrent systems, so it is significant for some model checking problems. We also define a subset of CWKS, named conditional CWKS, which satisfies a constraint referring to the weighted transitions in the structure. The paper modifies the explicit computation tree logic (CTL) model checking algorithm to accommodate the conditional CWKS. It can also be regarded as the foundation of some more complex models obtained by extending from the Kripke structure, which will be studied in the future.