English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In this paper, we investigate formal test-case generation for high-levelmission objectives, specifically reachability, of autonomous systems. We useKripke structures to represent the high-level decision-making of the agentunder test and the abstraction of the test environment. First, we define thenotion of a test specification, focusing on a fragment of linear temporal logicrepresented by sequence temporal logic formulas. Second, we formulate theproblem of test graph synthesis to find a test configuration for which theagent must satisfy the test specification to satisfy its mission objectives. Wean algorithm, based on network flows, for synthesizing a test graph byrestricting transitions, represented by edge deletions, on the original graphinduced by the Kripke structures. The algorithm synthesizes the test graphiteratively using an integer linear program. We prove completeness for ouralgorithm, and we show that the edge deletions in each iteration maintainfeasibility of the integer linear program in the subsequent iteration. Weformalize the notion of a minimally constrained test graph in terms of maximumflow, and prove the synthesized test graph to be minimally constrained. Wedemonstrate our algorithm on a simple graph and on gridworlds.

Synthesis of Static Test Environments for Observing Sequence-like Behaviors in Autonomous Systems