On the Meaning of Transition System Specifications

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Transition System Specifications provide programming and specification languages with a semantics. They provide the meaning of a closed term as a process graph: a state in a labelled transition system. At the same time they provide the meaning of an n-ary operator, or more generally an open term with n free variables, as an n-ary operation on process graphs. The classical way of doing this, the closedterm semantics, reduces the meaning of an open term to the meaning of its closed instantiations. It makes the meaning of an operator dependent on the context in which it is employed. Here I propose an alternative process graph semantics of TSSs that does not suffer from this drawback. Semantic equivalences on process graphs can be lifted to open terms conform either the closedterm or the process graph semantics. For pure TSSs the latter is more discriminating. I consider five sanity requirements on the semantics of programming and specification languages equipped with a recursion construct: compositionality, applied to n-ary operators, recursion and variables, invariance under α-conversion, and the recursive definition principle, saying that the meaning of a recursive call should be a solution of the corresponding recursion equations. I establish that the satisfaction of four of these requirements under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics.
Original languageEnglish
Title of host publication6th International Workshop on Expressiveness in Concurrency 6th Workshop on Structural Operational Semantics, The Netherlands, 26th August 2019
EditorsJ.A. Pérez, J. Rot
PublisherOpen Publishing Association
Pages69-85
Number of pages17
Volume300
DOIs
Publication statusPublished - 22 Aug 2019
Event30th International Conference on Concurrency Theory (CONCUR 2019) - Amsterdam, Netherlands
Duration: 26 Aug 201931 Aug 2019
https://event.cwi.nl/concur2019/

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume300
ISSN (Electronic)2075-2180

Workshop

Workshop30th International Conference on Concurrency Theory (CONCUR 2019)
Abbreviated titleCONCUR 2019
Country/TerritoryNetherlands
CityAmsterdam
Period26/08/1931/08/19
Internet address

Fingerprint

Dive into the research topics of 'On the Meaning of Transition System Specifications'. Together they form a unique fingerprint.

Cite this