Leveraging Classification Metrics for Quantitative System-Level Analysis with Temporal Logic Specifications
Apurva Badithela, Tichakorn Wongpiromsarn, Richard M. Murray

TL;DR
This paper presents a framework that uses classification metrics and temporal logic to quantitatively analyze system-level safety and performance in autonomous systems, integrating perception accuracy with formal specifications.
Contribution
It introduces a novel method to compute the probability of satisfaction of temporal logic specifications based on confusion matrices, linking perception performance to system-level guarantees.
Findings
Probability of safety satisfaction varies with perception accuracy.
The framework effectively models perception and control interactions.
Quantitative analysis guides system improvements and safety assurances.
Abstract
In many autonomy applications, performance of perception algorithms is important for effective planning and control. In this paper, we introduce a framework for computing the probability of satisfaction of formal system specifications given a confusion matrix, a statistical average performance measure for multi-class classification. We define the probability of satisfaction of a linear temporal logic formula given a specific initial state of the agent and true state of the environment. Then, we present an algorithm to construct a Markov chain that represents the system behavior under the composition of the perception and control components such that the probability of the temporal logic formula computed over the Markov chain is consistent with the probability that the temporal logic formula is satisfied by our system. We illustrate this approach on a simple example of a car with…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification
