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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Towards General Trace Theory

  • Ryszard Janicki,
  • Maciej Koutny,
  • Łukasz Mikulski,
  • Rajiv Ranjan

摘要

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.