We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement—in addition to collision avoidance as in the original RSS—requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issued only when necessary, which saves energy. To this end, we first quantise the state and input spaces, and then translate the controller synthesis problem to the computation of a winning strategy in a mean-payoff parity game. We illustrate the feasibility of our method on the example of a navigating nonholonomic robot.

This paper studies state-based optimal supervisors for non-terminating discrete event systems (DESs) modeled by weighted automata. An optimal supervisor controls the DES to avoid system halts and maximizes the worst-case limit-average weight of the generated infinite sequences. A state-based supervisor controls the DES depending only on its current state, and required only polynomial space of memory in the number of states and events of the DES. An s-minimally restrictive optimal (s-optimal) supervisor is a state-based optimal supervisor whose enabled set of sequences is as large as possible. We propose an algorithm to compute an s-optimal supervisor if it exists. Moreover, we consider the control costs for enabling controllable events. We derive conditions for assigning the control costs in such a way that the optimal supervisor for the DES with the control costs is also optimal for the DES without the control costs.

We consider a quantitative discrete event system modeled by a weighted automaton, where a weight assigned to each transition represents a cost by the occurrence of the transition. An optimal directed controller selects at most one controllable event at each state to optimize director's cost of the controlled discrete event system. On the other hand, linear temporal logic is often used to specify the qualitatively desired behavior of a discrete event system. In this paper, we formulate a novel optimal directed control problem where the selection of the controllable event at each state is determined so as to maximize the worst-case value of the mean payoffs of controlled behaviors subject to a given linear temporal logic control specification. We propose a design method using a two-player game automaton whose players are the director and the product automaton. The former aims to maximize the worst-case value of the generated behaviors while the latter wants to minimize it. Under this situation, we use the concept of a best response and provide an algorithm to compute an optimal director. Then, we apply the proposed algorithm to a control problem of an AGV.