A logic for n-dimensional hierarchical refinement
This work addresses the need for formal verification in software specification, but it appears incremental as it builds on existing hierarchical transition systems without claiming broad practical impact.
The paper tackles the problem of representing hierarchical state-based software applications by introducing a hybrid modal logic for k-layered transition systems, along with a first-order standard translation, bisimulation notion, and modal invariance result.
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.