Framework I - A network of robots is modeled as a network of multi-modal hybrid automata. The notion of bisimulations is used to abstract robots in the network. The result is a network of interacting timed automata which allows coordination among the robots and timing constraints to be considered. The model checker UPPAAL is used for formal symbolic model checking against a requirement specification in Computational Tree Logic (CTL) for a network of robots. The result is a set of motion plans for the robots which satisfy the specification.
Framework II - A framework for controller synthesis for a single robot with respect to requirement specification in Linear-time Temporal Logic (LTL) is presented. The notion of bisimulations is used to find an abstraction of the robot. The abstraction is subsequently used for controller synthesis together with the formal specification. Since the abstraction and the original system are bisimilar the discrete controller synthesized for the abstraction will equivalently work for the original system.
|Effektiv start/slut dato||01/09/2002 → 31/05/2007|
- <ingen navn>