We present ABS, a software for Abstraction-Based Synthesis of controllers for continuous-state control systems. The tool distinguishes itself from previously known such software by being formally correct, i.e., any controller synthesized by ABS is mathematically guaranteed to solve the control problem provided as input. ABS achieves this quality by providing an input language with mathematically defined semantics and a respective compiler, and by carefully taking into account all numerical and rounding errors that might be incurred at either compile- or run-time. To mitigate computational overhead caused by the aforementioned approach, ABS implements, e.g. on-the-fly synthesis algorithms with greatly reduced memory requirement. The tool is currently applicable to invariance and reachability problems and requires state measurement. We discuss structure, algorithmic details and basic usage of ABS, and we demonstrate on two examples that its performance compares favorably with that of competing, not formally correct synthesis software. The source code of ABS is publicly available. See http://www.reiszig.de/gunther/pubs/ABS.html

Modeling and predicting human behavior is indispensable when industrial robots interacting with human operators are to be manipulated safely and efficiently. One challenge is that human operators tend to follow different motion patterns, depending on their intention and the structure of the environment. This precludes the use of classical estimation techniques based on kinematic or dynamic models, especially for the purpose of long-term prediction. In this paper, we propose a method based on Hidden Markov Models to predict the region of the workspace that is possibly occupied by the human within a prediction horizon. In contrast to predictions in the form of single points such as most likely human positions as obtained from previous approaches, the regions obtained here may serve as safety constraints when the robot motion is planned or optimized. This way one avoids collisions with a probability not less than a predefined threshold. The practicability of our method is demonstrated by successfully and accurately predicting the motion of a human arm in two scenarios involving multiple motion patterns.