English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In a human-machine system, an interface displays an abstracted state of the machine. The abstracted state may differ from that anticipated by a user. 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 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 live lock can be detected formally.

Detection of Automation Surprises for a Manual Modeled by Linear-Time Temporal Logic