TY - JOUR

T1 - Extending Modal Transition Systems with Structured Labels

A1 - Bauer,Sebastian S.

A1 - Juhl,Line

A1 - Larsen,Kim Guldstrand

A1 - Legay,Axel

A1 - Srba,Jiri

AU - Bauer,Sebastian S.

AU - Juhl,Line

AU - Larsen,Kim Guldstrand

AU - Legay,Axel

AU - Srba,Jiri

PB - Cambridge University Press

PY - 2012/5/8

Y1 - 2012/5/8

N2 - We introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification formalism is general enough to include models like weighted modal transition systems and allows the system developers to employ more complex label refinement than in the previously studied theories. On the other hand, the formalism maintains the desirable properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough refinement, determinization, parallel composition, conjunction, quotient, and logical characterization of label-structured modal transition systems.

AB - We introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification formalism is general enough to include models like weighted modal transition systems and allows the system developers to employ more complex label refinement than in the previously studied theories. On the other hand, the formalism maintains the desirable properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough refinement, determinization, parallel composition, conjunction, quotient, and logical characterization of label-structured modal transition systems.

UR - http://www.scopus.com/record/display.url?eid=2-s2.0-84863959617&origin=resultslist&sort=plf-f&src=s&sid=7ANRXJ4yeBntcN4OFYYErZD%3a70&sot=aut&sdt=a&sl=31&s=AU-ID%28%22Juhl%2c+Line%22+50161726000%29&relpos=1&relpos=1&searchTerm=AU-ID(\%22Juhl,%20Line\%22%2050161726000)

U2 - 10.1017/S0960129511000697

DO - 10.1017/S0960129511000697

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 4

VL - 22

SP - 581

EP - 617

ER -