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

L. Aceto*, I. Fábregas, A. García-Pérez, A. Ingólfsdóttir

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)64-86
Number of pages23
JournalJournal of Logical and Algebraic Methods in Programming
Publication statusPublished - 1 Nov 2017

Bibliographical note

Funding Information:
This research has been supported by the project ‘Nominal Structural Operational Semantics’ (nr. 141558-051 ) of the Icelandic Research Fund , the projects StrongSoft ( TIN2012-39391-C04–04 ) and TRACES ( TIN2015-67522-C3-3-R ) of the Spanish Ministerio de Economía y Competitividad , the project 001-ABEL-CM-2013 within the NILS Science and Sustainability Programme, and the grant GR3/14 of the Universidad Complutense de Madrid – Banco Santander .

Publisher Copyright:
© 2017 Elsevier Inc.

Other keywords

  • Bounded nondeterminism
  • Labelled transition systems
  • Rule formats
  • Structural operational semantics


Dive into the research topics of 'A unified rule format for bounded nondeterminism in SOS with terms as labels'. Together they form a unique fingerprint.

Cite this