QUARTERLY PROGRESS REPORT CONTRACTOR: University of California at Berkeley AGREEMENT NUMBER: F33615-98-C-3614 CONTRACT PERIOD: 9/1/99 - 12/31/03 TITLE: Integrated Design and Analysis Tools for Software Based Control Systems REPORT PERIOD: 1/1/03 - 3/31/03 SPONSOR: Air Force Research Laboratory (AFRL) TECHNICAL POC: Ray Bortner REPORT PREPARED BY: Edward Lee (eal@eecs.berkeley.edu) 0. Executive Summary Our effort integrates three tasks: formal modeling and verification; embedded software design; and controller design and analysis. We made substantial progress in all three directions. Some of the highlights include: we developed a new, robust model and corresponding theory for timed, hybrid, and probabilistic systems, based on the idea of discounting; we demonstrated distributed control for the Caltech ducted fan vehicle and introduced the concept of migrating models; and we realized a Giotto/E-Machine code generator from Ptolemy II. 1. Research Status Formal Modeling and Analysis ============================ Discounting the Future in Systems Theory ----------------------------------------- Discounting the future means that the value, today, of a unit payoff is 1 if the payoff occurs today, a if it occurs tomorrow, a^2 if it occurs the day after tomorrow, and so on, for some real-valued discount factor 0 < a < 1. Discounting (or inflation) is a key paradigm in economics and has been studied in Markov decision processes as well as game theory. We submit that discounting also has a natural place in systems engineering: for nonterminating systems, a potential bug in the far-away future is less troubling than a potential bug today. We therefore developed a systems theory with discounting. Our theory includes several basic elements: discounted versions of system properties that correspond to the omega-regular properties, fixpoint-based algorithms for checking discounted properties, and a quantitative notion of bisimilarity for capturing the difference between two states with respect to discounted properties. We developed the theory in a general form that applies to probabilistic systems as well as multicomponent systems (games), but it readily specializes to classical transition systems. We showed that discounting, besides its natural practical appeal, has also several mathematical benefits. First, the resulting theory is robust, in that small perturbations of a system can cause only small changes in the properties of the system. This is of particular relevance for hybrid systems, where the classical models are not robust. Second, the theory is computational, in that the values of discounted properties, as well as the discounted bisimilarity distance between states, can be computed to any desired degree of precision. Counterexample-guided Control ----------------------------- A major hurdle in the algorithmic verification and control of systems is the need to find suitable abstract models, which omit enough details to overcome the state-explosion problem, but retain enough details to exhibit satisfaction or controllability with respect to the specification. The paradigm of counterexample-guided abstraction refinement suggests a fully automatic way of finding suitable abstract models: one starts with a coarse abstraction, attempts to verify or control the abstract model, and if this attempt fails and the abstract counterexample does not correspond to a concrete counterexample, then one uses the spurious counterexample to guide the refinement of the abstract model. We developed a counterexample-guided refinement algorithm for solving omega-regular control objectives. The main difficulty is that in control, unlike in verification, counterexamples are strategies in a game between system and controller. In the case that the controller has no choices, our scheme subsumes known counterexample-guided refinement algorithms for the verification of omega-regular specifications. Our algorithm is useful in all situations where omega-regular games need to be solved, such as supervisory control, sequential and program synthesis, and modular verification. The algorithm is fully symbolic, and therefore applicable also to infinite-state systems. Stack-size Analysis for Interrupt-driven Programs ------------------------------------------------- We solved the problems of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we showed that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we considered, the two problems are PSPACE-hard and can be solved in exponential time. Embedded Software Design ======================== Giotto and the E Machine ------------------------ Steve Neuendorffer, Marco Sanvido, Christoph Kirsch were able to automatically generate code from a Giotto model in Ptolemy, and target the embedded machine. Task code is generated from SDF models, E machine drivers are generated from the connectivity in the model, and the Giotto compiler is used to generate the E machine code. This heavily leveraged Haiyang Zheng's previous work generating Giotto code from Ptolemy. Essentially they filled in the drivers and task code using code generated using Copernicus. Currently, only single mode systems are supported, and the Giotto model is assumed to be at the top level. This work was cooperative with Mobies. Open Control Platform --------------------- Steve Neuendorffer and Yang Zhao attended the OCP workshop in January at Caltech. They tested some of the concepts that we have been working on, and came away with a few observations. Steve Neuendorffer tested his "crazyboard" controller models, built in Ptolemy II, on the Caltech hardware. There was one laptop sitting on the Crazyboard and running a very simple model to receive control commands, and there was another laptop that runs the control algorithm remotely and sends commands to the laptop on the Crazyboard. The reason for two laptops is that they wanted to test different control algorithms and modify algorithms conveniently. But this approach has a drawback: the latency is quite big due to the control being over the network. Yang and Steve have suggested an alternative architecture where the control law is implemented in a migrating model that is transported over the network and executed locally. Yang built an experimental setup where a MobileModel actor accepts a model over the network and executes that model to process streaming inputs. The model can be updated in real time by a supervisory model on the second laptop, but the control loop no longer includes the network, thus greatly improving performance. This work continues, with the objective of building an infrastructure that is easy for control systems designers to use. Yang has also experimented with using JXTA to discover control services and Crazyboard configurations. JXTA is a discovery infrastructure from Sun Microsystems. A key observation that Yang and Steve made is that there is a need for a modeling and simulation environment for developers designing distributed systems based on OCP. Designers today can use Simulink to draw the component diagram of a system, but they cannot do the simulation in Simulink since it does not provide the proper semantics. It would be possible to build a Ptolemy II domain with OCP semantics that might serve this purpose. Controller Design and Analysis ============================== Nonlinear Model Predictive Planning and Control ----------------------------------------------- H. Jin Kim presented nonlinear model predictive planning & control framework which combines trajectory planning and control into a single problem, using ideas from potential-field based navigation for real-time path planning and nonlinear model predictive control for optimal control of nonlinear multi-input, multi-output systems with input/state constraints. She incorporates a tracking performance, potential function, state constraints into the cost function to minimize, and use gradient-descent for on-line optimization. A scenario with three UAVs which are given straight line trajectories that will lead to collision is considered. By using the framework, the safe trajectory of the vehicles are dynamically replanned and tracked by the vehicles under input saturation and state constraints. Optimization-based Formation Reconfiguration Planning For Autonomous Vehicles ----------------------------------------------------------------------------- Given a group of autonomous vehicles, an initial configuration, a final configuration, a set of inter- and intra-vehicle constraints, and a time for reconfiguration, the Formation Reconfiguration Planning problem is focused on determining a nominal input trajectory for each vehicle such that the group can start from the initial configuration and reach its final configuration at the specified time while satisfying the set of inter- and intra- vehicle constraints. S. Zelinski, T. J. Koo, and S. Sastry were interested in solving the Formation Reconfiguration Planning problem for a specific class of systems and a particular form of input signals so that the problem can be reformulated as an optimization problem which can be solved more efficiently, especially for a large group of vehicles. Optimization has proved to be a successful solution to the FRP problem. Our method of implementation is general and portable allowing for use in a wide range of applications for coordinated robots. For example, our method could easily be transported to two dimensions for ground robot coordination. This centralized control scheme has limitations in applications where formations are very large or communication is disrupted. For such applications, a decentralized control scheme is preferred. We are currently working on a decentralized approach to the FRP problem where each vehicle produces its own localized solution based on only local sensor information about its neighboring vehicles. As expected, this is proving to be a more complex problem. Therefore, centralized control is preferred in applications for smaller fully connected formations. Platform-Based Embedded Software Design and System Integration for Autonomous Vehicles ------------------------------------------------------------------ B. Horowitz, J. Liebman, C. Ma, T. J. Koo, A. Sangiovanni-Vincentelli, and S. Sastry used the concepts of platform-based design to develop a methodology for the design of automatic control systems that built in modularity and correct-by-construction procedures. We illustrated our strategy by describing the application of the methodology to the design of a time-based control system for a helicopter-based Uninhabited Aerial Vehicle (UAV) so that the following objectives can be met: a. The use of platform-based design allows us to build a bridge between the time-based controller application and the non-time-based sensors and actuators. b. A time-based controller eliminates the timing irregularities present in first generation system. Further, the Giotto compiler ensures that the controller application meets its timing requirements. c. Our platform-based design achieves a high degree of modularity. For example, to substitute a different sensor suite in our first redesign requires only changes to the data processor and the data formatting library. The data processor would require a different sensor initialization routine and a new circular buffer; the formatting library would need a new format conversion routine. However, no part of the controller application would need to be changed. 2. Interactions and Technology Transfer Presentations ------------- Interactions ------------ * Steve Neuendorffer and Yang Zhao attended the OCP workshop in January. Technology Transfer ------------------- T. John Koo, Ian M. Mitchell, Slobodan N. Simic and S. Shankar Sastry were teaching a graduate course on "Hybrid Systems" in the Dept. of EECS at UC Berkeley. Personnel --------- No personnel changes. 4. Publications [1] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. Proceedings of the 30th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science, Springer-Verlag, 2003. [2] Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample guided control. Proceedings of the 30th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science, Springer-Verlag, 2003. [3] Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, and Jens Palsberg. Stack size analysis for interrupt-driven programs. Proceedings of the Tenth International Static Analysis Symposium (SAS), Lecture Notes in Computer Science, Springer-Verlag, 2003. [4] Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch. Giotto: A time-triggered language for embedded programming. Proceedings of the IEEE 91:84-99, 2003. [5] Thomas A. Henzinger, Christoph M. Kirsch, Marco A.A. Sanvido, and Wolfgang Pree. From control models to real-time code using Giotto. IEEE Control Systems Magazine 23(1):50-64, 2003. [6] Johan Eker, Jörn W. Janneck, Edward A. Lee, Jie Liu, Xiaojun Liu, Jozsef Ludvig, Stephen Neuendorffer, Sonia Sachs, Yuhong Xiong, "Taming Heterogeneity---the Ptolemy Approach," Proceedings of the IEEE, v.91, No. 2, January 2003 (with Mobies). [7] Jie Liu, Johan Eker, Jörn W. Janneck, Xiaojun Liu, and Edward A. Lee, "Actor-Oriented Control System Design: A Responsible Framework Perspective," accepted to IEEE Transactions on Control System Technology, March, 2003 (with Mobies). [8] S. Zelinski, T. J. Koo, and S. Sastry, " Optimization-based Formation Reconfiguration Planning For Autonomous Vehicles," submitted to the International Conference on Robotics and Automation, Taipei, Taiwan, May 2003. [9] T. J. Koo, S. Zelinski, and S. Sastry, "Formation Reconfiguration For Autonomous Vehicles," submitted to the AHS 59th Annual Forum and Technology Display, Vertical Flight Transformations, Phoenix, Arizona, May 6-8, 2003 5. Financial Data Provided separately on a quarterly basis by the university.