A Doxastic Characterisation of Autonomous Decisive Systems

TL;DR

This paper formalizes autonomous decisive systems using a doxastic framework, enabling verification and synthesis of belief formation to ensure decision-making aligns with mission goals in safety-critical applications.

Contribution

It introduces a formal doxastic model for autonomous systems, allowing verification of decision strategies and synthesis of belief formation mechanisms.

Findings

Can verify if an autonomous decisive system can be built for a given domain

Provides methods to synthesize belief formation processes

Supports extrapolation of beliefs for decision-making

Abstract

A highly autonomous system (HAS) has to assess the situation it is in and derive beliefs, based on which, it decides what to do next. The beliefs are not solely based on the observations the HAS has made so far, but also on general insights about the world, in which the HAS operates. These insights have either been built in the HAS during design or are provided by trusted sources during its mission. Although its beliefs may be imprecise and might bear flaws, the HAS will have to extrapolate the possible futures in order to evaluate the consequences of its actions and then take its decisions autonomously. In this paper, we formalize an autonomous decisive system as a system that always chooses actions that it currently believes are the best. We show that it can be checked whether an autonomous decisive system can be built given an application domain, the dynamically changing knowledge base and a list of LTL mission goals. We moreover can synthesize a belief formation for an autonomous decisive system. For the formal characterization, we use a doxastic framework for safety-critical HASs where the belief formation supports the HAS's extrapolation.