Automata-based Verification of Linear Temporal Logic Models with Bounded Variability

A model has variability bounded by v/k when the state changes at most v times over any linear interval containing k time instants. When interpreted over models with bounded variability, specification formulae that contain redundant metric information---through the usage of next operators---can be simplified without affecting their validity. This paper shows how to harness this simplification in practice: we present a translation of LTL into B\ufcchi automata that removes redundant metric information, hence makes for more efficient verification over models with bounded variability. To show the feasibility of the approach, we also implement a proof-of-concept translation in ProMeLa and verify it using the Spin off-the-shelf model-checker