ITAS: A Portable, Interactive Transportation Scheduling Tool Using a Search Engine Generated from Formal Specifications

Proceedings Of The Third Artificial Intelligence Planning Systems Conference

Volume

Proceedings Of The Third Artificial Intelligence Planning Systems Conference

Contents

In a joint project, BBN and Kestrel Institute have developed a prototype of a mixed-initiative scheduling system called ITAS (In-Theater Airlift Scheduler) for the U.S. Air Force, Pacific Command. The system was built in large part using the KIDS (Kestrel Interactive Development System) program synthesis tool. In previous work for the ARPA/Rome Laboratory Planning Initiative (ARPI), Kestrel has used their program transformation technology to derive extremely fast and accurate transportation schedulers from formal specifications, as much as several orders of magnitude faster than currently deployed systems. The development process can produce highly efficient code along with a proof of the code’s correctness. This paper describes the current prototype ITAS system and its scheduling algorithm, as a concrete example of a generated scheduling working on a real problem. We outline the generalized search algorithm in order to promote and facilitate comparison with other constraint-based scheduling systems. The overall system includes a database and interactive interface that allows users to control shape of the schedule produced in a number of ways. ITAS runs on a Macintosh PowerbookTM notebook computer, for reasons of portability.