Structured operational semantics for concurrency and hierarchy

Abstract

This paper presents a language, CHA, and semantics for studying Statechartslike drawings. CHA is a process algebra. CHA terms are interpreted as programs that extend Mealy-style finite automata with concurrent execution and hierarchical structure. Transitions in CHA can cross hierarchy boundaries, and it is this fact that makes giving a semantics to CIIA (and to Statecharts) an interesting problem. In the terminology of [Mil89] all of the function symbols in CHA except the constants are static combinators. CHA is given an operational semantics in the Structural Operational Semantics (SOS) style of Plotkin [PI08I]. The Transition System Specification (TSS) methodology of [GV88] is employed, and the TSS presented is in the ty ft/tyxt format from that paper. Conformance to the tyft/tyxt format has several benefits for analyzing CHA, the most important of which is that bisimulation is a congruence in the Labeled Transition System (LTS) C of the language.