OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Abstracting an Operational Semantics to Finite Automata

Baklanova, Nadezhda and Ricciotti, Wilmer and Smaus, Jan-Georg and Strecker, Martin Abstracting an Operational Semantics to Finite Automata. (2015) In: 11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015), 14 May 2015 - 16 May 2015 (Lviv, Ukraine).

(Document in English)

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

Official URL: https://doi.org/10.1007/978-3-319-30246-1_7


There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction mapping from semantics to automata and proving a simulation property seems to be easy. This paper aims at identifying the reasons why simple proofs break, among them artifacts in the semantics that lead to stuttering steps in the simulation. We then present a semantics based on the zipper data structure, with a direct interpretation of evaluation as navigation in the syntax tree. The abstraction function is then defined by an equivalence class construction.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Proceedings of ICTERI 2015: Information and Communication Technologies in Education, Research, and Industrial Applications ISBN 978-3-319-30245-4, part of volume 594 of the Communications in Computer and Information Science book series (CCIS) ISSN 1865-0929 The original PDF is available at: https://link.springer.com/chapter/10.1007%2F978-3-319-30246-1_7
HAL Id:hal-01782563
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited By: IRIT IRIT
Deposited On:30 Mar 2018 12:33

Repository Staff Only: item control page