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

doi:10.1016/j.jlamp.2017.03.002

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

Department of Computer Science

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

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.

Original language	English
Pages (from-to)	64-86
Number of pages	23
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	92
DOIs	https://doi.org/10.1016/j.jlamp.2017.03.002
Publication status	Published - 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

Access to Document

10.1016/j.jlamp.2017.03.002

Cite this

@article{ab003ae63ea04922aaecc8a8693e9db4,

title = "A unified rule format for bounded nondeterminism in SOS with terms as labels",

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.",

keywords = "Bounded nondeterminism, Labelled transition systems, Rule formats, Structural operational semantics",

author = "L. Aceto and I. F{\'a}bregas and A. Garc{\'i}a-P{\'e}rez and A. Ing{\'o}lfsd{\'o}ttir",

note = "Funding Information: This research has been supported by the project {\textquoteleft}Nominal Structural Operational Semantics{\textquoteright} (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{\'i}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: {\textcopyright} 2017 Elsevier Inc.",

year = "2017",

month = nov,

day = "1",

doi = "10.1016/j.jlamp.2017.03.002",

language = "English",

volume = "92",

pages = "64--86",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2208",

publisher = "Elsevier BV",

}

TY - JOUR

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

AU - Aceto, L.

AU - Fábregas, I.

AU - García-Pérez, A.

AU - Ingólfsdóttir, A.

N1 - 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.

PY - 2017/11/1

Y1 - 2017/11/1

N2 - 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.

AB - 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.

KW - Bounded nondeterminism

KW - Labelled transition systems

KW - Rule formats

KW - Structural operational semantics

UR - http://www.scopus.com/inward/record.url?scp=85016819567&partnerID=8YFLogxK

U2 - 10.1016/j.jlamp.2017.03.002

DO - 10.1016/j.jlamp.2017.03.002

M3 - Article

AN - SCOPUS:85016819567

VL - 92

SP - 64

EP - 86

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

ER -

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

Abstract

Bibliographical note

Other keywords

Access to Document

Fingerprint

Cite this