On Synthesis and Verification from Event Diagrams in a Robot Theatre Application

We present a new type of expressions called Event Expressions (EE), and diagrams called Event Diagrams (ED), that are used to describe robot behaviors (motions). These diagrams are very general and include operators from many known representations, such as Regular Expressions, Boolean and Fuzzy Logic plus many new operators. Most importantly, EDs create probability operator counterparts for all these deterministic operators. They can be used for event acceptance or event generation. The diagrams are intended to simulate robot controllers and verify their correctness and properties.