2019
Contribution to book  Open Access

States and Events in KandISTI: A Retrospective

Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F.

Modal Transition Systems  KandISTI  Model checking  Temporal logic 

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.

Source: Models, Mindsets, Meta: The What, the How, and the Why Not?, edited by Margaria T.; Graf S.; Larsen K.G., pp. 110–128. Berlin: Springer, 2019

Publisher: Springer, Berlin, DEU


Metrics



Back to previous page
BibTeX entry
@inbook{oai:it.cnr:prodotti:403887,
	title = {States and Events in KandISTI: A Retrospective},
	author = {Ter Beek M.  H. and Fantechi A. and Gnesi S. and Mazzanti F.},
	publisher = {Springer, Berlin, DEU},
	doi = {10.1007/978-3-030-22348-9_8},
	booktitle = {Models, Mindsets, Meta: The What, the How, and the Why Not?, edited by Margaria T.; Graf S.; Larsen K.G., pp. 110–128. Berlin: Springer, 2019},
	year = {2019}
}