Well Structured Transition Systems with History

TL;DR

This paper introduces a formal model of concurrent systems that explicitly incorporates historical event data, enabling enhanced verification techniques and extending the applicability of well-structured transition systems to historical data analysis.

Contribution

It formalizes a new model integrating history into transition systems and extends wsts theory to verify properties involving historical information.

Findings

Model allows explicit historical data representation in system configurations.

Extends verification capabilities of wsts to include historical event data.

Facilitates symbolic trace reconstruction using historical meta-information.

Abstract

We propose a formal model of concurrent systems in which the history of a computation is explicitly represented as a collection of events that provide a view of a sequence of configurations. In our model events generated by transitions become part of the system configurations leading to operational semantics with historical data. This model allows us to formalize what is usually done in symbolic verification algorithms. Indeed, search algorithms often use meta-information, e.g., names of fired transitions, selected processes, etc., to reconstruct (error) traces from symbolic state exploration. The other interesting point of the proposed model is related to a possible new application of the theory of well-structured transition systems (wsts). In our setting wsts theory can be applied to formally extend the class of properties that can be verified using coverability to take into consideration (ordered and unordered) historical data. This can be done by using different types of representation of collections of events and by combining them with wsts by using closure properties of well-quasi orderings.