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.
|Number of pages||23|
|Journal||Journal of Logical and Algebraic Methods in Programming|
|Publication status||Published - 1 Nov 2017|
Bibliographical noteFunding 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 .
© 2017 Elsevier Inc.
- Bounded nondeterminism
- Labelled transition systems
- Rule formats
- Structural operational semantics