Towards General Trace Theory
摘要
This paper investigates abstract semantical foundations for modelling and verifying concurrent systems by analysing the fundamental relationships between events that shape individual executions. We unify and generalise the established trace-based approaches by developing two label-free semantical frameworks: a step-based model grounded in stratified orders, and an interval-based model capturing observable durations through interval orders. Building on the view of traces as classes of equivalent executions, we introduce novel rewriting mechanisms (including a new rule for sequences of maximal antichains) that characterise these classes independently of concrete syntactic representations. Our approach employs closed relational structures as invariants of concurrent processes and studies their maximal extensions to derive canonical representatives of behaviours. The resulting trace-like equivalences provide, for the first time, an abstract treatment of unlabelled partial orders that isolates the essence of concurrent behaviour and has the potential to support more principled verification techniques.