Mathematical Structures in Computer Science

Paper

Extending modal transition systems with structured labels

SEBASTIAN S. BAUERa1, LINE JUHLa2, KIM G. LARSENa3, AXEL LEGAYa4 and JIŘÍ SRBAa5

a1 Institut für Informatik, Ludwig-Maximilians-Universität München, München, Germany Email: bauerse@pst.ifi.lmu.de

a2 Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220 Aalborg Ø, Denmark Email: linej@cs.aau.dk

a3 Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220 Aalborg Ø, Denmark Email: kgl@cs.aau.dk

a4 INRIA/IRISA, Rennes, France Email: axel.legay@irisa.fr

a5 Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220 Aalborg Ø, Denmark Email: srba@cs.aau.dk

Abstract

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 system developers to employ more complex label refinement than in 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, determinisation, parallel composition, conjunction, quotient and logical characterisation of label-structured modal transition systems.

(Received December 22 2010)

(Revised November 02 2011)

(Online publication May 08 2012)

Footnotes

Sebastian Bauer is partially supported by the German Academic Exchange Service (DAAD), grant D/10/46169, and by MT-LAB, VKR Centre of Excellence.

Axel Legay is partially supported by an ‘action de recherche collaborative’ ARC (TP)I, INRIA and the European Project COMBEST.