Anil Nerode on hybrid systems control

Luke Muehlhauser: In Nerode (2007), you tell the origin story of hybrid systems control. A 1990 DARPA meeting in Pacifica seems to have been particularly seminal. As you describe it:

the purpose of the meeting was to explore how to clear a major bottleneck, the control of large military systems such as air-land-sea forces in battle space.

Can you describe in more detail what DARPA’s long-term objectives for that meeting seemed to be? Presumably they hoped the meeting would spur new lines of research that would allow them to solve particular control problems in the next 5-20 years?

Anil Nerode: The director of the DARPA program Domain Specific Software Initiative, Col Eric Mettala, had called the meeting. I had no idea what was intended by that term.. I was there because I was director of the Army sponsored Mathematical Sciences Institute at Cornell and was sent by the ARO math director Jagdish Chandra. I found out the first morning that Mettala had recognized that the current control software industry in 1991 was not developing software for real time control by generals of land-sea-air battles in real time. He invited control software industry, a few control engineers from big companies (such as Wolf Kohn from Boeing), and a few academic Control Engineering professors. I believe that I was only logic-computer science person there. (I worked in design and verification of control systems in the 1950’s, but not thereafter.)

The first days discussion made it quite clear that the control software industry had not a clue how to write programs for logical based digital control of real time continuous machines, and absolutely no idea how to verify that such a program was correct. We were asked to leave position papers on what should be done for the next day. I went to my room and formulated the concept of a system of interacting continuous and discrete (logical) devices, and made it clear that to prove a program governing them works properly, you had to verify that the mixed execution sequence of digital and continuous steps always lead to satisfying the performance specification. I did not expect anyone to pick up on it.

But the next morning, after a completely confused discussion, some member of the audience said “why don’t we use Prof. Nerode’s definition of our problem.” Amazingly enough, they did. Later in the day there was a discussion in which I was very strongly supported in the conclusion that a research program, not a development program, needed to be undertaken. A lot of the audience did not see it that way, they wanted many hundreds of millions to blow to larger proportions what they were currently doing. Wolf Kohn from Boeing articulated my points much more clearly than I did. In the end Mettala put out RFP’s for a research program, I asked Wolf to send me his papers. So that was the Pacific meeting from my point of view.

Luke: Was the Pacifica meeting your inspiration for organizing the 1991 and 1992 Hybrid Systems Workshops at Cornell? And do you know whether anything came of Mettala’s RFPs?

Anil: I recognized the issue Col. Mattela raised as very significant, both for the Armed Forces and for business and industrial future systems. I did not think that Mettala was sufficiently clear on what the problem was to be able to formulate a DARPA RFP that would address the issue directly.

I had the funds available from US ARO in my Institute to sponsor new lines of research. So I organized the first hybrid systems meeting in Ithaca entirely independently of Darpa to confer with those world wide I had identified as having something to offer. These participants were from the AI and expert systems community and from the control community.

This first meeting in Ithaca was not intended to yield a volume or paper, but rather to establish that a smart bunch of people thought this is a productive research area. I explained my concept of a hybrid system, and they bought it. I chose “hybrid systems” as the name of the area. The group I chose as organizing committee for the subsequent first real hybrid systems workshop and volume was an extension of that original group.

Metalla put out a generic RFP for research in the long term military problem of control of forces and machines. I applied and got some of the funds. Others secured some of the funds under his RFP.

The principal outcome was development of hybrid systems theory simply because I continued to organize a community for several years under these monies and others. Once the point was established, there were, and are, plenty of sources of funding for the area. It takes time to develop a community. My substantial research in the area started after that seminal preparatory meeting.

Luke: In those early years, what actions did you take — or see others take — to develop the hybrid systems community? In retrospect, which actions turned out to have been the most important for the development of the field?

Anil: What my hybrid systems model revealed was that to either extract or to verify digital programs interconnected with continuous devices, expertise is required in both program verification ( a discrete logic language enterprise) and control theory (analysis based continuous mathematics).

I enlisted the best of both communities and their graduate students at the initial three hybrid systems volume meetings. This mix was the key to success. The first of the brilliant to participate actively were leading professors in control and program verification at Stanford, MIT and Berkeley. Many others followed the lead of these institutions. They have, through their PhD’s, provided many of the professors and engineers world wide for computer science and engineering departments of universities and industries. .

The compelling attraction to the computer scientists was the development of digital tools to analyze continuous devices, a new use for the technology they had developed for the digital world.

The compelling interest for the control community was that digital control of continuous devices was demanded by industry, business, and the military. Their previous technology was piecewise linear quadratic control with breakpoints for highly non-linear systems, where there was no mathematical basis assuring that the resulting systems would perform as requested. After the mathematical security of linear-quadratic control, they were skating on thin ice. This was an ad hoc process of constructing state tables followed by simulation.

In many cases now, embedded control systemshave been verified by formal (hybrid system) methods. (For instance, the Mercedes car embedded systems were first verified by a scientist with an MIT mathematical logic degree. He showed me his verification after a Florida invited lecture I gave a few years ago.)

I must add that for commercial or military systems with a life safety risk, having such verification makes it much easier to get federal certification or industrial approval.

Finally, once leading world figures had been engaged, the funding agencies followed: what else could they do?

Luke: What have been some of the major success stories of this research program? What practical problems in industry or government were solved, which could not have been solved without hybrid systems control? André Platzer outlines some applications of KeYmaera alone, here; I’m hoping you can provide some earlier examples.

Anil: Before Kohn and I introduced hybrid systems as a subject, there existed highly developed logic based technology for proving that execution sequences for digital programs always satisfy their program specification, or finding counterexamples. At the same time there were countless embedded digital control systems for continuous devices and also many attempts to make programs which would act as, for example, an assistant controlling battlefield hardware. (That was one of the purposes served by construction of ADA.)

The concept of execution sequence of a hybrid system which we introduced led to extending the program verification paradigm to mixed digital-continuous systems. This, rather than any particular theoretical development, was the main impact in science and engineering. As for program verification, this was carried out in many industries. My favorite application, created by a PhD logician from MIT, was the verification of the control systems for Mercedes limousines.

There are technical groups now for verifying such applications.

I and my partner’s primary interest was extracting digital controls for continuous systems from system description and performance specification. We have done this commercially in some practical cases, but as a whole the math background required and the magnitude of the computations needed have discouraged development of the field. It will happen in the long run because it is useful and possible.

Luke: Thanks, Anil!