On the Meaning of Transition System Specifications

TL;DR

This paper introduces an alternative process graph semantics for Transition System Specifications that overcomes limitations of the classical closed-term semantics, ensuring better discrimination and preserving key semantic properties.

Contribution

It proposes a new process graph semantics for TSSs that avoids dependency on context and maintains important semantic equivalences and properties.

Findings

The new semantics is more discriminating for pure TSSs.

Four key semantic requirements under closed-term semantics imply their satisfaction under the new semantics.

The approach preserves compositionality, invariance, and recursive solution principles.

Abstract

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 closed-term 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 closed-term 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 $\alpha$-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.