arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 1709.02557

A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification

Lucas E. R. Fernandes·Vinicius Custodio·Gleifer V. Alves·Michael Fisher
View original source ↗Read source document ↗Export metadata ↓

Abstract

The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent.

Explore related subjects

cs.LOcs.MA

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Lucas E. R. Fernandes, Vinicius Custodio, Gleifer V. Alves, Michael Fisher. 2017-09-08. A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification. https://doi.org/10.4204/eptcs.257.5

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Differential Equations as Fixpoints and Games

Games and fixpoints are unified by proving that first-order game logic GL and the first-order modal mu-calculus L_mu are proved to be equiexpressive and equivalent, thereby fully aligning their expressive and deductive power. That is, there is a semantics-preserving translation from GL to L_mu, and vice versa. And both translations are provability-preserving, while equivalence with there-and-back-again roundtrip translations are provable in both calculi. This is to be contrasted with the propositional case, where game logic is strictly less expressive than the modal mu-calculus (without adding sabotage games). The extensions with differential equations, differential game logic (dGL) and differential modal mu-calculus, are also proved equiexpressive and equivalent. Moreover, as the continuous dynamics are definable by fixpoints or via games, ODEs can be axiomatized completely and, as a consequence, infinitesimally robust properties of ODEs can be decided via proof search. Rational gameplay provably collapses the games into single-player games to yield a strong arithmetical completeness theorem for dGL with rational-time ODEs.

cs.LO↗
arXiv2026

Self-extensional logics of formal inconsistency: Decidability and limits for paraconsistency

RmbC is a self-extensional paraconsistent logic in the family of Logics of Formal Inconsistency (LFIs). This system is obtained from mbC (the basic LFI) by adding the replacement property via two global inference rules. RmbC is characterized by a non-explosive negation $\neg$ and a consistency operator $\circ$, which recovers the principle of explosion in a controlled way. Together with its principal axiomatic extensions, RmbC admits a standard Lindenbaum-Tarski algebraization, with Boolean algebras with LFI operators (BALFIs) as its algebraic semantics. In this paper, we study how far this self-extensional paraconsistent behavior can be extended axiomatically, starting from RmbC. We classify pairs of very natural consistency axioms according to whether they preserve paraconsistency or force classical collapse; identify six minimal explosive combinations that collapse to a single algebraic core; and isolate a separate structural obstruction for the combination of excluded middle for $\neg$ with an involutive negation. We also investigate, for the first time, the decidability of this family of self-extensional LFIs. As a first result, we prove the finite model property for RmbC with respect to BALFI semantics via an algebraic filtration, which yields decidability, and transfer this result to several paraconsistent axiomatic extensions of RmbC. Finally, we establish a coNEXPTIME upper bound for the validity problem of RmbC and a coNP-hardness lower bound, and prove coNP-completeness for the principal extensions containing one of the six minimal explosive pairs.

cs.LO↗
arXiv2026

The Stochastic Target Discounted-Sum Problem

The target discounted-sum problem (TDS) asks, given a finite integer alphabet $Σ$, a rational discount factor $λ$, and a rational target $t$, whether some infinite sequence over $Σ$ has discounted sum exactly $t$. This problem remains open and underlies several open questions in automata theory, games, and Markov decision processes. We introduce and solve its stochastic counterpart, the stochastic target discounted-sum problem, which replaces existence by computation of the probability. We show that the probability that a random sequence generated by a finite Markov chain has discounted sum $t$ is rational and computable in pseudo-polynomial time. We further show how to decide, in polynomial time, whether the discounted-sum distribution of a Markov chain is atomless, and how to approximate to an arbitrary precision the probability that the discounted sum exceeds a rational threshold. Our techniques for the stochastic TDS problem allow us to make progress on TDS objectives in stochastic games, which are known to be as hard as the TDS problem. Restricting the maximizing player to finite-memory strategies, while allowing the minimizing player to use arbitrary strategies, we reduce the value problem and the synthesis problem to corresponding problems for safety objectives in stochastic games. This yields computable optimal values and deterministic optimal strategies with pseudo-polynomially bounded memory for stochastic games, and results in pseudo-polynomial-time algorithms for special cases of Markov decision processes and deterministic two-player games.

cs.LO↗