Towards provably safe control for smart wheelchairs

Meeko Oishi and Nikolai Matni

Abstract

We propose verification techniques from hybrid control theory to address safety issues in the indoor operation of powered wheelchairs. Verification through hybrid system reachability can provide a mathematical guarantee of safety, where safety is defined as the ability of the system to remain within a desired subset of the state-space. Current eorts are in developing a general algorithm for verification in semi-automated systems, general methods for implementation of control laws for safety, and in the development of an instrumented smart wheelchair testbed at UBC.

Introduction

In Canada, approximately 176,000 seniors with disabilities reside in long-term care facilities as of 2001 (Can 2005). This number will continue to grow as Canada's population inexorably ages. While many of these residents would benefit from access to powered wheelchairs, which can provide more mobility, greater independence, and significantly improve quality of life, unsafe operation can be hazardous to the operator, other residents, staff, and the facility itself.

Driving conditions are a significant factor in many accidents involving powered wheelchairs (Mortenson et al. 2006). Powered mobility users must navigate precisely around fixed obstacles (e.g., carts, custodial equipment) in narrow hallways, through narrow doorways, and around tight corners. In addition, powered mobility users face moving obstacles which include other wheelchair users and walkers, each traveling at a wide range of speeds. Smart wheelchairs that can to reduce or even eliminate collisions or near-collisions with fixed and mobile obstacles have the potential to reduce the liability associated with powered wheelchairs in residential care facilities (Pineau et al. 2003; Cooper 2008; Parikh et al. 2007; Rotenstein et al. 2007; Simpson 2005; Mihailidis et al. 2007).

We aim to improve the safety of powered wheelchair use through verification techniques that can provide mathematical guarantees of safety. Computational techniques for verification (e.g., reachability analysis) can create a new level of confidence and reliability in safety-critical systems such as smart wheelchairs, by predicting where failures might occur, and how human operators can predict them (Oishi et al. 2008). These methods are based in hybrid control theory, in which both continuous dynamics (from physical processes) and discrete dynamics (from the automation's mode-logic) are modeled. Verification provides a mathematical guarantee of safety, where safety is defined as the ability to remain within a desired set in the statespace, despite bounded control authority. These techniques involve quantifying "bad" behavior, then identifying configurations that could lead to the bad region of operation. By eliminating those configurations, safety is ensured. In previous applications to aircraft flight management systems, bad regions represented speeds below which an aircraft could stall (Tomlin et al. 2003).

While repeated simulation can provide intuition about how a given system will behave, results are highly dependent on the particular initial conditions chosen. It is impossible to simulate system trajectories from all initial conditions and for all inputs, and therefore impossible to determine all possible outcomes through simulation. However, reachability analysis can provide information about outcomes from an infinite number of initial conditions within a bounded set. The reachability computation is accomplished by evolving the boundary of the set backwards in time according to the system's dynamics. We draw upon level set methods that can handle general nonlinear systems, such as powered wheelchair dynamics, with bounded inputs and disturbances (Mitchell, Bayen, and Tomlin 2005).

In semi-automated hybrid systems, such as smart powered wheelchairs, it is vital that the automation and the user eectively share control of the system. Depending on the specific wheelchair setup, the user can provide either discrete inputs (e.g. pushing buttons, toggling levers) and/or continuous inputs (e.g. joystick control). The user-interface both provides information to the user about the underlying automation, and allows the user to issue input commands to the system. Any potential conflicts between the automation's input and the user's input must be resolved, and communicated to the user such that the user understands the state of the automation and can easily predict its evolution (Sheridan 1999). Humanautomation interaction problems can be dificult to detect through simple inspection (Sarter andWoods 1995; Degani and Heymann 2002; Oishi et al. 2002; Umeno and Lynch 2007), hence our work is in extending verification techniques for standard, fully-automated systems to accommodate semi-automated hybrid systems.

While a highly trained, specialized group of users, such as pilots, may exhibit a great deal of uniformity in their interaction with automation, users of assistive technologies will have significantly more variation in their interaction with automation, depending on their particular physical and/or cognitive disabilities. Our approach therefore is to model the user's intent by specifying broad bounds on what the user can do, rather than trying to model an individual user's or prototype user's dynamics. This allows us to capture the user's intent in a way that is mathematically tractable for hybrid system verification techniques. Standard control techniques assume unlikely extremes (that the human is acting as precisely as an automation, or alternatively, that the human is a disturbance actively driving the system to unsafety). Neither of these captures the types of inadvertent mishaps that occur in many systems.

Recently we have explored how the verification algorithm for semi-automated systems diers depending on the type of user-input (Matni and Oishi 2008). We are currently designing generic algorithms for user-interface design based on our modified application of reachability analysis for safety verification in semi-automated systems, and implementing our computational results onboard actual physical testbeds. We describe our efforts to implement the reachability calculation on a physical system (discretized over space and time) in a manner which upholds the desired safety guarantees.

Experimental testbed

A vision-based LEGO NXT robot testbed has been built to test and validate general algorithms for verification of semi-automated systems and implementation of safe control laws. The system operates as either a fullyautonomous or semi-autonomous platform. Users can interact with a variety of GUIs to mimic discrete and continuous user-inputs. This testbed provides an inexpensive, low-risk platform for testing new algorithms.

In addition, we are building a two-wheelchair testbed with fully instrumented powered wheelchairs and indoor GPS for ground-truthing. The wheelchair testbed will enable physical testing and validation of reachability-based algorithms for provably safe control of semi-autonomous powered wheelchairs.

References

1. 2005. Advancing the inclusion of people with disabilities. Technical Report SD23-4/2005E, Government of Canada, Canada.
2. Cooper, R. 2008. Quality-of-life technology. IEEE Engineering in Medicine and Biology 27(2):10-11.
3. Degani, A., and Heymann, M. 2002. Formal verification of human-automation interaction. Human Factors 44(1):28-43.
4. Matni, N., and Oishi, M. 2008. Reachability-based abstraction for an aircraft landing under shared control. In Proc of the American Control Conf.
5. Mihailidis, A.; Elinas, P.; Boger, J.; and Hoey, J. 2007. An intelligent powered wheelchair to enable mobility of cognitively impaired older adults: An anticollision system. IEEE Transactions on Neural Systems and Rehabilitation Engineering 15(1):136-143.