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

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 generated search algorithm in order to promote and facilitate comparison with other constraint-based schedu..