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.
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01220607
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Monday, October 26, 2015 - 4:07:04 PM
Last modification on : Thursday, October 24, 2019 - 2:44:10 PM
Long-term archiving on : Wednesday, January 27, 2016 - 4:30:21 PM

File

fares_12720.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01220607, version 1
  • OATAO : 12720

Citation

Elie Fares, Jean-Paul Bodeveix, Mamoun Filali. Event Algebra for Transition Systems Composition - Application to Timed Automata. 20th International Symposium on Temporal Representation and Reasoning (TIME 2013), Sep 2013, Penscacolq, FL, United States. pp. 125-132. ⟨hal-01220607⟩

Share

Metrics

Record views

273

Files downloads

149