A compositional semantics for statecharts using labeled transition systems

We characterize the statecharts step semantics of Pnueli and Shalev as a mapping Psi from an inductively defined algebra of statecharts terms to a domain of labeled transition systems (LTSs). Statecharts equivalence =(sc), i.e. LTS isomorphism, is shown not to be a congruence and hence the step semantics is not compositional. We define a new semantic mapping Psi(>) to a domain of LTSs with a richer label structure, and show that LTS isomorphism in this domain is the largest congruence contained in =(sc).