Event Algebra for Transition Systems Composition - Application to Timed Automata

Abstract

Formal specification languages have a lot of notions in common. They all introduce entities usually called processes, offer similar operators, and most importantly define their operational semantics based on labeled transition systems (LTS). However, each language defines specific synchronizing and/or memory structures. For instance, in CSP, the synchronization is defined between identical events, while in CCS and in synchronization vectors-based views it is defined respectively between complementary events or between possibly different events. In this paper, we aim at capturing some similarities of specification languages by defining a label-based composition formal framework. Firstly, we define a high-level synchronization mechanism in the form of an abstract label structure. We then couple this label structure with several compositional operations and properties. Secondly, we introduce an LTS-based behavioral framework and define a unique LTS composition operator which is reused to define syntactic composition of extended transition systems and a compositional semantics.