OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Event algebra for transition systems composition Application to timed automata

Fares, Elie and Bodeveix, Jean-Paul and Filali, Mamoun Event algebra for transition systems composition Application to timed automata. (2018) Acta Informatica, 55. 363-400. ISSN 0001-5903

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
844kB

Official URL: https://doi.org/10.1007/s00236-017-0302-9

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 labelled 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 formal framework for reasoning on LTS, their semantics and related properties. Firstly, we define a high-level synchronization mechanism in the form of an abstract label structure and identify some properties. Then, we introduce operators for composing and transforming label structures, study their intrinsic properties and explore howlabel structure properties propagate. Secondly, we introduce a LTS-based behavioral framework. We then lift the label structure composition and transformation operator to the LTS level and establish LTS-related properties derived from those of their underlying labelled structures. Thirdly, we consider extended transition systems,more specifically timed automata, as LTS built on top of specific labelled structures. Their semantics is reconstructed by applying operators of our framework on the syntactic LTS, which allows the direct proof of some semantic properties such as compositionality

Item Type:Article
HAL Id:hal-02538359
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited On:30 Mar 2020 09:40

Repository Staff Only: item control page