A logic for n-dimensional hierarchical refinement

Alexandre Madeira
(HASLab INESC TEC & Universidade do Minho)
Manuel A. Martins
(CIDMA & Dep Matemática Universidade de Aveiro)
Luís S. Barbosa
(HASLab INESC TEC & Universidade do Minho)

Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalisms.

This paper introduces a hybrid modal logic for k-layered transition systems, its first-order standard translation, a notion of bisimulation, and a modal invariance result. Layered and hierarchical notions of refinement are also discussed in this setting.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 17th International Workshop on Refinement (Refine'15), Oslo, Norway, 22nd June 2015, Electronic Proceedings in Theoretical Computer Science 209, pp. 40–56.
Published: 4th June 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.209.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org