Compliance is when a human positively responds to a request or a recommendation given by a system. For example, when prompted, providing your thumbprint for an automated biometric scanner at the airport or starting to watch a new TV show on a streaming service ‘we think you will love’. In trust-related research, compliance is frequently used as a behavioural measure of trust. When evaluating the compliance-trust association in experimental settings, typically, the participants agree, when asked, that they complied because they trusted the system. We developed three scenarios in instantaneous settings where compliance with an instruction delivered by a robot would typically be ascribed to trust. However, rather than asking, ‘Did you trust?’, we asked, ‘Why did you comply?’ In a thematic analysis of responses, we discovered robot design characteristics and sources not related to the design that persuade humans to comply with instructions delivered by a robot.

Abstract We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in co NExpTime and PSpace -hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.

We investigate the problem of verifying the strategic properties of multi-agent systems equipped with machine learning-based perception units. We introduce a novel model of agents comprising both a perception system implemented via feed-forward neural networks and an action selection mechanism implemented via traditional control logic. We define the verification problem for these systems against a bounded fragment of alternating-time temporal logic. We translate the verification problem on bounded traces into the feasibility problem of mixed integer linear programs and show the soundness and completeness of the translation. We show that the lower bound of the verification problem is PSPACE and the upper bound is coNEXPTIME. We present a tool implementing the compilation and evaluate the experimental results obtained on a complex scenario of multiple aircraft operating a recently proposed prototype for air-traffic collision avoidance.

We introduce agent-environment systems where the agent is stateful and executing a ReLU recurrent neural network. We define and study their verification problem by providing equivalences of recurrent and feed-forward neural networks on bounded execution traces. We give a sound and complete procedure for their verification against properties specified in a simplified version of LTL on bounded executions. We present an implementation and discuss the experimental results obtained.