Takahashi, Satoshi (Osaka Univ.), Ushio, Toshimitsu (Osaka Univ.), Adachi, Masakazu (Graduate School of Engineering Science, Osaka Univ.)

Formal Detection of Automation Surprises in Discrete Event Systems with Linear-Time Temporal Logic Manual

Scheduled for presentation during the Mini-Symposium "Formal Methods for Discrete-Event Systems" (ThP10), Thursday, July 27, 2006, 17:00−17:25, Room 103

17th International Symposium on Mathematical Theory of Networks and Systems, July 24-28, 2006, Kyoto, Japan

This information is tentative and subject to change. Compiled on May 19, 2024

Abstract

In a human-machine system, an interface displays an abstracted state of the machine and a user supervises and controls the machine's progress through the interface. However, the abstracted state sometimes differs from that anticipated by a user due to the incompleteness of information. Such a phenomenon is called an automation surprise and may cause a serious human error.

In this paper, we assume that the user operates the machine according to a manual which is modeled by LTL (Linear-Time Temporal Logic). We propose a formal method for detection of three automation surprises and livelocks due to the manual. First, we introduce a representation of atomic propositions suitable for the detection and transform the LTL representation of the manual into a transition system. Next, we propose a composite model derived from the transition system and a machine model, which describes concurrent behavior of the machine and the user. Finally, solving a reachability problem and searching strongly-connected components for the composite model, both the automation surprises and livelocks can be detected formally.