Operational semantics

Formally verified animation for RoboChart using interaction trees

RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based …

Kangfeng Ye, Simon Foster, Jim Woodcock