Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Deontic Logic Analysis of Autonomous Systems Safety
137
0
0.0
(
0
)
Added by
Colin Shea-Blymyer
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We consider the pressing question of how to model, verify, and ensure that autonomous systems meet certain textit{obligations} (like the obligation to respect traffic laws), and refrain from impermissible behavior (like recklessly changing lanes). Temporal logics are heavily used in autonomous system design; however, as we illustrate here, temporal (alethic) logics alone are inappropriate for reasoning about obligations of autonomous systems. This paper proposes the use of Dominance Act Utilitarianism (DAU), a deontic logic of agency, to encode and reason about obligations of autonomous systems. We use DAU to analyze Intels Responsibility-Sensitive Safety (RSS) proposal as a real-world case study. We demonstrate that DAU can express well-posed RSS rules, formally derive undesirable consequences of these rules, illustrate how DAU could help design systems that have specific obligations, and how to model-check DAU obligations.
rate research
Read More
The formalization of action and obligation using logic languages is a topic of increasing relevance in the field of ethics for AI. Having an expressive syntactic and semantic framework to reason about agents decisions in moral situations allows for unequivocal representations of components of behavior that are relevant when assigning blame (or praise) of outcomes to said agents. Two very important components of behavior in this respect are belief and belief-based action. In this work we present a logic of doxastic oughts by extending epistemic deontic stit theory with beliefs. On one hand, the semantics for formulas involving belief operators is based on probability measures. On the other, the semantics for doxastic oughts relies on a notion of optimality, and the underlying choice rule is maximization of expected utility. We introduce an axiom system for the resulting logic, and we address its soundness, completeness, and decidability results. These results are significant in the line of research that intends to use proof systems of epistemic, doxastic, and deontic logics to help in the testing of ethical behavior of AI through theorem-proving and model-checking.
The motivation of our research is to establish a Laplace-domain theory that provides principles and methodology to analyze and synthesize systems with nonlinear dynamics. A semigroup of composition operators defined for nonlinear autonomous dynamical systems -- the Koopman semigroup and its associated Koopman generator -- plays a central role in this study. We introduce the resolvent of the Koopman generator, which we call the Koopman resolvent, and provide its spectral characterization for three types of nonlinear dynamics: ergodic evolution on an attractor, convergence to a stable equilibrium point, and convergence to a (quasi-)stable limit cycle. This shows that the Koopman resolvent provides the Laplace-domain representation of such nonlinear autonomous dynamics. A computational aspect of the Laplace-domain representation is also discussed with emphasis on non-stationary Koopman modes.
In this paper, we explore how, and if, free choice permission (FCP) can be accepted when we consider deontic conflicts between certain types of permissions and obligations. As is well known, FCP can license, under some minimal conditions, the derivation of an indefinite number of permissions. We discuss this and other drawbacks and present six Hilbert-style classical deontic systems admitting a guarded version of FCP. The systems that we present are not too weak from the inferential viewpoint, as far as permission is concerned, and do not commit to weakening any specific logic for obligations.
Control schemes for autonomous systems are often designed in a way that anticipates the worst case in any situation. At runtime, however, there could exist opportunities to leverage the characteristics of specific environment and operation context for more efficient control. In this work, we develop an online intermittent-control framework that combines formal verification with model-based optimization and deep reinforcement learning to opportunistically skip certain control computation and actuation to save actuation energy and computational resources without compromising system safety. Experiments on an adaptive cruise control system demonstrate that our approach can achieve significant energy and computation savings.
Given a stochastic dynamical system modelled via stochastic differential equations (SDEs), we evaluate the safety of the system through characterisations of its exit time moments. We lift the (possibly nonlinear) dynamics into the space of the occupation and exit measures to obtain a set of linear evolution equations which depend on the infinitesimal generator of the SDE. Coupled with appropriate semidefinite positive matrix constraints, this yields a moment-based approach for the computation of exit time moments of SDEs with polynomial drift and diffusion dynamics. To extend the capability of the moment approach, we propose a state augmentation method which allows us to generate the evolution equations for a broader class of nonlinear stochastic systems and apply the moment method to previously unsupported dynamics. In particular, we show a general augmentation strategy for sinusoidal dynamics which can be found in most physical systems. We employ the methodology on an Ornstein-Uhlenbeck process and stochastic spring-mass-damper model to characterise their safety via their expected exit times and show the additional exit distribution insights that are afforded through higher order moments.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
