June 16-24, 2008 DTU - Lyngby, Denmark | organised and funded by ARTIST |
Monday | ||
Morning | Introduction to the course, modeling of finite-state systems | |
Afternoon | Computation tree logic (CTL) and CTL model checking | |
Tuesday- Symbolic methods I: Finite state | ||
Morning | Circuit equivalence and propositional SAT solving | |
Afternoon | Symbolic representation of transition systems, reachability (both bounded and full), symbolic CTL model checking | |
Wednesday - Symbolic methods II: Hybrid state | ||
Morning | Hybrid discrete-continuous automata models | |
Afternoon: | Verification by approximation | |
Thursday - Symbolic techniques III: Satisfiability for large arithmetic formulae | ||
Morning | SAT modulo theory | |
Afternoon | Lab exercises | |
Friday - Symbolic techniques III: Satisfiability for large arithmetic formulae | ||
Morning | Robust semantics of arithmetic formulae, satisfiability procedures for undecidable arithmetic | |
Afternoon | Lab exercises | |
Monday | ||
A strong interest shift from single robot to mulrirobot systems has been taken place in robotics during recent years. Multirobot systems are considered as physically embodied multi agent systems constrained with the laws of physics. Planning and coordination of multirobot systems are generally approached with a centralized controller in mind. Coordination methods for systems involving large number of robots like in robot swarms can be scaled up by using fully distributed coordination architectures only. That sets a new challenge to formal methods supporting the design and verification of multirobot systems. | ||
The focus of this course is on techniques and software-tools that can be used to assess the quality and correctness of multirobot systems’ behavior. The course emphasizes tools and techniques for model-based development and formal verification of multirobot system designs, particularly for model construction, model-based reactive planning and mission verification. The topic is illustrated with two case-studies: synthesis of the planning unit for an assistive Scrub Nurse Robot and verification of a self-stabilizing robot swarm coordination algorithm. The course will contain a mix of lecturing and hands-on exercises especially built around the Uppaal tool suite. | ||
Tuesday | ||
To be decided |
(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009