  This paper provides the first correct semantical representation of UML
state-machines within the logical framework of an institution (previous
attempts were flawed). A novel encoding of this representation into first-order
logic enables symbolic analyses through a multitude of theorem-provers.
  UML state-machines are central to model-based systems-engineering. Till now,
state-machine analysis has been mostly restricted to model checking, which for
state-machines suffers heavily from the state-space explosion problem. Symbolic
reasoning, as enabled and demonstrated here, provides a powerful alternative,
which can deal with large or even infinite state spaces.
  Full proofs are given.
