Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A unified rule format for bounded nondeterminism in SOS with terms as labels

Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir

TL;DR

The paper addresses bounding nondeterminism in structural operational semantics for languages with higher-order, term-labeled transitions. It introduces dyadic transformations to convert triadic rules into a uniform dyadic form, and then defines S-types and restricted supports to robustly detect junk rules, yielding a general rule format that guarantees finite branching across a spectrum of bounded-nondeterminism properties. A key contribution is the formal theorem establishing that a dyadic-bounded, finitely-inhabited rule set ensures finite branching for the transformed system, which in turn implies bounded nondeterminism for the original triadic TSS. The approach is demonstrated on a MicroCHOCS-style subset of CHOCS, illustrating how image finiteness and finite branching can be obtained for distinct sub-systems of transitions. Overall, the work advances the theory of SOS rule formats for higher-order systems and lays groundwork for future extensions to nominal SOS and CHOCS-like congruence notions.

Abstract

We present a unified rule format for structural operational semantics with terms as labels that guarantees that the associated labelled transition system has some bounded-nondeterminism property. The properties we consider include finite branching, initials finiteness and image finiteness.

A unified rule format for bounded nondeterminism in SOS with terms as labels

TL;DR

The paper addresses bounding nondeterminism in structural operational semantics for languages with higher-order, term-labeled transitions. It introduces dyadic transformations to convert triadic rules into a uniform dyadic form, and then defines S-types and restricted supports to robustly detect junk rules, yielding a general rule format that guarantees finite branching across a spectrum of bounded-nondeterminism properties. A key contribution is the formal theorem establishing that a dyadic-bounded, finitely-inhabited rule set ensures finite branching for the transformed system, which in turn implies bounded nondeterminism for the original triadic TSS. The approach is demonstrated on a MicroCHOCS-style subset of CHOCS, illustrating how image finiteness and finite branching can be obtained for distinct sub-systems of transitions. Overall, the work advances the theory of SOS rule formats for higher-order systems and lays groundwork for future extensions to nominal SOS and CHOCS-like congruence notions.

Abstract

We present a unified rule format for structural operational semantics with terms as labels that guarantees that the associated labelled transition system has some bounded-nondeterminism property. The properties we consider include finite branching, initials finiteness and image finiteness.
Paper Structure (14 sections, 10 theorems, 24 equations, 3 figures)

This paper contains 14 sections, 10 theorems, 24 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Dyadic transformations
  4. Space of bounded-nondeterminism properties
  5. Junk rules and the $\eta$-types
  6. Refining the $\eta$-types
  7. Restricted support
  8. Targets of premises are important too
  9. Uniformity in the targets of premises
  10. Introducing the $S$-types
  11. Rule format for $\mathcal{D}_k^\mathit{prj}$-finiteness
  12. Application
  13. Future work
  14. Acknowledgements

Key Result

Lemma 1

Let $R$ be a triadic TSS with terms as labels and let $R'$ be the dyadic TSS obtained by applying to $R$ some dyadic transformation $\mathcal{D}_k$ with $1\leq k\leq 6$, i.e., $R'=\mathcal{D}_k(R)$. A transition $p\buildrel l\over\longrightarrow p'$ is provable in $R$ iff $\mathcal{D}_k(p\buildrel l

Figures (3)

  • Figure 1: Schematic representation of the properties in Definition \ref{['def:properties']}. The dots indicate that the components branch finitely (i.e., the indices $n$ and the $m$ are natural numbers), and the dashes indicate that the missing components can branch infinitely.
  • Figure 2: Hasse diagram of the properties in Definition \ref{['def:properties']}.
  • Figure 3: Inference rules for MicroCHOCS.

Theorems & Definitions (52)

  • Definition 1: Signature and Term
  • Definition 2: Formula
  • Definition 3: Substitution
  • Definition 4: Labelled transition system with processes as labels
  • Definition 5: Transition system specification with terms as labels
  • Definition 6: Unify with a rule
  • Definition 7: Proof tree
  • Definition 8: TSS induces LTS
  • Definition 10: Dyadic transformation
  • Example 1
  • ...and 42 more