States and Events in KandISTI

Early work on automated formal verification produced pioneering model-checking algorithms, in which system computations were modelled either as sequences of distinguished states in which the system evolves or as sequences of events or actions occurring during the system’s state transitions. In both cases, automata-like structures generally known as transition systems were exploited to capture all possible computations, but still either state-based or event-based. Many years later, both views were combined in descriptions of computations as the evolution between distinguished states by means of transitions characterised by the occurrence of events, and verification tools were adapted to this more general setting. Meanwhile, the most important drive in improving verification tools concerned the complexity of models, which was attacked by algorithms capable of minimising the information needed for deciding the verification questions. One of the outcomes of this quest was local, on-the-fly model checking. Both of these lines of research, pioneered by Bernhard Steffen, are discussed in this paper in a general retrospective on state-based and event-based models of transition systems and temporal logics, followed by an overview of how this is exploited in the KandISTI model-checking environment.