A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures CHENMING GE∗✉∗ , University of Michigan, USA ASTRID KEWEN PENG† , University of Utah, USA CHENYANG SHI‡ , University of Michigan, USA BEN GREENMAN, University of Utah, USA YUE JIANG, University of Utah, USA

arXiv:2609.17959v1 [cs.HC] 16 Sep 2026

For blind and low-vision (BLV) screen-reader users, a website that appears accessible in a static snapshot can become difficult or impossible to navigate once interaction begins. Yet, most automated accessibility checkers miss failures involving focus, interface state, and accessible feedback across interactions. We present A11yLTLNav, a property-based approach for automatically detecting accessibility navigation failures. Through a structured review of prior research, we organize accessibility navigation failures into a failure taxonomy and formalize a browser-observable subset as executable Linear Temporal Logic properties over action-state traces. A11yLTLNav combines random keyboard exploration with runtime property monitoring to detect these failures during interactions. We evaluate A11yLTLNav on 31 generated websites based on real-world websites and tasks. It reported 309 accessibility failures, of which 274 were confirmed, achieving 88.7% precision and identifying more confirmed failures than the comparison checkers. Our results show that A11yLTLNav transforms accessibility knowledge into reusable checks of interface behavior over time. ACM Reference Format: Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang. 2018. A11yLTLNav: Automatic Detection of Accessibility Navigation Failures. In Proceedings of Make sure to enter the correct conference title from your rights confirmation email (Conference acronym ’XX). ACM, New York, NY, USA, 41 pages. https://doi.org/XXXXXXX.XXXXXXX

1

Introduction

The web has become essential to many everyday activities, including accessing information and public services, shopping, travel, education, and employment [106]. However, accessibility barriers remain common across modern websites [70]. These barriers can limit whether people with disabilities can independently access information and complete everyday activities online, especially for blind and low-vision (BLV) users. As essential services increasingly move online, inaccessible navigation can directly restrict BLV users’ independence, participation, and access to opportunities. Prior work has shown that BLV users face difficulties not only in understanding the static content of websites, but also in navigating and interacting with dynamic websites [13, 89]. For example, users may lose track of their position ∗ Equal contribution. † Equal contribution. ‡ Equal contribution.

Authors’ Contact Information: Chenming Ge, gecm@umich.edu, University of Michigan, Ann Arbor, Michigan, USA; Astrid Kewen Peng, talentedastrid@gmail.com, University of Utah, Salt Lake City, Utah, USA; Chenyang Shi, chengysh@umich.edu, University of Michigan, Ann Arbor, Michigan, USA; Ben Greenman, benjaminlgreenman@gmail.com, University of Utah, Salt Lake City, Utah, USA; Yue Jiang, yue.jiang@utah.edu, University of Utah, Salt Lake City, Utah, USA. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. © 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM. Manuscript submitted to ACM Manuscript submitted to ACM

1

2

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

after an interface change, have difficulty reaching newly displayed content with the keyboard, or receive insufficient feedback about the result of an action. These problems can prevent users from continuing to navigate or completing a task, even when individual elements have appropriate labels or roles. Thus, an interface that appears accessible when inspected in a single state may still become inaccessible as a user navigates through it. In this work, we define accessibility navigation failures as website behaviors that make it difficult for BLV users to reach and operate interactive content, stay oriented as the interface changes, or receive the feedback needed to continue navigating. Our definition includes both accessibility violations and usability problems when they directly affect BLV users’ experience in navigating and operating a website, following prior work that treats accessibility and usability as distinct but closely related aspects of website use [2, 86]. This definition focuses on the consequences of a failure for navigation rather than only on whether an individual element violates a technical rule. For example, a dialog may open with appropriate roles and labels while keyboard focus remains on the page behind it. Detecting this failure requires considering the user’s activation, the newly opened dialog, and the resulting focus state together. Prior accessibility research has documented a broad range of accessibility failures encountered by BLV users, including problems with text alternatives, structure and semantics, keyboard and focus, composite widgets, feedback and state, dynamic content, and task navigation [13, 61, 89]. However, knowledge about these failures remains distributed across individual studies and is expressed at different levels of observation, making it difficult to apply systematically in automated testing. We therefore conducted a scoping review of the literature following PRISMA guidelines [80] to synthesize documented accessibility failures into a unified taxonomy organized by the evidence required to identify them: element-level failures can be observed from individual interface elements; interaction-level failures emerge across an action and its resulting interface state; and task-level failures depend on whether navigation supports a user’s broader goal. The taxonomy consolidates prior knowledge into a shared representation and identifies which accessibility navigation failures can be operationalized for automatic detection. Rule-based accessibility checkers efficiently detect many violations whose evidence is available in a single page state [36, 107]. Recent checkers extend automated evaluation by driving keyboard interactions [21–23, 55], replaying accessibility tests [99], analyzing screen-reader output [124], or reasoning over task execution traces [37, 125]. These approaches demonstrate the value of observing interfaces during navigation. However, to our knowledge, no existing accessibility checker translates failure mechanisms documented in prior research into explicit, reusable temporal properties. Consequently, automated checkers either remain limited to predefined static rules or infer accessibility problems from particular execution traces without a reusable specification of the expected behavior. We address this gap by formalizing the browser-observable subset of accessibility navigation failures as Linear Temporal Logic (LTL) properties over action-state traces. An action-state trace records keyboard actions on screen readers and the accessibility-relevant interface states observed before and after them. An LTL property specifies the behavior expected across this sequence, for example, that opening a dialog must be followed by keyboard focus moving inside it. This formalization allows expectations involving focus movement, widget-state changes, and accessible feedback to be evaluated explicitly across interface transitions rather than inferred anew from isolated states or complete task traces. We propose A11yLTLNav, an LTL-property-based navigation accessibility checker built on Bombadil, a propertybased Web testing framework [6]. Property-based testing evaluates interface behavior against explicit properties whenever their triggering conditions occur. A11yLTLNav performs random keyboard exploration, extracts accessibilityrelevant interface states from the websites, and evaluates executable LTL properties over the resulting action-state traces. Exploration and checking are separated: the explorer determines which keyboard actions on screen readers to execute, while temporal properties determine whether the resulting behavior violates an accessibility expectation. The Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

3

same property can therefore be checked whenever its trigger arises across different interfaces and exploration paths. This separation makes each report traceable to a triggering action, an observed outcome, and a violated expectation, while allowing the properties to be reused without defining a complete task for every website. We evaluate A11yLTLNav on 31 locally hosted website environments generated based on real-world websites and tasks, comparing it with rule-based static accessibility checkers and an agentic accessibility checker adapted from TaskAudit [125]. A11yLTLNav reported 309 unique accessibility navigation failures, of which 274 were confirmed correct, corresponding to 88.7% precision. Precision remained between 85.9% and 88.7% across three independent exploration runs, while the adapted agentic checker achieved 57.2% precision. A11yLTLNav also identified more confirmed failures than any comparison checker, required 18.52× less runtime than the agentic checker, and required no language-model inference during testing. This work makes the following contributions: • A unified failure taxonomy that synthesizes accessibility navigation failures documented in prior research and organizes them by the element-, interaction-, or task-level evidence required for detection. Beyond consolidating previously distributed knowledge, the taxonomy identifies the boundary between failures that can be checked from browser-observable behavior and those requiring additional user, task, or assistive-technology context. • A11yLTLNav, an automated accessibility checker that operationalizes browser-observable accessibility navigation failures as executable LTL properties and combines state-aware random keyboard exploration with runtime property monitoring over action-state traces. • An evaluation on 31 website environments showing that A11yLTLNav detects accessibility navigation failures with high and stable precision, identifies more confirmed failures than the comparison checkers, and operates without language-model inference.

2

Background & Motivation

2.1

Accessibility Barriers in Dynamic Web Navigation

Blind and low-vision (BLV) users continue to encounter substantial barriers when interacting with modern websites [28, 66, 105, 110]. Beyond reducing task efficiency, repeated accessibility failures accumulate into frustration, learned helplessness, and accessibility debt, reflecting a systemic mismatch between mainstream web design and non-visual interaction rather than individual ability [50, 58, 61, 83]. These consequences reflect a systemic mismatch between mainstream web design and non-visual navigation rather than a limitation of individual users. While early text-based websites were comparatively accessible, increasingly dynamic, visually structured interfaces have made accessibility failures more dependent on how users interact with a webpage over time [8, 46, 57, 61]. A large body of user studies has documented these failures, including screen-reader navigation problems, focus traps, ARIA misuse, inaccessible widgets, misleading labels, broken jump links, and poorly designed forms [24, 61, 71, 89]. Prior work further shows that BLV users may remain unaware of information or functionality that an inaccessible interface never exposes to them [12]. Importantly, many of these problems cannot be understood in isolation. The same interface issue may have little impact in one task but completely prevent task completion in another, depending on the interaction history, page state, assistive technology, and user strategy [12, 61, 71, 115]. For example, losing focus may be recoverable when the next control is easy to locate but become a blocking failure when an interface update leaves the user without an identifiable navigation position. Manuscript submitted to ACM

4

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang Consequently, user studies remain indispensable because they reveal accessibility failures as they unfold during

real interaction rather than as isolated interface defects. At the same time, these studies have also revealed rich behavioral phenomena, including navigation strategies, compensatory behaviors, and recurring failure patterns adopted by experienced BLV users [13]. However, these observations remain fragmented across individual studies and have not been consolidated into a systematic representation that can support automated reasoning. 2.2

Accessibility Navigation Failures

Prior work shows that accessibility guideline conformance does not fully reflect the accessibility problems that disabled users experience when interacting with websites. Studies with blind users have found that accessibility and usability problems only partially overlap, and that many problems encountered during real tasks are not covered by accessibility guidelines [86, 89]. Prior work also found that perceived Web accessibility is closely related to user experience, while its relationship with Web Content Accessibility Guidelines (WCAG) standards is more limited [2]. Automated evaluation should therefore consider not only whether individual elements satisfy technical requirements, but also whether users can successfully navigate the interface as it changes. Based on these findings, we define accessibility navigation failures as website behaviors that make it difficult for BLV users to reach and operate interactive content, stay oriented as the interface changes, or receive the feedback needed to continue navigating. This definition includes accessibility-conformance violations and usability problems when they directly affect BLV users’ ability to navigate and operate a website. For example, a missing label is an accessibility navigation failure because it can prevent a user from identifying a control. A correctly labeled dialog that opens without receiving keyboard focus is also an accessibility navigation failure because the user may be unable to reach its content. Accessible feedback refers to information about an action or state change that is programmatically exposed so that assistive technologies, such as screen readers, can communicate it to the user. This definition focuses on the consequences of website behavior for navigation rather than treating guideline conformance as the only boundary of accessibility. It also establishes the scope of our failure taxonomy: a problem is included when prior research shows that it can interfere with reaching content, operating controls, maintaining orientation, or receiving the information needed to proceed. 2.3

Automated Detection and Repair

Although user studies are essential for understanding BLV users’ experiences, they are resource-intensive and cannot continuously evaluate every page, interaction path, and website update. Automated tools can complement these studies by repeatedly evaluating interfaces at development time and after deployment [31]. Static analyzers such as axe [30], WAVE [111], and Lighthouse [42] are highly effective at identifying element-level issues, including missing labels, malformed ARIA attributes, and other WCAG violations [21, 70]. However, these tools primarily reason over static interface properties, and therefore cannot detect runtime failures that emerge only during interaction [13, 66, 71, 89, 110]. To move beyond static analysis, recent work has explored dynamic accessibility evaluation through scripted interactions, test replay, and interface exploration [21, 36, 124]. These approaches can expose some interaction- and task-level accessibility navigation failures by observing how an interface responds to user actions. However, scripted approaches generally depend on predefined interaction sequences and checking procedures, limiting their ability to reuse an accessibility expectation whenever the relevant behavior occurs along a different path. More recently, large language models (LLMs) and Computer Use Agents (CUAs) have been introduced to support accessibility evaluation and repair by executing multistep interface actions and reasoning about task outcomes [44, 67, Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

5

105, 124]. A CUA is an agent that observes and operates a graphical interface through actions such as keyboard input, pointer input, or accessibility-service commands. These agents offer greater flexibility than fixed scripts because they can adapt their actions to the current interface and task. However, recent studies show that they remain susceptible to hallucination, execution errors, and inconsistent accessibility judgments [58, 85, 101]. These limitations highlight the need for explicit and inspectable specifications of expected interface behavior rather than reliance on model inference alone [53]. A11yLTLNav addresses a complementary need: it uses random keyboard exploration to discover interface behaviors and formal temporal properties to determine whether those behaviors satisfy accessibility expectations. This separation preserves the flexibility to encounter failures along different navigation paths while grounding each judgment in an explicit property. Such properties may also provide reliable validation criteria for future repair systems, although the present work focuses on detection. 2.4

Formal Model for Failure Analysis

Formal models provide a principled way to specify how actions, interface states, and expected outcomes relate over time. For example, Stary introduced a user-based modeling method for human-computer interaction [98]. By expressing expected sequences of actions, feedback, and state transitions, this decomposition and connection makes it possible to simplify the interaction and scale it into automated analysis [21, 43, 49, 96, 100]. It is particularly useful when interactions depends not on a single state, but on how states relate to one another across time [3, 21, 37, 76, 109]. Accessibility failures in interaction-to-task level are inherently temporal. For instance, missing feedback after an action, unexpected focus changes, and unsuccessful recovery from an error are not isolated interface defects. These failures emerge only as interaction sequences unfold. Although prior BLV accessibility research has documented these failures through user studies, barrier-based evaluations, and qualitative reports [21, 89, 124], the resulting accessibility knowledge has not been systematically represented as reusable properties for runtime checking. We address this gap by synthesizing documented accessibility navigation failures into a unified failure taxonomy and translating the browser-observable subset into Linear Temporal Logic (LTL) properties. LTL is a formal language for specifying how conditions should hold across an ordered sequence of states. It can express, for example, that a condition must always hold, must eventually become true, or must become true after a particular event [62, 87]. In A11yLTLNav, these properties are evaluated over action-state traces: ordered records of keyboard actions and the accessibility-relevant interface states observed before and after them. Each property defines a triggering condition and an expected outcome. For example, when a keyboard action opens a modal dialog, the resulting state should place keyboard focus inside that dialog. A violation of this expectation provides concrete evidence of an accessibility navigation failure. This representation makes expected and prohibited interface behaviors explicit, executable, and reusable across websites. Temporal logic therefore bridges accessibility knowledge documented in prior research and scalable automated evaluation, enabling A11yLTLNav to check not only what an interface contains, but also how it behaves as users navigate. 3

Failure Taxonomy

To support systematic analysis and formal reasoning, we synthesize accessibility navigation failures documented in prior research into a unified failure taxonomy. Following the user-centered definition of accessibility [86], we include both accessibility violations and usability problems when they make it difficult for BLV users to reach or operate interactive content, stay oriented as an interface changes, or receive the feedback needed to continue navigating. Manuscript submitted to ACM

6

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 1. Comparison of three levels of BLV web accessibility evaluation. Our work derives task-level ecological validity from empirical evidence while preserving the scalability of formal checking. Taxonomy Level

Failure Target

Detection Methods

Scalability

Ecological Validity

L1: Element-level

Elements, Labels, ARIA

Rule-based Detection e.g., axe [30], WAVE [111], Lighthouse [42]

Automatic (no human required)

Low (static properties only)

L2: Interaction-level

Interaction Steps

Simulated interaction: barrier walkthrough [16], expert usability evaluations [71]

Semi-automatic (requires expert setup)

Partial (expert-simulated, naturalistic)

not

L3: Task-level

Real-world tasks

Real-user observation: user studies [9, 52, 64, 84], thinkaloud [13]

Manual (requires real users)

High (naturalistic tasks & context)

Ours L2 + L3

Interactive failure patterns from real-world tasks

Formalized Detection

Automatic (temporal checking)

High (derived from real-world observations)

3.1

Observations

property

Scoping Review Method

Our work focuses on bridging the gap between scalability and ecological validity for accessibility navigation failures that extend beyond isolated interface elements. Instead of relying only on isolated conformance violations [21], we synthesize interaction- and task-level accessibility navigation failures into a unified taxonomy that serves as the foundation for formal, automated reasoning. We constructed the taxonomy through a structured multi-source literature review following PRISMA [80, 81]. We search four databases (ACM Digital Library, IEEE, Springer and Science Direct) for research articles using complementary queries over abstract fields: population (e.g., "blind" "low vision") × context (e.g., "web") × outcome (e.g., "failure""usability") query in July, 2026. Specifically, ACM Digital Library yields 196 papers (190 via abstract searching+ 6 via title); IEEE Xplore yields 138 papers; Springer yields 383 papers(originally 33,967 papers, narrowing to Article, and HCI subjects "Interaction design", "Web accessibility evaluation and user experience", "User interfaces and human computer interaction", Subdisciplines of "User interfaces and human computer interaction" and Language of "English"); ScienceDirect 238 papers. To assess the recall of the primary query, 6 additional papers were retained from two supplementary searches in August, 2026: Q1 applied broader term combinations (n = 115) and Q2 targeted keyboard- and interaction-level failure terminology (n = 16), deduplication excluded. Detailed queries attached in the Appendix. 145 papers were removed due to deplication and wrong content type (e.g., magazines, proposals,etc.). Of the 936 candidate papers, 460 were excluded in the screening stage for "Irrelevant Topics" (SC1), "Not Full Paper"(SC2), and "Non-English"(SC3). SC1 involves mobile apps and softwares, independent games and blind studies. 476 met our inclusion criteria of reporting empirically observed interaction failures encountered by BLV or keyboard-only users on web platforms. Failures extracted from the final 56 studies were iteratively coded, consolidated, and refined into 13 taxonomy categories organized by the stage of interaction in which they occur. In addition to database searches, we conducted one round of backward snowballing on all papers retained after full-text screening, examining their reference lists for relevant works not captured by keyword search. This yielded 4 additional candidates. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures 3.2

7

Levels of Accessibility Failure

Based on the review, we found that existing accessibility research has progressively expanded from evaluating isolated interface elements to understanding user interaction and real-world task performance. We organize prior work into three complementary levels of accessibility evaluation: conformance-level (L1), interaction-level (L2), and task-level (L3). Table 1 summarizes the targets, common detection methods, scalability, and ecological validity associated with these three levels and situates our approach in relation to them. L1: Element-level evaluation asks whether individual interface elements satisfy accessibility rules and can be flagged by rule-based tools and checklists [16, 102]. This includes WCAG success criteria [16, 25, 90], whose A/AA/AAA levels indicate the classification of a given criterion, national or regional guidelines, and other specific rules derived from experts [38, 124]. Such approaches are automatic and effective at identifying node-level issues, including missing labels, malformed ARIA attributes, and insufficient contrast. However, they primarily reason over static interface properties and cannot determine whether these issues ultimately prevent successful navigation [8]. L2: Interaction-level evaluation shifts the focus from interface elements to interaction steps, asking whether users can successfully navigate and operate an interface. Representative approaches include barrier walkthroughs, expert usability evaluations, and interaction-based accessibility testing [8, 16, 71]. Rather than checking isolated violations, these simulation methods reveal failures such as navigation confusion, missing feedback, focus loss, and interaction dead ends that emerge during interaction. Recent systems such as BAGEL further extend automated evaluation from isolated interface elements to interaction flow by assessing keyboard navigability and interaction sequences [21]. Nevertheless, these approaches still evaluate whether individual interaction steps remain executable under predefined evaluation procedures rather than whether users ultimately accomplish real-world tasks in their natural contexts [8, 17]. L3: Task-level evaluation asks whether a sequence of interactions ultimately supports successful completion of users’ real-world goals. Real-user observation studies demonstrate that the same interaction issue may be recoverable in one task but prevent task completion in another, depending on the user’s strategy, interaction history, assistive technology, and task context [13, 52, 97, 100]. Such studies offer high ecological validity, revealing recurring navigation strategies, compensatory behaviors, and context-dependent failure patterns that cannot be explained by isolated interaction steps alone [8, 9, 64, 84]. However, these findings remain largely qualitative and fragmented across individual studies, making them difficult to scale for automated reasoning. Table 2 and Table 3 present the resulting failure taxonomy for L2 and L3 (The full failure taxonomy for L1, L2, and L3 is in the Appendix), including each accessibility navigation failure, an illustrative example, and the prior studies documenting it. By organizing accessibility navigation failures according to their required evidence, the taxonomy identifies which failures can be evaluated from browser-observable interface behavior and therefore provides the basis for their subsequent formalization as temporal properties. 4

A11yLTLNav: A Failure-driven Checker for Navigation Accessibility Failures

To automatically detect accessibility navigation failures in websites, we built A11yLTLNav, an accessibility checker that automatically detects these failures. Figure 1 shows the overall pipeline of our checker. 4.1

Temporal Property-Based Testing for Accessibility Navigation Failures

We model an interaction as a trace of user actions and the interface states that change following these actions. Many accessibility navigation failures are not identifiable from a single interface state. For example, a failure occurs when Manuscript submitted to ACM

8

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 2. Taxonomy of Level 2 BLV web accessibility failures, organized by the level of evidence required to observe them. Citations after each failure give the reporting studies. Category

Failure

Example

L2: Interaction-level Keyboard and focus

Loss of focus after activation [32, 44, 47, 48, 52, 82] No exit from a composite widget [44] Improperly hidden elements remain focusable [44, 113, 114]

Composite widgets

No valid active option in expanded combobox [44, 113] No active-option movement on arrow keys [44, 114] No commit state after option selection [44, 113] No valid active cell in a managed grid [44] No active-cell movement on arrow keys [44] No effect from a role-specific activation key [44, 83]

Feedback and state

No feedback confirming an activation [14, 19, 52, 63, 89, 93, 113] Misplaced or disconnected response to an activation [13, 14, 44, 47, 95, 104, 113, 114] ARIA state contradicts the native state [44] No exposed expanded state after a reveal [8, 44] No trace of operation progress or mode [52, 65, 113]

Dynamic content

Structure & semantics AT interoperability

No accessible name or named dismissal control on a dialog [13, 26, 44, 45, 63, 112] No focus move into a newly opened dialog [13, 44, 113] No dialog dismissal or focus return on Escape [44] No reachable control to start playing or stop playing media [73, 83, 103] Inadequate labels to reveal nearby context [8, 14, 19, 64, 113, 114] Inconsistent name exposure across reading modes [19, 88] Screen-reader shortcut captured outside page [44, 68]

Manuscript submitted to ACM

after confirming a departure airport, focus returns to the top of the page and the date fields must be found again Tab is intercepted inside a video description panel and never advances to the next control Tab stops on items in a collapsed carousel and the screen reader announces an empty string the suggestion list is open but no option is marked as current, so nothing is announced while arrowing pressing Down inside an open suggestion list does not advance to the next entry Enter on a highlighted airport leaves the field showing a partial string, and the user believes the choice was taken a date picker opens with no cell marked as current, so arrow keys have no starting point Tab passes over the whole calendar, and the arrow keys that would move within it are never announced a calendar cell is selected only by Space; pressing Enter repeatedly produces nothing after submitting a form nothing is announced, and the user rereads the page to find out whether it was accepted a filter updates a results panel further down the page with nothing tying the two together; correcting a typo re-opens the suggestion list on every keystroke a checkbox reported as aria-checked="false" while the native control is checked an accordion panel opens visually but the trigger continues to report itself as collapsed an upload gives no sign of whether it is running or has stalled; the same key both inspects and edits a block, with nothing saying which just happened a consent banner is announced only as dialog, with no way to tell what it is or how to close it a cookie notice appears over the page while focus stays behind it, so the user keeps reading content that is now blocked Escape does not close the overlay; when it finally closes, focus is left at the top rather than on the control that opened it a video begins on load and its pause control is neither reachable by Tab nor announced a price is read out with no indication of which product row or which column it belongs to a password field is announced by name while browsing, but only as edit box once the user starts typing the context-menu command opens the browser’s own menu instead of the page’s; an injected accessibility widget claims keys the user’s screen reader needs

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

9

Table 3. Taxonomy of Level 3 BLV web accessibility failures. L3: Task-level Feedback and state

No guidance for recovering from a rejected action [14, 52, 93]

Text alternatives

Inadequate description of goal-relevant information [4, 10, 13, 35, 38, 41, 48, 54, 56, 59, 60, 63, 64, 66, 83, 89, 93, 104, 114, 115, 118, 120]

Structure & semantics

Reading order and grouping inconsistent with task’s logic [1, 35, 39, 60, 63, 82, 88, 89, 93, 112, 117, 120] Excessive heading marks relative to page content [39, 120] Tab order inconsistent with task’s order [8, 32] Position learned from prior visits no longer predicts where the control is [52, 113] No efficient route to the control the task requires [13, 27, 33, 38, 44, 88, 89, 93, 113] No confirmation of completeness, driving reverification [12–14, 39, 48, 59] No way to resume from a prior position [14, 91, 92]

Navigation efficiency

Websites

1. Action Selector

Valid Actions

a submission is refused with no indication of which field was wrong or what format it expected; a category must exist before an expense can be added, and nothing says so a binary tree described as running prose, leaving parent and child relations unrecoverable; a chart summarised in one sentence when the task requires comparing series; a link named read more among twenty others a product’s price is read far from its name; the store-locator sits under Account rather than under Stores every list item carries a heading, so the heading list is as long as the page the submit button is reached before the fields it depends on the submit button sits in the top bar on one page and after the last field on the next reaching a store-selection setting takes several hundred Tab presses through the footer a forum thread is re-read from the top because nothing confirms that no later reply revised the answer returning from a product page drops the user at the top of the results list rather than at the item they left

2. A11y State Extractor

A11y tree

Feedback

DOM state

Focus

Execute

3. Runtime Monitor

LTL Properties: G(openModal(d)→X(focusInside(d))) G(escapeClosesModal(𝑑, 𝑣)) → X(focus = 𝑣) …

Random Select

Failure Logs Restart from new state

Fig. 1. Overview of our temporal property testing workflow. From each webpage state, the action selector chooses a valid keyboard action. The accessibility state extractor captures the resulting interface state including a11y tree, DOM and ARIA state, focus and accessible feedback, which is checked against executable temporal properties by the runtime monitor. Violations are recorded as failure logs, while exploration continues from the new state.

activating a button opens a modal but keyboard focus remains in the background page, which cannot be detected through static analysis of the elements. Therefore, detecting such failures requires modeling the relationship between an interaction event and the interface states that follow it. We use Linear Temporal Logic (LTL) to represent these interaction expectations over execution traces. LTL provides temporal operators for conditions that should always hold (G), hold after an interaction (X), or eventually become true (F). Appendix A presents a brief formal semantics of LTL. These operators allow us to express an accessibility navigation failure as an interaction trigger followed by an expected state transition. We use LTL to formalize generic, interaction level properties that determine whether an observed interface transition is accessible for BLV users. None of our LTL formulas require knowledge of the user’s website-specific task goal. Manuscript submitted to ACM

10

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

4.2

Property-Based Checker for Accessibility Navigation Failures

Existing accessibility checkers typically evaluate a page state at the moment the checker is invoked [30, 111, 124]. In contrast, navigation failures may occur only in the process of state transactions. Traditional browser automation frameworks such as Playwright [72] provide the frameworks needed to perform keyboard actions and inspect browser state, but are primarily based on example-based tests where the test author specifies the assertions and elements that should be evaluated. Such tests work well for known workflows, but do not easily generalize the same interaction check to controls and state changes that have not been identified in advance, since would require specifying the interaction paths where each accessibility failure may occur. We therefore build A11yLTLNav on Bombadil [6], a property-based testing framework that provides state-aware random exploration and temporal property checking for building our checker. For exploration, Bombadil repeatedly captures the current browser state, constructs the actions that are available in that state, and randomly selects an action to execute. Because the available actions are generated from the current interface state, this exploration can check interaction sequences that are not specified in advance. The same accessibility property can therefore be checked across different interface states whenever its triggering condition arises. For checking, Bombadil allows developers to define correctness properties over the sequence of browser states produced during exploration. Its property-based language directly supports temporal operators, allowing the LTL properties derived from our failure taxonomy to be implemented as executable scripts. Bombadil thus provides both the random exploration mechanism used to expose candidate interaction failures and the temporal checking infrastructure used to detect violations. However, Bombadil is still a general-purpose UI testing framework rather than an accessibility checker. Its default interaction space and browser observations are not designed around keyboard navigation, focus management, or accessibility-relevant interface state. We therefore extend Bombadil with three components: an action selector, an accessibility state extractor, and a property monitor. 4.2.1 Action Selector. Bombadil randomly select actions from sighted users, like click and scroll, to explore the websites. BLV users instead use keyboard-only and screen reader actions. Therefore, we replace Bombadil’s default action space with a state-aware keyboard action generator tailored to BLV users’ navigation methods. At each browser state, the generator determines the valid action set based on the currently focused element and widget context: • Sequential navigation (Tab, Shift+Tab1 ) is universally enabled. • Activation actions (Enter, Space) are exposed for interactive controls. • Directional navigation (arrow keys) is enabled in composite widgets like comboboxes, grids, tabs, and menus. • Espace actions (Escape) are enabled in dialogs or layered overlays. During exploration, Bombadil selects actions from this action space. Exploration and property checking are decoupled: the explorer decides where and how to navigate, while runtime monitors independently verify whether the observed trace violates an accessibility property. The exploration continues even after detecting a defect, allowing a single session to discover multiple distinct violation witnesses within its time budget. 4.2.2 Accessibility State Extractor. Bombadil provides the browser exploration and temporal-property execution infrastructure, but its browser state does not directly expose the accessibility-relevant information required by our properties. We therefore extend Bombadil with an accessibility state layer that derives four types of observations from each browser state: accessibility semantics, DOM and ARIA state, focus, and interaction feedback. Accessibility semantics 1 Since Bombadil do not support Shift+Tab, we modified the action generator to support this action.

Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures Website After Action

Website Before Action

…

11

…

Enterr

Focus: Add to List

Focus: Add to List (not changed)

LTL formula: G(openNewModal(d)→X(focusInside(d)))

Results: Failure (Focus outside the modal) Actual focus

Expected focus

Fig. 2. Example of a focus-management failure. Activating “Add to List” opens a dialog, but focus remains on the trigger.

capture information relevant to the accessibility tree, such as element roles and accessible names derived from native marks and ARIA attributes. DOM and ARIA state captures interaction-relevant properties such as whether dialogs or controlled regions are open or visible, and values including aria-expanded, aria-checked, and related state attributes. Focus observations record the currently focused element and changes in focus across interactions. Finally, feedback observations capture changes that can communicate the result of an action, including updates to live regions, status messages, and alerts. 4.2.3 Runtime Property Monitor. During exploration, A11yLTLNav continuously evaluates the written LTL properties against the browser states produced by the action selector. The monitor creates a property-specific transaction when a trusted keyboard action satisfies the property’s triggering condition. The transaction binds the triggering action to the relevant interface object and records the pre-action observations required by that property. At the subsequent settled browser state, the monitor collects the corresponding post-action evidence and determines whether the property is applicable, whether sufficient evidence is available to evaluate it, and whether the observed transition violates the expected behavior. An observation is reported as a violation only when the property is applicable. 4.3

From Empirical Failures to Executable Temporal Properties

4.3.1

From Failure Taxonomy to Temporal Properties. Our failure taxonomy captures accessibility navigation failures

observed across prior BLV studies. We turn these empirical observations into temporal properties by identifying three components for each failure taxonomy: the interaction that triggers the relevant behavior, the interface outcome expected after that interaction, and the observations needed to determine whether the expectation holds. This process converts qualitative descriptions of accessibility failures into reusable temporal properties that can be checked automatically across different websites and interaction paths. For failure taxonomy items that span multiple cases, we formulate several temporal properties. For example, as shown in Figure 2, our taxonomy includes cases in which opening a modal does not move keyboard focus into the new interaction context. This failure corresponds to a violation of the following LTL property, where 𝑑
denotes the newly opened modal dialog: G openModal(𝑑) → X focusInside(𝑑) The property states that whenever an interaction opens a new modal, keyboard focus should enter that same modal in the next relevant post-action state. Manuscript submitted to ACM

12

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang Before opening

Dialog opened

Enter

Focus: Log in

Before Escape

Tab × 2

Focus: Email field

After Escape

Escape

Focus: Sign in

Focus: Document

LTL Property: G(escapeClosesModal(d, v) → X(focus = v))

Result: Failure (focus resets to the document) Actual focus

Expected focus

Fig. 3. Example of a focus-return failure after dialog closes. Activating Log in opens the dialog and establishes the button as its invoker. Escape closes the dialog, but focus resets to the document instead of returning to the invoker.

This formulation captures the temporal relationship between the triggering interaction and its expected accessibility outcome, rather than checking either interface state in isolation. Figure 3 illustrates another property when a modal closes. Pressing Enter on Log in opens a dialog and moves focus into the email field. Two Tab actions then move focus to Sign in. Pressing Escape closes the dialog, but focus resets to the document instead of returning to Log in. We express the expected focus return as follows: G escapeClosesModal(𝑑, 𝑣) →
X(focus = 𝑣) . Here, 𝑑 denotes the modal and 𝑣 denotes its invoker, the button used to open it. The triggering condition captures an Escape action that closes the modal while its invoker remains eligible to receive focus. The property requires focus to return to that same button in the next relevant post-action state. Checking this expectation requires retaining information across the interaction sequence: the checker records the invoker when the modal opens and compares it with the observed focus after the modal closes. In this example, Log in remains available, but the resulting focus is on the document, violating the property. The expected destination therefore depends on how the user entered the dialog, not just on the page state after dismissal. The same failure category may produce multiple temporal properties when different interaction mechanisms expose distinct observable behaviors. In this way, the taxonomy provides the empirical foundation, while the temporal properties provide precise and reusable guidelines for automated checking. The complete failure-to-property mapping is provided in Appendix E. 4.3.2

From Temporal Properties to Executable Scripts. Afterwards, we convert each temporal property into a runtime

script to monitor over the interaction trace. Each script identifies the triggering interaction, binds it to the relevant state extracted by previous steps, records the required observations before the action, and evaluates the expected behavior after the interface settles with the action. This formulation allows the property to capture a common accessibility expectation without prescribing a single implementation mechanism. Different interfaces may communicate the same successful action through different accessible signals, while the monitor checks whether the resulting transition remains perceivable through accessibility-relevant browser state. For example, in Figure 3, the script records Log in as the invoker when Enter opens the dialog. Moving focus to the email field and then Sign in does not change this association. After Escape, the script observes that the dialog has closed and Log in remains eligible, but focus is on the document. These observations establish the violation of the property. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures 5

13

Evaluation

We evaluate A11yLTLNav’s performance by comparing to several state-of-the-art accessibility checkers: axe, WAVE and taskAudit [30, 111, 125]. We study the following research questions: RQ1: How does A11yLTLNav compare with existing accessibility checkers in precision, and how stable is its precision across exploration runs? RQ2: How quickly does A11yLTLNav check the accessibility failures comparaed to other accessibility checkers? RQ3: How do A11yLTLNav and other accessibility checkers differ in the failures they detect and diagnose? We evaluate the tools on 31 websites. For static checkers, we ran them on the first page of each website and excluded failures that are not targeted for BLV users. For the agentic checker, we ran the pipeline using DeepSeek V4 Flash 0731 [116]. For A11yLTLNav, we run three trials of 30-minutes each, because the exploration process is random. We ran all experiments on Rocky Linux 8.10, allocating one Intel Xeon Gold 6530 CPU core and 4GB of memory to each run. 5.1

Baselines

Rule-based static accessibility scanner. Axe [30] and WAVE [111] are representative rule-based accessibility checkers commonly used for automated web accessibility evaluation. These tools inspect the webpage and identify violations of static accessibility rules. Task-driven agentic checker. We implement a task-driven agentic accessibility checker following TaskAudit [125], the closest prior approach to our setting since it targets accessibility failures through the process of task execution. For each generated website, a web agent powered by browser-use [75] attempts each task using screen reader transcript as observations and keyboard and screen reader actions for navigation. The interaction traces are then analyzed for accessibility failures using an LLM. Our prompts to the agentic checker are shown in Appendix G. 5.2

Website Generation

It is challenging to evaluate live websites using automatic tools because the websites are designed for humans, and often block tools [7, 52, 94, 99]. Also, since website behavior changes over time, live websites are a poor setting for reproducible experiments. Following prior work that reconstructs real websites as executable synthetic environments [20, 40, 123, 126], we evaluate our checker on locally hosted generated websites. We generated a subset of cloned websites from Mind2Web [29]. Following CowCorpus’s method for website selection [51], for each of Mind2Web’s 31 subdomains, we selected the website with the highest U.S. traffic according to Similarweb, resulting in 31 websites. We synthesized these environments using Claude Code [5] with GPT-5.6 Sol [77], adapting the website generation pipeline from uxCUA [40]. The prompt for website generation is attached in Appendix F. 5.3

Metrics

We evaluate each checker by the precision of its reported accessibility failures and its efficiency in terms of execution time and cost. Firstly, we deduplicated the detected failures. Two reported accessibility failures were grouped when they belonged to the same component of the same website and were reported by the same checker. Then, we followed the definition of the accessibility failures discussed before when annotating these reported failures. Two of the authors manually reviewed all reported failures across checkers against the corresponding interaction traces and the error definitions in our failure taxonomy. Each report of accessibility errors by these checkers was annotated for whether it represented a correct detection or a false positive, and afterwards we resolved different opinions through discussion. Manuscript submitted to ACM

14

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 4. Precision of static checkers, the agentic checker, and A11yLTLNav on deduplicated reports. The shaded row denotes our method; boldface indicates the best result for each evaluation metric. Checker

6

Reports

Correct

False Positives

Precision

Axe WAVE Agentic checker

18 68 276

17 34 158

1 34 118

94.4% 50.0% 57.2%

A11yLTLNav (ours)

309

274

35

88.7%

Results

Table 4 summarizes the precision of reported accessibility failures from all four checkers. Because axe and WAVE primarily evaluate page-level failures and find fewer failures then others, our analysis for the result focus on the task-driven agentic checker and A11yLTLNav, both of which observe accessibility failures during runtime interactions. 6.1

RQ1: Precision and Stability

6.1.1 Agentic Checker. The task-driven agentic checker reported 276 failures across 31 websites, of which 158 were confirmed correct and 118 were false positives, with a precision of 57.2% (95% CI: 52.0–62.5%). Its main advantage is that it has access to both task context and screen-reader output, which allows it to reason about failures whose significance depends on what the user is trying to accomplish. However, its reports of accessibility failures also depend on correctly executing and interpreting the task trace. Among 516 task runs by the web agent executor, 306 (59.3%) reached the maximum step limit and 367 (71.1%) contained at least one recorded action error. Our review further found false positives where the analyzer relied on an assumed website state from the screen reader output rather than the actual focus and action outcome from the websites, or inferred missing information from a single screen-reader output even though later output provided it. Moreover, the agents’ thoughts and traces are different from that of BLV users in the process of task execution, resulting in different subgoals and trajectories in the process of task execution [44]. Thus, task context provides useful semantic evidence, but also introduces uncertainty from both agent execution and LLM-based trace interpretation. 6.1.2 A11yLTLNav. A11yLTLNav reported 309 accessibility failures, of which 274 were confirmed correct and 35 were false positives, corresponding to a precision of 88.7% (95% CI: 82.2–93.8%). This was 31.4% higher than the agentic checker (95% CI: 23.2–39.3%). The false positives were primarily associated with the boundary of particular properties, such as imperfect conditions or accessibility failure properties not represented by the current state extractor. We examine representative correct and incorrect detections in the case analysis below. Stability. Because A11yLTLNav’s exploration is random, we additionally check precision across the three independent runs. Precision remained between 85.9% and 88.7% across runs, shown in Table 5, suggesting that although different exploration runs expose different interactions, the reported violations remain consistently precise. The overall row represents reports consolidated accessibility errors across runs. 6.2

RQ2: Runtime and Computational Cost

The task-driven agentic checker required substantially more computation than A11yLTLNav. Across the 31 websites, TaskAudit required 288.20 hours in total. This corresponds to an average runtime of 557.81 minutes per website (SD = 247.86 minutes). In comparison, A11yLTLNav completed exploration and property checking for Run 1 in 15.56 hours, Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

15

Table 5. Review of A11yLTLNav reports for accessibility errors across three exploration runs. Run

Total

Correct

False Positive

Precision

Run 1 Run 2 Run 3

309 313 299

274 269 257

35 44 42

88.7% 85.9% 86.0%

Pass@3

493

424

69

86.0%

Table 6. Runtime comparison across 31 websites. The shaded row denotes our method; boldface indicates the lower runtime. Checker

Total Runtime (h)

Mean / Website (min)

Agentic checker

288.20

557.81

A11yLTLNav (ours)

15.56

30.12

Table 7. Token usage and estimated cost across 31 websites. A11yLTLNav uses zero tokens. Checker

Statistic

Agentic checker

Total Per-site mean

Prompt Input (M tokens)

Output (M tokens)

Total (M tokens)

Cost (USD)

945.38 30.50

60.30 1.95

1005.69 32.44

63.11 2.04

averaging 30.12 minutes per website (SD = 0.01 minutes). Overall, the agentic checker required approximately 18.52× as much runtime as A11yLTLNav. The agentic checker also incurred substantial language-model usage. Across task execution and accessibility analysis, Agentic checker consumed approximately 1.01 billion tokens, including 945.38 million prompt tokens and 60.30 million output tokens, corresponding to $63.11 in API cost. For each website, Agentic checker consumed an average of 30.50 M input tokens (SD = 12.03 M) and 1.95 M output tokens (SD = 0.81 M), for an average of 32.44 million tokens in total (SD = 12.74 M). At the August 2026 DeepSeek V4 Flash pricing, the resulting average API cost was $2.04 per website (SD = $0.80). In contrast, A11yLTLNav does not invoke an LLM during exploration or property evaluation and therefore does not have any token cost. 6.3

RQ3: Comparative Analysis of Detected Failures

To further examine RQ3, Figure 4 groups the reports from the two runtime checkers by failure domain in our taxonomy. We use the evidence provided in the reports of accessibility errors to aggregate domains across taxonomy levels because the same interaction concern can arise with different levels of evidence. The two approaches produced substantially different failure reports in the figure. The agentic checker was dominated by reports involving composite widgets, which accounted for 160 of its 276 reports, followed by keyboard and focus (43), keyboard (22), and feedback and state (21). In contrast, A11yLTLNav’s reports were concentrated in feedback and state (112), keyboard and focus (103), and dynamic content (51). It additionally reported 37 structure and semantics failures. These distributions reflect the different evidence and checking boundaries of the two approaches. A11yLTLNav’s largest domains correspond to generalizable failures that can often be expressed as consistent relationships between a keyboard action and a browser-observable outcome, such as whether focus remains valid, an interface state is exposed consistently, or accessible feedback follows an activation. Composite-widget behavior is more different across Manuscript submitted to ACM

16

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Count of accessibility errors

Agentic Checker

Correct

A11yLTLNav

False Positive

160

160

50

120

112

103 11

24

80

0 2

43

37

40 15 13

5

9 8

1

37

4

22 18

92

51

110

88

34

0

Text Structure Keyboard alternatives and semantics

4

1

9

Keyboard and focus

Composite widgets

21

51

17

1

4 1

Feedback and state

Dynamic content

AT Navigation interoperability efficiency

5

0

0

0

Fig. 4. Accessibility error reports grouped by failure domain from the failure taxonomy. (b) Keyboard and Focus Before

(a) Feedback and State Before

After

Space

After

(c) Dynamic Content Before

Enter

Error: No accessible feedback for the change Error: Focus reset to the body LTL Property L2-11 LTL Property L2-01 G(effectfulActivation(c) → X notifiableFeedback(c)) G(localInvalidation(c) → X exposedFocus) Actual focus

Expected focus region

After

Space

Error: Focus in background when modal opened LTL Property L2-19 G(openNewModal(d) → X(focusInside(d))) Changed state / content

Fig. 5. Examples of accessibility navigation errors captured by A11yLTLNav and their corresponding temporal properties. Each example shows the interface state before and after a keyboard action, together with the property that specifies the expected accessible state transition: (a) missing accessible feedback after an effectful activation, (b) focus loss after a local interface update, and (c) focus remaining outside a newly opened modal. Colored outlines indicate observed focus, expected focus regions, and changed interface state or content.

widgets, websites and tasks: different widgets support different interaction models, states, and keyboard conventions, making them less easy to be captured by a small reusable property set. The agentic checker can instead interpret these interactions from task and screen-reader context without requiring a predefined property for each observable mechanism. These results therefore suggest different detection profiles by either approach; the following cases illustrate the mechanisms behind these differences. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

17

(a) State Change Misunderstand

(b) Task Progress Mismatch

(c) Incomplete Exploration

Before

Before

Before

Screen reader: “All sizes combo box. XS. S. M. L. XL…”

After

Screen reader: “Mobile ticket · 4 available.”

Screen reader: “Jeep.” · “6 of 6.”

ArrowDown

ArrowDown

Tab After

After

Screen reader: “Great deal.” Screen reader: “XS”

Screen reader: “Jeep combo box collapsed”

A11y analyzer

A11y analyzer

A11y analyzer

The Size button is broken since the button stays in XS

Focus do not move when Tab

Incomplete accessible name (without price).

Agentic Checker false-positive target

Actual focus

Counterevidence

Fig. 6. Representative false positives from the agentic checker: (a) misunderstanding an interface state change, (b) misinterpreting task progress as a keyboard-focus failure, and (c) making a judgment from incomplete screen-reader exploration. Orange boxes indicate the evidence targeted by the analyzer’s report; green dashed boxes highlight counterevidence identified during manual review.

6.3.1 A11yLTLNav. The three A11yLTLNav examples in Figure 5 illustrate how temporal properties connect a keyboard action to an expected interface state. In each case, the interface visibly responds, but the resulting state does not satisfy the accessibility expectation. For feedback and state, pressing Space on a setting of the loan updates the form values and monthly estimate. However, the update produces none of the accessible confirmation signals monitored by A11yLTLNav. Script of the LTL property L2-11 checks that an accessible activation is followed by notifiable feedback. The report therefore distinguishes a successful update from the missing confirmation accompanying it. For keyboard and focus, pressing Enter on a button to decrease quantity changes the quantity from two to one. However, keyboard focus then resets to the body of the page, leaving no control focused. Script of the LTL property L2-01 checks that focus remains exposed after a local change invalidates the focused control. The failure concerns losing focus during a small update within the same view. For dynamic content, pressing Space on Add to List opens a dialog, but keyboard focus remains on the background button behind it. Property L2-19 checks that opening a new modal is followed by focus inside it. The dialog’s appearance alone does not establish that keyboard users can interact with the newly displayed content. Together, these examples illustrate why A11yLTLNav can detect a broad set of interaction-level accessibility failures while maintaining high precision. By summarizing each judgment in an temporal property between a triggering action and its expected accessibility outcome, A11yLTLNav can systematically detect failures across many interactions while reducing errors from ambiguous or incomplete interpretation of execution traces. Manuscript submitted to ACM

18

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

6.3.2 Agentic Checker. Figure 6 illustrates three representative false-positive cases from the agentic checker and highlights how errors can arise when the accessibility analyzer interprets traces of task executor. Across these examples, the analyzer either misinterprets intermediate keyboard state changes, treats incomplete screen-reader observations as evidence of missing information, or reaches a judgment that is inconsistent with the progress already made during exploration.

Misunderstanding interface state changes. The accessibility analyzer can infer the wrong interface state from screenreader output. In the size-selector example, the selected value before the action is “All sizes,” while the screen reader also announces available options including “XS,” “S,” and “M.” After ArrowDown, the selected value changes to “XS.” The analyzer treats “XS” from the earlier screen-reader output as the pre-action value and therefore concludes that the selection did not change. The false positive results from misunderstanding which part of the screen-reader output represents the current interface state.

Mismatching task progress with focus movement. The analyzer can also interpret task progress differently from the executor. In the vehicle-search example, the Make combobox is expanded with “Jeep” selected before Tab. After Tab, the selection is retained and the combobox collapses, which the screen reader announces as “Jeep combo box collapsed.” The analyzer nevertheless reports that focus did not move when Tab was pressed. Here, it treats the absence of immediate focus relocation as a failure without accounting for the interaction progress made by closing the expanded combobox and completing the current selection.

Judging from incomplete exploration. The analyzer may make an accessibility judgment before the executor has explored enough of the interface. In the ticket-listing example, the screen reader first announces “Mobile ticket, 4 available” and then, after ArrowDown, “Great deal.” The analyzer concludes from this partial observation that the accessible name is incomplete because it does not include the price. However, the ticket also exposes the price and fee information as the user continues through the listing. The false positive therefore arises from treating information not yet encountered during sequential screen-reader exploration as information that is absent from the interface. Together, these cases show that the agentic checker’s false positives often arise from uncertainty in interpreting execution traces. Misidentified interface states, mismatched interpretations of interaction progress, and incomplete screen-reader exploration can cause successful interactions or available information to be judged as accessibility failures.

7

Discussion

Our results demonstrate that using temporal property checkers in websites is effective for automatically detecting navigation errors, with A11yLTLNav achieving 88.7% precision across websites. The key insight behind A11yLTLNav is to evaluate accessibility not only from individual interface states, but also from how those states change in response to user interactions. By combining random exploration with temporal properties derived from empirical accessibility failures, A11yLTLNav can systematically check interaction expectations involving focus, keyboard interaction, widget state, and user feedback as they arise during exploration. In this section, we discuss how temporal property testing complements existing accessibility evaluation methods, how empirical accessibility findings can inform executable accessibility checks, and the limitations and opportunities for extending this approach. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures 7.1

19

Complementing Existing Accessibility Checkers

Our results suggest that temporal property testing complements existing approaches to automate accessibility checking. Rule-based checkers efficiently identify many violations that can be determined from a single interface state, but automated checking covers only a subset of accessibility failures [36, 107]. In contrast, many failures targeted by A11yLTLNav arise from how an interface changes after an interaction, consistent with prior work on automatically detecting keyboard and dialog related navigation failures [21, 22]. For example, opening a dialog requires relating its appearance to the resulting focus state, while activating a control may require determining whether an accessibilityrelevant change or feedback follows. Temporal properties make these action–state relationships explicit and allow interaction expectations to be checked directly. Our comparison with the agentic checker further highlights complementary forms of accessibility evidence. A11yLTLNav is well suited to failures whose expected state transitions can be specified explicitly, whereas agentic checkers can incorporate screen-reader output and task context to reason about outcomes that depend on broader semantic interpretation [124, 125]. These approaches therefore occupy different roles in accessibility checking process: rule-based tools check local conformance, temporal properties check interaction transitions, and agentic checker can reason about richer task-specific and user-perceived outcomes. Combining these forms of evidence may enable automated evaluation to cover a broader range of accessibility failures than any single approach alone.

7.2

Limitations and Future Work

Observable evidence and assistive-technology feedback. A11yLTLNav currently focuses on accessibility failures whose expected behavior can be grounded in browser-observable interaction states. This scope allows us to check failures involving focus, keyboard operation, widget state, and accessibility-relevant feedback, but it does not cover all failures in our taxonomy. Some failures require evidence outside the current state model, such as actual screen-reader output, assistive-technology behavior, semantic relationships between interface regions, or interaction state that persists across views. For example, A11yLTLNav can determine whether an interaction produces a feedback signal that can be exposed to screen reader, but it does not verify what a screen reader actually announces. Future work could extend the state extractor with screen-reader and other assistive-technology observations, richer semantic relationships between interface elements, and persistent interaction state. These additional observations could allow more empirically observed accessibility failures in our taxonomy to be expressed as executable temporal properties.

Task-dependent accessibility properties. The current temporal properties are largely reusable and task-independent. This makes the same property applicable across websites, but limits A11yLTLNav’s ability to check failures whose expected behavior depends on the user’s goal, such as whether a description provides task-relevant information, whether controls occur in an appropriate task order, or whether a navigation path is sufficiently efficient. Agentic accessibility checkers can incorporate richer task and screen-reader context when reasoning about such outcomes [124, 125], suggesting a complementary direction for temporal checking. Future systems could provide parameterized temporalproperty templates whose task-specific predicates are instantiated during agent execution. An agent could identify the task-relevant target, expected outcome, or relationship between interface regions, while the temporal property provides an explicit condition for checking the resulting interaction. This could combine the semantic flexibility of task-driven agents with the explicit and reusable checking boundaries of temporal properties. Manuscript submitted to ACM

20

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang Coverage under stochastic exploration. Because A11yLTLNav relies on stochastic exploration, an implemented property

can be evaluated only when the explorer reaches an interaction that triggers it. Consequently, failing to report a violation within a fixed exploration budget does not establish that the violation is absent, and different exploration runs may exercise different portions of the interface. Our evaluation therefore reports the precision and stability of reported findings rather than exhaustive coverage of all failures on a website. Future work could make exploration property-aware by prioritizing states and action sequences that exercise properties that have not yet been triggered. Such guidance could be particularly useful for properties that require multiple related interactions, such as opening a dialog, navigating within it, and dismissing it to evaluate focus return. Property-guided exploration could therefore improve the coverage of executable properties within a fixed testing budget. From detection to repair. This work focuses on detecting accessibility failures and does not evaluate whether detected violations can be repaired safely. This distinction is increasingly relevant as GenAI-based authoring tools like coding agents introduce new accessibility workflows for BLV and keyboard-only users [78], while recent LLM-based accessibility repair systems show that generated fixes require explicit validation to preserve interface behavior and avoid regressions [74, 79, 108]. Prior accessibility checkers have also demonstrated the value of integrating concrete accessibility improvements into developer workflows and supporting collaboration around proposed changes [11]. Building on these directions, A11yLTLNav could serve as a continuous feedback mechanism alongside a generative UI system or coding agent: after a violation is detected, the system could return its triggering action, observed states, and expected transition, and then re-check a proposed revision before it is accepted. This would form a loop, generationexecution-checking-repair, in which generated fixes are validated against explicit behavioral expectations rather than accepted solely from model-generated reasoning. Such workflows should also ensure that the authoring and feedback interfaces themselves remain accessible to BLV and keyboard-only users [78]. 8

Conclusion

In this work, we introduced a failure-driven, property-based approach to automatically detecting accessibility navigation errors experienced by blind and low-vision users using screen readers when navigating the websites. We first organized empirically observed Web accessibility failures into a taxonomy and translated the browser-observable subset into executable temporal properties. Building on these properties, A11yLTLNav combines state-aware keyboard exploration with runtime property monitoring to detect accessibility failures that emerge across interaction transitions. Across 31 website environments, A11yLTLNav achieved 88.7% precision and remained stable across three independent exploration runs, while automating the checking process of some kinds of failures that complementary to both rule-based and agentic accessibility checkers. These results demonstrate that accessibility navigation failures involving focus, interface state, and accessible feedback can be expressed as reusable temporal properties. More broadly, our work provides a path for translating empirical knowledge from BLV accessibility research into executable properties, complementing existing accessibility evaluation methods and providing a foundation for future property-guided testing and generation– checking–repair workflows. Acknowledgments References [1] Amaia Aizpurua, Myriam Arrue, and Markel Vigo. 2015. Prejudices, memories, expectations and confidence influence experienced accessibility on the Web. Computers in Human Behavior 51 (2015), 152–160. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

21

[2] Amaia Aizpurua, Simon Harper, and Markel Vigo. 2016. Exploring the relationship between web accessibility and user experience. International Journal of Human-Computer Studies 91 (2016), 13–23. [3] Najd Al-Mouh and Hend S Al-Khalifa. 2016. Enhancing web accessibility by implementing context aware proxy. International Journal of Web Information Systems 12, 2 (2016), 201–214. [4] Md Zubair Ibne Alam, Shehnaz Islam, and Enamul Hoque. 2023. Seechart: Enabling accessible visualizations through interactive natural language interface for people with visual impairments. In Proceedings of the 28th International Conference on Intelligent User Interfaces. 46–64. [5] Anthropic. 2026. Claude Code: Overview (Documentation). https://code.claude.com/docs. Accessed: 2026-08-16. [6] Antithesis. 2026. Bombadil: Property-based testing for web and terminal UIs. https://github.com/antithesishq/bombadil [7] Sagnik Anupam, Davis Brown, Shuo Li, Eric Wong, Hamed Hassani, and Osbert Bastani. 2025. BrowserArena: Evaluating LLM agents on real-world web navigation tasks. arXiv preprint arXiv:2510.02418 (2025). [8] Chieko Asakawa. 2005. What’s the web like if you can’t see it?. In Proceedings of the 2005 International Cross-Disciplinary Workshop on Web Accessibility (W4A). 1–8. [9] Jeffrey P Bigham, Anna C Cavender, Jeremy T Brudvik, Jacob O Wobbrock, and Richard E Ladner. 2007. WebinSitu: a comparative analysis of blind and sighted browsing behavior. In Proceedings of the 9th International ACM SIGACCESS Conference on Computers and Accessibility. 51–58. [10] Jeffrey P Bigham, Ryan S Kaminsky, Richard E Ladner, Oscar M Danielsson, and Gordon L Hempton. 2006. WebInSight: making web images accessible. In Proceedings of the 8th International ACM SIGACCESS Conference on Computers and Accessibility. 181–188. [11] Jeffrey P. Bigham and Richard E. Ladner. 2007. Accessmonkey: a collaborative scripting framework for web users and developers. In Proceedings of the 2007 International Cross-Disciplinary Conference on Web Accessibility (W4A 2007), Banff, Canada, May 7-8, 2007 (ACM International Conference Proceeding Series, Vol. 225), Simon Harper and Yeliz Yesilada (Eds.). ACM, 25–34. doi:10.1145/1243441.1243452 [12] Jeffrey P Bigham, Irene Lin, and Saiph Savage. 2017. The Effects of" Not Knowing What You Don’t Know" on Web Accessibility for Blind Web Users. In Proceedings of the 19th international ACM SIGACCESS conference on computers and accessibility. 101–109. [13] Yevgen Borodin, Jeffrey P Bigham, Glenn Dausch, and IV Ramakrishnan. 2010. More than meets the eye: a survey of screen-reader browsing strategies. In Proceedings of the 2010 international cross disciplinary conference on web accessibility (W4A). 1–10. [14] Yevgen Borodin, Jeffrey P Bigham, Rohit Raman, and IV Ramakrishnan. 2008. What’s new? Making web page updates accessible. In Proceedings of the 10th international ACM SIGACCESS conference on Computers and accessibility. 145–152. [15] Erin L Brady, Yu Zhong, Meredith Ringel Morris, and Jeffrey P Bigham. 2013. Investigating the appropriateness of social network question asking as a resource for blind users. In Proceedings of the 2013 conference on Computer supported cooperative work. 1225–1236. [16] Giorgio Brajnik. 2008. A comparative test of web accessibility evaluation methods. In Proceedings of the 10th international ACM SIGACCESS conference on Computers and accessibility. 113–120. [17] Giorgio Brajnik, Yeliz Yesilada, and Simon Harper. 2009. Guideline aggregation: web accessibility evaluation for older users. In Proceedings of the 2009 International Cross-Disciplinary Conference on Web Accessibililty (W4A). 127–135. [18] Jeremy T Brudvik, Jeffrey P Bigham, Anna C Cavender, and Richard E Ladner. 2008. Hunting for headings: sighted labeling vs. automatic classification of headings. In Proceedings of the 10th international ACM SIGACCESS conference on Computers and accessibility. 201–208. [19] Maria Claudia Buzzi, Marina Buzzi, Barbara Leporini, and Fahim Akhter. 2010. Is Facebook really" open" to all?. In 2010 IEEE International symposium on technology and society. IEEE, 327–336. [20] Hyungjoo Chae, Jungsoo Park, and Alan Ritter. 2026. Safe and scalable web agent learning via recreated websites. arXiv preprint arXiv:2603.10505 (2026). [21] Paul T Chiou, Ali S Alotaibi, and William GJ Halfond. 2023. Bagel: An approach to automatically detect navigation-based web accessibility barriers for keyboard users. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems. 1–17. [22] Paul T Chiou, Ali S Alotaibi, and William GJ Halfond. 2023. Detecting dialog-related keyboard navigation failures in web applications. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 1368–1380. [23] Paul T. Chiou, Ali S. Alotaibi, and William G. J. Halfond. 2021. Detecting and localizing keyboard accessibility failures in web applications. In ESEC/FSE ’21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021, Diomidis Spinellis, Georgios Gousios, Marsha Chechik, and Massimiliano Di Penta (Eds.). ACM, 855–867. doi:10.1145/3468264.3468581 [24] Alex H Cohen, Jorge E Fresneda, and Rolph E Anderson. 2023. How inaccessible retail websites affect blind and low vision consumers: their perceptions and responses. Journal of Service Theory and Practice 33, 3 (2023), 329–351. [25] Daniel Costa, Luís Carriço, and Carlos Duarte. 2015. The differences in accessibility of tv and desktop web applications from the perspective of automated evaluation. Procedia Computer Science 67 (2015), 388–396. [26] Balázs Csontos and István Heckl. 2021. Accessibility, usability, and security evaluation of Hungarian government websites. Universal Access in the Information Society 20, 1 (2021), 139–156. [27] Luiz Felipe da Paixão Silva, Antônio Armando de O. Barbosa, Evelise Roman Corbalan Góis Freire, Paula Christina Figueira Cardoso, Rafael Serapilha Durelli, and André Pimenta Freire. 2018. Content-based navigation within mathematical formulae on the web for blind users and its impact on expected user effort. In Proceedings of the 8th International Conference on Software Development and Technologies for Enhancing Accessibility and Fighting Info-exclusion. 23–32. [28] Vagner Figueredo De Santana and Rogério Abreu De Paula. 2013. Web accessibility snapshot: an effort to reveal coding guidelines conformance. In Proceedings of the 10th International Cross-Disciplinary Conference on Web Accessibility. 1–4. Manuscript submitted to ACM

22

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

[29] Xiang Deng, Yu Gu, Boyuan Zheng, Shijie Chen, Sam Stevens, Boshi Wang, Huan Sun, and Yu Su. 2023. Mind2web: Towards a generalist agent for the web. Advances in Neural Information Processing Systems 36 (2023), 28091–28114. [30] Deque Systems. 2021. axe DevTools – The Accessibility Testing Toolkit for Developers. https://www.deque.com/axe/devtools/. Accessed: 2026-07-17. [31] Iyad Abu Doush, Khalid Sultan, Mohammed Azmi Al-Betar, Zainab AlMeraj, Zaid Abdi Alkareem Alyasseri, and Mohammed A. Awadallah. 2023. Web accessibility automatic evaluation tools: to what extent can they be automated? CCF Trans. Pervasive Comput. Interact. 5, 3 (2023), 288–320. doi:10.1007/S42486-023-00127-8 [32] Mohammed Fakrudeen. 2025. Evaluation of the accessibility and usability of university websites: a comparative study of the Gulf region. Universal Access in the Information Society 24, 2 (2025), 1883–1898. [33] Javedul Ferdous, Hae-Na Lee, Sampath Jayarathna, and Vikas Ashok. 2023. Enabling efficient web data-record interaction for people with visual impairments via proxy interfaces. ACM Transactions on Interactive Intelligent Systems 13, 3 (2023), 1–27. [34] Nádia Fernandes, Daniel Costa, Sergio Neves, Carlos Duarte, and Luís Carriço. 2012. Evaluating the accessibility of rich internet applications. In Proceedings of the International Cross-Disciplinary Conference on Web Accessibility. 1–4. [35] Simone Bacellar Leal Ferreira, Ricardo Rodrigues Nunes, and Denis Silva da Silveira. 2012. Aligning usability requirements with the accessibility guidelines focusing on the visually-impaired. Procedia Computer Science 14 (2012), 263–273. [36] Thomas Fischer, Björn Lundell, and Jonas Gamalielsson. 2025. Coverage of web accessibility guidelines provided by automated checking tools. Universal Access in the Information Society 24, 4 (2025), 3615–3637. [37] Nasr Eddine Fliti, Leisan Kokorina, Florian Tambon, and Michael Papadakis. 2026. Flow-A11y: Flow-Aware Accessibility Testing. arXiv preprint arXiv:2607.03100 (2026). [38] Kentarou Fukuda, Shin Saito, Hironobu Takagi, and Chieko Asakawa. 2005. Proposing new metrics to evaluate web usability for the blind. In CHI’05 extended abstracts on Human factors in computing systems. 1387–1390. [39] Prathik Gadde and Davide Bolchini. 2014. From screen reading to aural glancing: towards instant access to key page sections. In Proceedings of the 16th international ACM SIGACCESS conference on Computers & accessibility. 67–74. [40] Alice Gao, Weixi Tong, Rishab Vempati, Katharina Reinecke, R Benjamin Shapiro, Tianyi Zhang, and Jason Wu. 2026. Training Computer Use Agents to Assess the Usability of Graphical User Interfaces. arXiv preprint arXiv:2604.26020 (2026). [41] Cole Gleason, Amy Pavel, Emma McCamey, Christina Low, Patrick Carrington, Kris M Kitani, and Jeffrey P Bigham. 2020. Twitter A11y: A browser extension to make Twitter images accessible. In Proceedings of the 2020 chi conference on human factors in computing systems. 1–12. [42] Google. [n. d.]. Lighthouse. https://developer.chrome.com/docs/lighthouse. Accessed: 2026-07-17. [43] Filipe Del Nero Grillo and Renata Pontin de Mattos Fortes. 2014. Accessible modeling on the web: a case study. Procedia Computer Science 27 (2014), 460–470. [44] Ananya Gubbi Mohanbabu, Rosiana Natalie, Brandon Kim, Anhong Guo, and Amy Pavel. 2026. A11y-CUA Dataset: Characterizing the Accessibility Gap in Computer Use Agents. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–26. [45] Suhit Gupta and Gail Kaiser. 2005. Extracting content from accessible web pages. In Proceedings of the 2005 International Cross-Disciplinary Workshop on Web Accessibility (W4A). 26–30. [46] Simon Harper, Sean Bechhofer, and Darren Lunn. 2006. Taming the inaccessible web. In Proceedings of the 24th annual ACM international conference on Design of communication. 64–69. [47] Simon Harper, Carole Goble, and Robert Stevens. 2000. A pilot study to examine the mobility problems of visually impaired users travelling the web. ACM SIGCAPH Computers and the Physically Handicapped 68 (2000), 10–19. [48] Simon Harper, Carole A. Goble, Robert Stevens, and Yeliz Yesilada. 2004. Middleware to expand context and preview in hypertext. In Proceedings of the ACM SIGACCESS Conference on Computers and Accessibility, ASSETS 2004, Atlanta, GA, USA, October 18-20, 2004, Julie A. Jacko and Andrew Sears (Eds.). ACM, 63–70. doi:10.1145/1028630.1028643 [49] Simon Harper and Yeliz Yesilada. 2007. Web authoring for accessibility (WAfA). Journal of Web Semantics 5, 3 (2007), 175–179. [50] Joy E Harris. 2011. Towards a theory of learned technological helplessness. In Encyclopedia of information communication technologies and adult education integration. IGI Global Scientific Publishing, 83–101. [51] Faria Huq, Zora Zhiruo Wang, Zhanqiu Guo, Venu Arvind Arangarajan, Tianyue Ou, Frank Xu, Shuyan Zhou, Graham Neubig, and Jeffrey P Bigham. 2026. Modeling Distinct Human Interaction in Web Agents. arXiv preprint arXiv:2602.17588 (2026). [52] Syed Fatiul Huq, Ziyao He, Yirui He, and Sam Malek. 2026. Bridging the Gap between Automated Intervention and Actual User Experience: A Mixed-Methods Study on Mobile Accessibility Issues for Screen Reader Users. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–27. [53] Syed Fatiul Huq, Mahan Tafreshipour, Kate Kalcevich, and Sam Malek. 2025. Automated generation of accessibility test reports from recorded user transcripts. (2025). [54] Muhammad Asiful Islam, Yevgen Borodin, and IV Ramakrishnan. 2010. Mixture model based label association techniques for web accessibility. In Proceedings of the 23nd annual ACM symposium on User interface software and technology. 67–76. [55] Shubhi Jain, Syed Fatiul Huq, Ziyao He, and Sam Malek. 2025. Automated Detection of Web Application Navigation Barriers for Screen Reader Users. In 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 1906–1918. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

23

[56] Hyeonhak Jeong, Minki Chun, Hyunmin Lee, Seung Young Oh, and Hyunggu Jung. 2023. Wataa: Web alternative text authoring assistant for improving web content accessibility. In Companion proceedings of the 28th international conference on intelligent user interfaces. 41–45. [57] Arthur I Karshmer and Karlis Kaugars. 1995. Equal access to information for all: making the world of electronic information more accessible to the handicapped in our society. ACM SIGCAPH Computers and the Physically Handicapped 52-53 (1995), 11–23. [58] Omar Khan and JooYoung Seo. 2026. " I Don’t Trust Any Professional Research Tool": A Re-Imagination of Knowledge Production Workflows by, with, and for Blind and Low-Vision Researchers. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–24. [59] Satwik Ram Kodandaram, Jiawei Zhou, Xiaojun Bi, IV Ramakrishnan, and Vikas Ashok. 2026. Finding the Signal in the Noise: An Exploratory Study on Assessing the Effectiveness of AI and Accessibility Forums for Blind Users’ Support Needs. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–20. [60] Krzysztof Krejtz, Ann Marcus-Quinn, Carlos Duarte, Iga Stasiak, Letícia Seixas Pereira, and Izabela Krejtz. 2025. Higher education accessibility information in practice. A report on the accessibility of European Universities. Universal Access in the Information Society 24, 3 (2025), 2673–2685. [61] Jonathan Lazar, Aaron Allen, Jason Kleinman, and Chris Malarkey. 2007. What frustrates screen reader users on the web: A study of 100 blind users. International Journal of human-computer interaction 22, 3 (2007), 247–269. [62] Christine P Lee, David Porfirio, Xinyu Jessica Wang, Kevin Chenkai Zhao, and Bilge Mutlu. 2025. Veriplan: Integrating formal verification and llms into end-user planning. In Proceedings of the 2025 CHI Conference on Human Factors in Computing Systems. 1–19. [63] Barbara Leporini. 2011. Google news: how user-friendly is it for the blind?. In Proceedings of the 29th ACM international conference on Design of communication. 241–248. [64] Stefan Leuthold, Javier A Bargas-Avila, and Klaus Opwis. 2008. Beyond web content accessibility guidelines: Design of enhanced text user interfaces for blind internet users. International Journal of Human-Computer Studies 66, 4 (2008), 257–270. [65] Jiasheng Li, Zining Zhang, Zeyu Yan, Matthew Wong, Arnav Mittal, Ge Gao, and Huaishu Peng. 2026. As Content and Layout Co-Evolve: TangibleSite for Scaffolding Blind People’s Webpage Design through Multimodal Interaction. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–16. [66] Eleanor T Loiacono, Nicholas C Romano Jr, and Scott McCoy. 2009. The state of corporate website accessibility. Commun. ACM 52, 9 (2009), 128–132. [67] Juan-Miguel López-Gil and Juanan Pereira. 2025. Turning manual web accessibility success criteria into automatic: an LLM-based approach. Universal Access in the Information Society 24, 1 (2025), 837–852. [68] Tlamelo Makati, Garreth W Tigwell, and Kristen Shinohara. 2024. The promise and pitfalls of web accessibility overlays for blind and low vision users. In Proceedings of the 26th International ACM SIGACCESS Conference on Computers and Accessibility. 1–12. [69] João Marcelo Dos Santos Marques and Simone Bacellar Leal Ferreira. 2023. Description of dynamic images: a systematic mapping for the understanding and transparency of information that may be perceptible visually impaired citizens. In Proceedings of the XIX Brazilian Symposium on Information Systems. 229–236. [70] Beatriz Martins and Carlos Duarte. 2024. A large-scale web accessibility analysis considering technology adoption. Universal Access in the Information Society 23, 4 (2024), 1857–1872. [71] Mei Miao, Hoai Anh Pham, Jens Friebe, and Gerhard Weber. 2016. Contrasting usability evaluation methods with blind users. Universal access in the Information Society 15, 1 (2016), 63–76. [72] Microsoft. 2026. Playwright is a framework for Web Testing and Automation. It allows testing Chromium, Firefox and WebKit with a single API. https://github.com/microsoft/playwright [73] Hisashi Miyashita, Daisuke Sato, Hironobu Takagi, and Chieko Asakawa. 2007. Making multimedia content accessible for screen reader users. In Proceedings of the 2007 international cross-disciplinary conference on Web accessibility (W4A). 126–127. [74] Peya Mowar, Yi-Hao Peng, Jason Wu, Aaron Steinfeld, and Jeffrey P Bigham. 2025. Codea11y: Making ai coding assistants useful for accessible web development. In Proceedings of the 2025 CHI Conference on Human Factors in Computing Systems. 1–15. [75] Magnus Müller and Gregor Žunič. 2024. Browser Use: Enable AI to control your browser. https://github.com/browser-use/browser-use [76] Liam O’Connor and Oskar Wickström. 2022. Quickstrom: property-based acceptance testing with LTL specifications. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1025–1038. [77] OpenAI. 2026. GPT-5.6: Frontier intelligence that scales with your ambition. https://openai.com/index/gpt-5-6/. [78] Sushil K Oswal and Hitender K Oswal. 2024. Examining the accessibility of generative AI website builder tools for blind and low vision users: 21 best practices for designers and developers. In 2024 IEEE International Professional Communication Conference (ProComm). IEEE, 121–128. [79] Oluwatoyosi Oyelayo, Ghada Abushaqra, Parham Asadi, Durjoy Dey, and Diego Elias Costa. 2026. LLM Based Web Accessibility Repair: An Empirical Study of Detection, Remediation, and Cost. CoRR abs/2605.27716 (2026). arXiv:2605.27716 doi:10.48550/ARXIV.2605.27716 [80] Matthew J Page, Joanne E McKenzie, Patrick M Bossuyt, Isabelle Boutron, Tammy C Hoffmann, Cynthia D Mulrow, Larissa Shamseer, Jennifer M Tetzlaff, Elie A Akl, Sue E Brennan, et al. 2021. The PRISMA 2020 statement: an updated guideline for reporting systematic reviews. bmj 372 (2021). [81] Matthew J Page, David Moher, Patrick M Bossuyt, Isabelle Boutron, Tammy C Hoffmann, Cynthia D Mulrow, Larissa Shamseer, Jennifer M Tetzlaff, Elie A Akl, Sue E Brennan, et al. 2021. PRISMA 2020 explanation and elaboration: updated guidance and exemplars for reporting systematic reviews. bmj 372 (2021). [82] Kamonwan Pakdeechote and Pichaya Tandayya. 2012. A new web interface for the visually impaired to access facebook. In Proceedings of the 6th International Conference on Rehabilitation Engineering & Assistive Technology. 1–4. Manuscript submitted to ACM

24

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

[83] Afra Pascual, Mireia Ribera, Toni Granollers, and Jordi L Coiduras. 2014. Impact of accessibility barriers on the mood of blind, low-vision and sighted users. Procedia Computer Science 27 (2014), 431–440. [84] Letícia Seixas Pereira, Simone Bacellar Leal Ferreira, and Dominique Archambault. 2015. Preliminary web accessibility evaluation method through the identification of critical items with the participation of visually impaired users. Procedia Computer Science 67 (2015), 77–86. [85] Minoli Perera, Swamy Ananthanarayan, Cagatay Goncu, and Kim Marriott. 2026. I’m Always a Little Skeptical of It: Verification Practices of Blind Users When Working with Generative AI in Spreadsheets. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–21. [86] Helen Petrie and Omar Kheir. 2007. The relationship between accessibility and usability of websites. In Proceedings of the SIGCHI conference on Human factors in computing systems. 397–406. [87] David Porfirio, Allison Sauppé, Aws Albarghouthi, and Bilge Mutlu. 2018. Authoring and verifying human-robot interactions. In Proceedings of the 31st annual acm symposium on user interface software and technology. 75–86. [88] Venkatesh Potluri, Tadashi E Grindeland, Jon E Froehlich, and Jennifer Mankoff. 2021. Examining visual semantic understanding in blind and low-vision technology users. In Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems. 1–14. [89] Christopher Power, André Freire, Helen Petrie, and David Swallow. 2012. Guidelines are only half of the story: accessibility problems encountered by blind users on the web. In Proceedings of the SIGCHI conference on human factors in computing systems. 433–442. [90] Yash Prakash, Akshay Kolgar Nayak, Nithiya Venkatraman, Sampath Jayarathna, Hae-Na Lee, and Vikas Ashok. 2026. Micro-Behavioral Analysis of Online Shopping Patterns for Blind Users. In Proceedings of the 2026 Conference on Human Information Interaction and Retrieval. 295–305. [91] Yash Prakash, Mohan Sunkara, Hae-Na Lee, Sampath Jayarathna, and Vikas Ashok. 2023. AutoDesc: facilitating convenient perusal of web data items for blind users. In Proceedings of the 28th International Conference on Intelligent User Interfaces. 32–45. [92] Romisa Rohani Ghahari, Mexhid Ferati, Tao Yang, and Davide Bolchini. 2012. Back navigation shortcuts for screen reader users. In Proceedings of the 14th international ACM SIGACCESS conference on Computers and accessibility. 1–8. [93] Bektur Ryskeldiev, Kotaro Hara, Mariko Kobayashi, and Koki Kusano. 2022. Investigating accessibility challenges and opportunities for users with low vision disabilities in customer-to-customer (C2C) marketplaces. In Proceedings of the 24th International ACM SIGACCESS Conference on Computers and Accessibility. 1–4. [94] Navid Salehnamadi, Ziyao He, and Sam Malek. 2023. Assistive-technology aided manual accessibility testing in mobile apps, powered by record-and-replay. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems. 1–20. [95] Frode Eika Sandnes. 2024. “Consent notices are obstructing my view”: viewing sticky elements on responsive websites under the magnifying glass. Displays 81 (2024), 102579. [96] Kumari Sarita, Parminder Kaur, and Satinder Kaur. 2025. Fujma: a fuzzy-based user judgement model for accessibility. Universal Access in the Information Society 24, 3 (2025), 2819–2844. [97] Sidas Saulynas, Lawrence Burgee, Apoorva Bendigeri, and Ravi Kuber. 2022. Putting situational impairments in context: developing guidance for situational impairments and severely constraining situational impairments by examining parallel domains. Universal Access in the Information Society 21, 4 (2022), 941–966. [98] Christian Stary. 2001. User diversity and design representation: Towards increased effectiveness in Design for All. Universal Access in the Information Society 1, 1 (2001), 16–30. [99] Maryam Taeb, Amanda Swearngin, Eldon Schoop, Ruijia Cheng, Yue Jiang, and Jeffrey Nichols. 2024. Axnav: Replaying accessibility tests from natural language. In Proceedings of the 2024 CHI Conference on Human Factors in Computing Systems. 1–16. [100] Hironobu Takagi, Shin Saito, Kentarou Fukuda, and Chieko Asakawa. 2007. Analysis of navigability of Web applications for improving blind usability. ACM Transactions on Computer-Human Interaction (TOCHI) 14, 3 (2007), 13–es. [101] Yilin Tang, Yuyang Fang, Tianle Wang, Lingyun Sun, and Liuqing Chen. 2025. " This is My Fault", Really? Understanding Blind and Low-Vision People’s Perception of Hallucination in Large Vision Language Models. In Proceedings of the 38th Annual ACM Symposium on User Interface Software and Technology. 1–20. [102] Christian Thomsen and Torben Bach Pedersen. 2006. Building a web warehouse for accessibility data. In Proceedings of the 9th ACM international workshop on Data warehousing and OLAP. 43–50. [103] Shannon M Tomlinson. 2016. Perceptions of accessibility and usability by blind or visually impaired persons: a pilot study. Proceedings of the Association for Information Science and Technology 53, 1 (2016), 1–4. [104] Utku Uckun, Ali Selman Aydin, Vikas Ashok, and IV Ramakrishnan. 2020. Breaking the accessibility barrier in non-visual interaction with pdf forms. Proceedings of the ACM on Human-computer Interaction 4, EICS (2020), 1–16. [105] Guillermo Vera-Amaro and José Rafael Rojano-Cáceres. 2025. Accessible Web Content Generation Using LLMs: An Empirical Study on Prompting Strategies and Template-Guided Remediation. IEEE Latin America Transactions 23, 12 (2025), 1230–1239. [106] María Rosalía Vicente and Ana Jesús López. 2010. A multidimensional analysis of the disability digital divide: Some evidence for internet use. The information society 26, 1 (2010), 48–64. [107] Markel Vigo, Justin Brown, and Vivienne Conway. 2013. Benchmarking web accessibility evaluation tools: measuring the harm of sole reliance on automated tests. In Proceedings of the 10th international cross-disciplinary conference on web accessibility. 1–10. [108] Lily Bundgaard Wanscher, Markus Heidemann Lorensen, Mohammed Ammad Shafiq, Mahyar Tourchi Moghaddam, and Mina Alipour. 2026. From Blind Edits to Verified Repair: Building Trustworthy User-Side LLM Agents for Web Accessibility. arXiv preprint arXiv:2608.24913 (2026). Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

25

[109] Willian M Watanabe, Vanice Dalto, and André Pimenta Freire. 2026. ARIA region landmarks identification using a DOM-structure similarity classification and clustering pipeline. Universal Access in the Information Society 25, 1 (2026), 10. [110] WebAIM. 2024. Screen Reader User Survey #10 Results. https://webaim.org/projects/screenreadersurvey10/. Accessed: July 16, 2026. [111] WebAIM. 2026. WAVE Web Accessibility Evaluation Tool. https://wave.webaim.org/. Accessed: 2026-08-16. [112] Brian Wentz and Jonathan Lazar. 2011. Are separate interfaces inherently unequal? An evaluation with blind users of the usability of two interfaces for a social networking platform. In Proceedings of the 2011 iConference. 91–97. [113] Brian Wentz and Jonathan Lazar. 2011. Usability evaluation of email applications by blind users. Journal of Usability Studies 6, 2 (2011), 75–89. [114] Katy Whitelaw. 2003. Why make websites accessible? and how?. In Proceedings of the 31st annual ACM SIGUCCS fall conference. 259–261. [115] Brianna L. Wimer, Ritesh Kanchi, Kaija Frierson, Venkatesh Potluri, Ronald A. Metoyer, Jennifer Mankoff, Miya Natsuhara, and Matt X. Wang. 2026. Nonvisual Support for Understanding and Reasoning about Data Structures. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems, CHI 2026, Barcelona, Spain, April 13-17, 2026, Nuria Oliver, David A. Shamma, Heloisa Candello, Pablo César, Pedro Lopes, Alessandro Bozzon, Thomas Kosch, Vera Q. Liao, Xiaojuan Ma, Valentino Artizzu, Fiona Draxler, Gustavo López, Anke V. Reinschluessel, Xin Tong, and Phoebe O. Toups Dugas (Eds.). ACM, 1113:1–1113:21. doi:10.1145/3772318.3791656 [116] Anyi Xu, Bangcai Lin, Bing Xue, Bingxuan Wang, Bingzheng Xu, Bochao Wu, Bowei Zhang, Chaofan Lin, Chen Dong, Chenchen Ling, et al. 2026. Deepseek-v4: Towards highly efficient million-token context intelligence. arXiv preprint arXiv:2606.19348 (2026). [117] Tao Yang, Prathik Gadde, Robert Morse, and Davide Bolchini. 2013. Bypassing lists: accelerating screen-reader fact-finding with guided tours. In Proceedings of the 15th International ACM SIGACCESS Conference on Computers and Accessibility. 1–8. [118] Yeliz Yesilada, Robert Stevens, Carole Goble, and Shazad Hussein. 2003. Rendering tables in audio: the interaction of structure and reading styles. ACM SIGACCESS Accessibility and Computing 77-78 (2003), 16–23. [119] Daihua Xie Yu and Bambang Parmanto. 2011. US state government websites demonstrate better in terms of accessibility compared to federal government and commercial websites. Government Information Quarterly 28, 4 (2011), 484–490. [120] Yaman Yu, Bektur Ryskeldiev, Ayaka Tsutsui, Matthew Gillingham, and Yang Wang. 2025. From cluttered to clear: Improving the web accessibility design for screen reader users in e-commerce with generative AI. In Proceedings of the 27th International ACM SIGACCESS Conference on Computers and Accessibility. 1–19. [121] Mengxi Zhang, Yan Zhang, Guangyong Gao, and Huaxiao Liu. 2024. Enhancing accessibility of web-based SVG buttons: An optimization method and best practices. Expert Systems with Applications 238 (2024), 121883. [122] Mingrui Ray Zhang, Mingyuan Zhong, and Jacob O Wobbrock. 2022. Ga11y: An automated gif annotation system for visually impaired users. In Proceedings of the 2022 CHI Conference on Human Factors in Computing Systems. 1–16. [123] Ziyun Zhang, Zezhou Wang, Xiaoyi Zhang, Zongyu Guo, Jiahao Li, Bin Li, and Yan Lu. 2026. Infiniteweb: Scalable web environment synthesis for gui agent training. In Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 28465–28492. [124] Mingyuan Zhong, Ruolin Chen, Xia Chen, James Fogarty, and Jacob O Wobbrock. 2025. Screenaudit: Detecting screen reader accessibility errors in mobile apps using large language models. In Proceedings of the 2025 CHI Conference on Human Factors in Computing Systems. 1–19. [125] Mingyuan Zhong, Xia Chen, Davin Win Kyi, Chen Li, James Fogarty, and Jacob O Wobbrock. 2026. TaskAudit: Detecting Functiona11ity Errors in Mobile Apps via Agentic Task Execution. In Proceedings of the 2026 CHI Conference on Human Factors in Computing Systems. 1–20. [126] Shuyan Zhou. 2026. WebArena-Infinity: Generating browser environments with verifiable tasks at scale. shuyanzhou. com, March (2026).

A

LTL Semantics

Linear Temporal Logic (LTL) specifies the behavior of systems that change over time. The LTL syntax that we use in this paper extends propositional logic with four temporal operators. A propositional formula 𝑃 is one of the following: an atom x, a conjunction 𝑃 0 ∧ 𝑃1 , a disjunction 𝑃 0 ∨ 𝑃1 , an implication 𝑃0 → 𝑃 1 , or a negation ¬ 𝑃 0 . The atoms come from some finite set; typically, one that describes a dynamic system. An LTL formula 𝑄 is one of the following: • a propositional formula 𝑃, or a conjunction, disjunction, implication, or negation of LTL formulas; • an “always” formula G(𝑄 0 ); • an “eventually” (or “finally”) formula F(𝑄 0 ); • a “next” formula X(𝑄 0 ); or • an “until” formula 𝑄 0 U 𝑄 1 . Semantically, an LTL formula describes a set of traces, each of which describes one run of the system under test. We model traces as infinite sequences of sets of atoms. For example, the trace 𝑇 = 𝑇0,𝑇1,𝑇2, . . . where 𝑇𝑖 = {Red} if 𝑖 is even and 𝑇𝑖 = {Green} if 𝑖 is odd describes an execution of a stoplight in which the Red and Green lights alternate forever. Manuscript submitted to ACM

26

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang Let 𝑇 >> 𝑘 be the suffix of trace 𝑇 obtained by dropping the first 𝑘 elements. For example, 𝑇 >> 0 = 𝑇 and

𝑇 >> 2 = 𝑇2,𝑇3, . . . (dropping 𝑇0 and 𝑇1 ). A temporal formula 𝑄 is satisfied by a trace 𝑇 , written 𝑇 ⊨ 𝑄, under the following conditions:

B

• 𝑇 ⊨ G(𝑄 0 )

if 𝑇 >> 𝑘 ⊨ 𝑄 0 for all 𝑘 ∈ N;

• 𝑇 ⊨ F(𝑄 0 )

if 𝑇 >> 𝑘 ⊨ 𝑄 0 for some 𝑘 ∈ N;

• 𝑇 ⊨ X(𝑄 0 )

if 𝑇 >> 1 ⊨ 𝑄 0 ;

• 𝑇 ⊨ 𝑄0 U 𝑄1

if 𝑇 >> 𝑘 ⊨ 𝑄 1 for some 𝑘 ∈ N and 𝑇 >> 𝑗 ⊨ 𝑄 0 for all 𝑗 < 𝑘.

PRISMA records

ACM Digital Library search results (July 2026). IEEE Xplore search results (July 2026). Springer Nature Link. ("blind" OR "low vision" OR "screen reader" OR "visually impaired") AND ("web" OR "webpage" OR "website" OR "browser") AND ("failure" OR "barrier" OR "error" OR "difficulty" OR "problem" OR "inaccessible" OR "usability")

Special selection due to system search of Springer Nature Link. - Content type → **Article** - Language → **English** - Subjects → **Interaction design**, **Web accessibility evaluation and user experience**, **User interfaces and human computer interaction** - Subdisciplines → User interfaces and human computer interaction Elsevier ScienceDirect. Keywords varied since the limitations of figures via search ("Use fewer boolean connectors (max 8 per field"). ("blind" OR "visually impaired" OR "low vision") AND ("web" OR "website") AND ("accessibility" OR "barrier" OR "failure" OR "usability")

- Content type → Research Articles Q1: ("blind" OR "low vision" OR "screen reader" OR "visually impaired") AND ("web" OR "webpage" OR "website" OR "browser" OR "web application") AND ("failure" OR "barrier" OR "error" OR "difficulty" OR "problem" OR "inaccessible" OR "usability" OR "challenge" OR "obstacle") Q2: ("blind" OR "screen reader" OR "visually impaired") AND ("web" OR "website" OR "browser") AND ("keyboard" OR "navigation" OR "interaction" OR "focus") AND ("failure" OR "barrier" OR "problem" OR "challenge") Table 8. Record counts and deduplication prior to screening. Q1 yielded 112 records (abstract field) and 3 records (title field); Q2 yielded 16 records, all subsumed by Q1. After deduplication, 113 unique records remained for screening. Source / step ACM DL Abstract + Title search IEEE Xplore Abstract search Springer ScienceDirect Q1+Q2 Total records for screening

C

𝑛

Reduced

Screen Sampling

196 138 383 238 115+16

−6 (not papers) −4(not papers) −2 (Duplicate) −18 (Duplicate)

6 4 12 8 0

1,056

30

A11y-CUA Trace Annotation

While our systematic literature review captures a broad foundation of accessibility barriers, published studies often report broad findings that lack the step-by-step execution traces needed for formalization [52]. Furthermore, taxonomies Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

27

from previous literature may not fully reflect the temporal navigation errors that appear in highly dynamic websites [34]. To complement our literature synthesis with concrete evidence, we analyzed empirical interaction traces from the A11y-CUA dataset [44], which records blind and low-vision (BLV) users completing 12 everyday tasks on websites using screen readers and keyboard navigation. Rather than treating task completion as a single binary outcome, we analyzed the traces as sequences of individual actions. Specifically, we identified cases where users’ navigation was interrupted, took unnecessary steps, or led to unexpected interface states that they had to recover from [61]. For each case, we recorded the task context, the interactions leading to the navigation error, and its effect on user progress. We then compared navigation errors across tasks and grouped cases with similar navigation problems into general failure types. For example, repeatedly navigating through irrelevant page structures was categorized as excessive sequential navigation, while unexpected focus jumps back to earlier parts of the page were categorized as focus reset failures. This grouping captures frequent navigation problems across different websites and tasks. Finally, we focused on navigation errors caused by interface behavior, including keyboard navigation, focus management, widget interaction, and the exposure of dynamic elements, while excluding cases caused by user mistakes or operating system behavior. These failure types, derived from prior literature and real-world traces, form the basis for our temporal properties. D

Detailed Failure Taxonomy

Table 2 shows the full failure taxonomy from L1 to L3 levels. Table 9. Taxonomy of BLV web accessibility failures, organised by the level of evidence required to observe them (Table 1). Levels are cumulative rather than compositional: an L3 failure persists even when every L1 and L2 check passes. A failure domain therefore recurs across levels—a missing text alternative is an L1 failure, a state change that is never announced is an L2 failure, and a description that is present yet does not reveal goal-relevant information is an L3 failure. Evidence cites the reporting studies, including our own A11y-CUA sessions with blind screen-reader participants [44]. Appendix C describes our trace annotation procedure for A11y-CUA sessions. The temporal properties instantiated for the formalised subset are given in Table 10. Category L1: Element-level

Failure

Example

Evidence

decidable by rule-based checking of the rendered page

Text alternatives

No alt text, label, or accessible name

an image, chart or animation with no alt attribute; a form field whose visible label is not bound to the control; a link whose only content is an icon; a CAPTCHA offering no audio route

[8, 10, 15, 19, 26, 28, 32, 41, 47, 54, 56, 63, 66, 66, 69, 85, 89, 93, 103, 104, 113, 114, 119–122]

Structure and semantics

No headings or landmarks

a page built entirely from <div> and <span>, offering nothing to jump between

[18, 19, 44, 100, 114, 120]

Improper heading levels or structural tags

a section heading marked <h4> purely because that size looked right; every heading on the page at the same level

[39, 63, 120]

No skip link past the navigation

the same forty navigation links must be traversed on every page before the content begins

[44, 82, 93]

Broken or duplicated links

a product thumbnail and its title announced as two separate links to the same page; a menu entry leading to a dead URL

[8, 8, 26, 83, 89, 114]

Keyboard

No keyboard path to a control

a <div> styled as a button that Tab never reaches; a slider that responds only to dragging

[32, 78, 83]

L2: Interaction-level

surfaces only when the page is driven; invisible to static checking

Keyboard and focus

Loss of focus after activation

after confirming a departure airport, focus returns to the top of the page and the date fields must be found again

[32, 44, 47, 48, 52, 82]

No exit from a composite widget

Tab is intercepted inside a video description panel and never advances to the next control

[44]

continued on the next page

Manuscript submitted to ACM

28

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 2, continued Category

Failure

Example

Evidence

Improperly hidden elements remain focusable

Tab stops on items in a collapsed carousel and the screen reader announces an empty string

[44, 113, 114]

No valid active option in an expanded combobox

the suggestion list is open but no option is marked as current, so nothing is announced while arrowing

[44, 113]

No active-option movement on arrow keys

pressing Down inside an open suggestion list does not advance to the next entry

[44, 114]

No commit state after option selection

Enter on a highlighted airport leaves the field showing a partial string, and the user believes the choice was taken

[44, 113]

No valid active cell in a managed grid

a date picker opens with no cell marked as current, so arrow keys have no starting point

[44]

No active-cell movement on arrow keys

Tab passes over the whole calendar, and the arrow keys that would move within it are never announced

[44]

No effect from a role-specific activation key

a calendar cell is selected only by Space; pressing Enter repeatedly produces nothing

[44, 83]

No feedback confirming an activation

after submitting a form nothing is announced, and the user re-reads the page to find out whether it was accepted

[14, 19, 52, 63, 89, 93, 113]

Misplaced or disconnected response to an activation

a filter updates a results panel further down the page with nothing tying the two together; correcting a typo re-opens the suggestion list on every keystroke

[13, 14, 44, 47, 95, 104, 113, 114]

ARIA state contradicts the native state

a checkbox reported as aria-checked="false" while the native control is checked

[44]

No exposed expanded state after a reveal

an accordion panel opens visually but the trigger continues to report itself as collapsed

[8, 44]

No trace of operation progress or mode

an upload gives no sign of whether it is running or has stalled; the same key both inspects and edits a block, with nothing saying which just happened

[52, 65, 113, 113]

No accessible name or named dismissal control on a dialog

a consent banner is announced only as dialog, with no way to tell what it is or how to close it

[13, 26, 44, 45, 63, 112]

No focus move into a newly opened dialog

a cookie notice appears over the page while focus stays behind it, so the user keeps reading content that is now blocked

[13, 44, 113]

No dialog dismissal or focus return on Escape

Escape does not close the overlay; when it finally closes, focus is left at the top rather than on the control that opened it

[44]

No reachable control to start playing or stop playing media

a video begins on load and its pause control is neither reachable by Tab nor announced

[73, 83, 103]

Structure and semantics

Inadequate labels to reveal nearby context

a price is read out with no indication of which product row or which column it belongs to

[8, 14, 19, 64, 113, 114]

AT interoperability

Inconsistent name exposure across reading modes

a password field is announced by name while browsing, but only as edit box once the user starts typing

[19, 88]

Screen-reader shortcut captured outside the page

the context-menu command opens the browser’s own menu instead of the page’s; an injected accessibility widget claims keys the user’s screen reader needs

[44, 68]

Composite widgets

Feedback and state

Dynamic content

L3: Task-level

persists when L1 and L2 checks pass; the failure lies in the fit between structure and goal

Feedback and state

No guidance for recovering from a rejected action

a submission is refused with no indication of which field was wrong or what format it expected; a category must exist before an expense can be added, and nothing says so

[14, 52, 93]

Text alternatives

Inadequate description of goal-relevant information

a binary tree described as running prose, leaving parent and child relations unrecoverable; a chart summarised in one sentence when the task requires comparing series; a link named read more among twenty others

[4, 10, 13, 35, 38, 41, 48, 54, 56, 59, 60, 63, 64, 66, 66, 83, 89, 93, 104, 114, 115, 118, 120]

Structure and semantics

Reading order and grouping inconsistent with the task’s logic

a product’s price is read far from its name; the store-locator sits under Account rather than under Stores

[1, 35, 39, 60, 63, 82, 88, 89, 93, 112, 117, 120]

Excessive heading marks relative to page content

every list item carries a heading, so the heading list is as long as the page

[39, 120]

continued on the next page

Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

29

Table 2, continued Category

Navigation efficiency

E

Failure

Example

Evidence

Tab order inconsistent with the task’s order

the submit button is reached before the fields it depends on

[8, 32]

Position learned from prior visits no longer predicts where the control is

the submit button sits in the top bar on one page and after the last field on the next

[52, 113]

No efficient route to the control the task requires

reaching a store-selection setting takes several hundred Tab presses through the footer

[13, 27, 33, 38, 44, 88, 89, 93, 113]

No confirmation of completeness, driving reverification

a forum thread is re-read from the top because nothing confirms that no later reply revised the answer

[12–14, 39, 48, 59]

No means of resuming from a prior position

returning from a product page drops the user at the top of the results list rather than at the item they left

[14, 91, 92]

Failure-to-Temporal-Property Mapping

For readability, we assign compact property identifiers by taxonomy level, like L1-01, L2-01, and so on. Table 10 shows how the failure categories formalized by A11yLTLNav map to executable temporal properties. A failure may map to more than one property when distinct observable interaction mechanisms require separate checks. Failure categories that are outside the current executable property set remain in the full taxonomy appendix and are not repeated here. Table 10. Mapping from formalized accessibility failures to simplified temporal properties. Each row represents one executable property; a blank Failure cell continues the failure immediately above. Failure

ID

Simplified temporal property

No alt text, label, or accessible name

L1-01

G(exposed(𝑥 ) ∧ nameReq(𝑥 ) → hasNameOrTextAlt(𝑥 ) )

No headings or landmarks

L1-02

G(documentComplete → orientationAnchorCount > 0)

Improper heading levels or structural tags

L1-03

G(documentComplete → ¬forwardHeadingSkip)

L1: Element-level

L1-04

G(longPreMainPrefix → bypassPresent)

L1-05

G(activateBypass(𝑐, 𝑡 ) → X validContinuation(𝑡 ) )

Broken or duplicated links

L1-06

G(documentComplete → ¬redundantLocalLinkPair)

No keyboard path to a control

L1-07

G(eligibleControl(𝑐 ) → tabReachable(𝑐 ) )

No skip link past the navigation

L2: Interaction-level Loss of focus after activation

L2-01

G(localInvalidation(𝑐 ) → X exposedFocus)

L2-02

G(majorViewTransition(𝑐 ) → X orientationCue(𝑐 ) )

No exit from a composite widget

L2-03

G(blockedTab(𝑐 ) → X focusMoves(𝑐 ) )

Improperly hidden elements remain focusable

L2-04

G(trustedTab → X(¬focusHidden) )

No valid active option in an expanded combobox

L2-05

G(expandedCombobox(𝑐 ) → validActiveOption(𝑐 ) )

No active-option movement on arrow keys

L2-06

G(comboboxArrow(𝑐, 𝑘, 𝑛) → X(activeDescendant(𝑐 ) = 𝑛) )

No commit state after option selection

L2-07

G(enterOnActiveOption(𝑐, 𝑜 ) → X(committed(𝑐, 𝑜 ) ) )

No valid active cell in a managed grid

L2-08

G(managedGrid(𝑔) → validActiveCell(𝑔) )

No active-cell movement on arrow keys

L2-09

G(gridArrow(𝑔, 𝑘, 𝑛) → X(activeCell(𝑔) = 𝑛) ) continued on the next page

Manuscript submitted to ACM

30

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 10, continued Failure

ID

Temporal property

No effect from a role-specific activation key

L2-10

G(roleActivation(𝑐, 𝑘, 𝑒 ) → X(exactEffect(𝑒 ) ) )

No feedback confirming an activation

L2-11

G(effectfulActivation(𝑐 ) → X notifiableFeedback(𝑐 ) )

ARIA state contradicts the native state

L2-12

G(nativeCheckableARIA(𝑐 ) → ariaChecked(𝑐 ) = nativeChecked(𝑐 ) )

L2-13

G(nativeOptionWithARIA(𝑜 ) → ariaSelected(𝑜 ) = nativeSelected(𝑜 ) )

L2-14

G(nativeRangeWithARIA(𝑞) → ariaValueNow(𝑞) = nativeValue(𝑞) )

No exposed expanded state after a reveal

No accessible name or named dismissal control on a dialog

L2-15

G(expansionAction(𝑐, 𝑟 ) → X(ariaExpanded(𝑐 ) = exposed(𝑟 ) ) )

L2-16

G(disclosureReveal(𝑐, 𝑟 ) → X(ariaExpanded(𝑐 ) = exposed(𝑟 ) ) )

L2-17

G(visibleDialog(𝑑 ) → hasProgrammaticName(𝑑 ) )

L2-18

G(visibleDialog(𝑑 ) → namedFocusableAction(𝑑 ) )

No focus move into a newly opened dialog

L2-19

G(openNewModal(𝑑 ) → X(focusInside(𝑑 ) ) )

No dialog dismissal or focus return on Escape

L2-20

G(escapeInDialog(𝑑 ) → X(¬exposed(𝑑 ) ) )

L2-21

G(escapeClosesModal(𝑑, 𝑣) → X(focus = 𝑣) )

L3-01

G(nativeRejection(𝑓 ) → X actionableGuidance(𝑓 ) )

L3-02

G(newARIAInvalid(𝑖 ) → X(linkedGuidance(𝑖 ) ) )

L3: Task-level No guidance for recovering from a rejected action

E.1

Meaning and scope of the executable properties

Table 11 explains the operational meaning of each property without repeating its formula. The Scope column records only important boundaries on what the property claims to detect; an em dash means that no additional boundary is needed beyond the triggering conditions stated in the formula. Table 11. Operational meaning and scope of the temporal properties in Table 10. ID

What it checks

Scope

L1: Element-level L1-01

Every exposed element that requires a name or text alternative must expose one.

Covers supported name-required elements; adequacy of an existing name is outside this property.

L1-02

A completed content-bearing page should expose at least one heading or landmark for nonvisual orientation.

—

L1-03

The exposed heading sequence should not jump forward by more than one hierarchy level.

Covers heading-level discontinuities, not every kind of semantically inappropriate structural markup.

L1-04

A long keyboard-navigation prefix before main content should provide a usable bypass control.

—

L1-05

Activating an exact main-content bypass should establish a valid keyboard validContinuation(𝑡 ) means focus reaches the continuation at its target. target directly or the requested next Tab reaches the expected continuation at or after it. continued on the next page

Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

31

Table 11, continued ID

What it checks

Scope

L1-06

A local image/text pair for the same destination should be exposed as one Covers the duplicated-local-link subtype; unreachnavigation opportunity. able or dead URLs are outside this property.

L1-07

Every eligible standalone semantic control should be reachable through sequential keyboard navigation.

eligibleControl(𝑐 ) abbreviates an exposed, enabled standalone semantic control; tabReachable(𝑐 ) means sequentially keyboard-focusable. Compositewidget descendants and controls with no declared interactive semantics are outside this property.

L2: Interaction-level L2-01

A local activation that invalidates its control should leave settled focus on localInvalidation(𝑐 ) denotes control invalidation a concrete exposed element. within a stable local view; exposedFocus requires concrete connected and programmatically exposed focus.

L2-02

After a major same-document view transition, the interface should estab- orientationCue(𝑐 ) means focus enters the new lish the user’s orientation in the new context. context or the persistent invoker gains a currentlocation cue.

L2-03

If page code blocks Tab while another usable keyboard target exists, settled focus should leave the current control.

blockedTab(𝑐 ) combines author-cancelled Tab with an available alternative target; this remains a single-step no-progress check rather than complete cycle detection.

L2-04

Tab navigation should not land on a programmatically hidden element.

—

L2-05

An expanded managed combobox should identify one valid active option.

—

L2-06

An admitted arrow-key action should move the combobox active option to the inferable adjacent option.

—

L2-07

Pressing Enter on the active option should commit that exact option.

—

L2-08

A managed grid should expose one valid active cell.

—

L2-09

An admitted arrow-key action should move the grid active cell to the inferable adjacent cell.

—

L2-10

When a role/key pair has a declared browser effect, activating it should produce that effect.

Generic buttons without a declared exact effect remain outside this property.

L2-11

An activation that changes the interface should produce at least one AT-surfaceable feedback signal.

notifiableFeedback(𝑐 ) includes a focus move, focused-control state or name change, live notification, or same-document navigation; it does not prove actual screen-reader speech.

L2-12

Redundant aria-checked should agree with the native checked or indeterminate state.

—

L2-13

Redundant aria-selected should agree with the native option selected state.

—

L2-14

Redundant aria-valuenow should agree with the native range value.

—

L2-15

After an expansion or collapse action, aria-expanded should match whether the controlled region is exposed.

—

L2-16

When a local disclosure reveals content, the revealing control should expose expanded state consistent with the region.

—

L2-17

Every visible dialog should expose a non-empty programmatic name.

—

L2-18

Every visible dialog should expose at least one named, enabled, sequentially focusable action.

Establishes an identifiable action candidate; it does not prove that the action dismisses the dialog. continued on the next page Manuscript submitted to ACM

32

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 11, continued ID

What it checks

Scope

L2-19

Opening a new modal should move keyboard focus into that exact modal.

—

L2-20

Pressing Escape in the active dialog should close or hide that exact dialog.

—

L2-21

When Escape closes a modal and its invoker remains eligible, focus should return to that exact invoker.

—

L3-01

When native form validation rejects submission, the form should expose actionable guidance for at least one invalid field.

actionableGuidance(𝑓 ) summarizes linked accessible guidance or focused native validation guidance; arbitrary task-level prerequisites remain outside this property.

L3-02

When an action newly marks a field aria-invalid=true, that field should expose programmatically linked guidance.

Covers action-bound aria-invalid transitions, not arbitrary task-level prerequisites.

L3: Task-level

E.2

Notation used in simplified temporal properties

Table 12 defines the logical symbols and variables used in Table 10. Domain-specific predicate names are short descriptive atomic propositions; their operational meanings are given in Table 11. Table 12. Notation used in the simplified temporal properties. Symbol

Meaning

Interpretation / use

Temporal and logical operators

G

Globally / always

X

Next logical state

The next relevant post-action state after the triggering interaction.

∧

Logical AND

Both conditions must hold.

∨

Logical OR

At least one condition must hold.

¬

Logical NOT

The following condition must not hold.

→

Implication

If the condition on the left occurs, the condition on the right is required.

The property must hold whenever its triggering condition occurs along the interaction trace.

=

Equality

Two observed values or identities must agree.

>

Greater than

Used for threshold predicates such as requiring at least one orientation anchor.

Variables

𝑥

Generic interface element

Used when a property is not tied to a particular control type.

𝑐

Control

The interactive control that triggers or owns the relevant state.

𝑘

Keyboard key

The key used for the interaction, such as Enter, Space, or an arrow key.

𝑒

Expected / declared effect

The browser-observable effect associated with a role-specific activation.

𝑡

Target

The target of a bypass or navigation control.

𝑑

Dialog / modal

The exact dialog involved in opening, closing, naming, or focus management.

𝑣

Invoker

The exact control that opened a modal and should receive focus again after closing. A form field identified as invalid.

𝑖

Invalid field

𝑜

Option

The active or selected option in a combobox or listbox.

𝑔

Grid

The managed grid whose active cell is being checked.

𝑟

Controlled / revealed region

The region whose exposed state should correspond to a disclosure control. continued on the next page

Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

33

Table 12, continued Symbol

Meaning

Interpretation / use

𝑞

Native range control

A slider or range input whose native value is compared with aria-valuenow.

𝑛

Next item

The inferable adjacent option or grid cell expected after an arrow-key action.

𝑓

Form

The native form involved in a validation rejection.

Atomic propositions Predicate names

E.3

Descriptive atomic propositions

Composite names abbreviate browser-observable conditions. Examples include eligibleControl, orientationCue, and notifiableFeedback; Table 11 gives their operational meaning and scope.

Unformalized Failure Taxonomies

Across the 36 failure categories in our taxonomy in the main text, the current property set operationalizes 22 with at least one executable temporal property. The remaining 14 are not omitted because they are inexpressible in LTL. Rather, an executable property must be grounded in predicates that the checker can observe and attribute to a concrete interaction. For these failures, at least one required predicate depends on information that is not available from browser state alone, such as a semantic relation between interface regions, an operation lifecycle, assistive-technology behavior, a task or relevance oracle, a calibrated cost threshold, or persistent cross-view identity. Table 13 summarizes these boundaries and the additional support that would be needed to encode them as Bombadil properties. Table 13. Taxonomy failures not directly formalized by the current browser-observable property set. These failures are not necessarily inexpressible in LTL; the limitation is that one or more predicates needed for an executable check are not currently grounded by Bombadil. Level

Failure

Why it is not directly executable

Additional Bombadil support needed

L2

Misplaced or disconnected response to an activation

A state change can be observed, but browser state alone does not establish which region is the semantically intended response to the triggering control.

A declared or inferred trigger-to-responseregion relation that binds the activated control to the region expected to change.

L2

Inadequate labels to reveal nearby context

The checker can observe a label and surrounding elements, but it cannot infer which nearby context is necessary for the label to be meaningful.

An element-to-context relation or semantic oracle specifying which surrounding information is required for interpretation.

L2

No trace of operation progress or mode

Checking progress or mode requires knowing when an operation starts, remains active, changes phase, and completes; those lifecycle boundaries are not generally exposed by the page.

An operation or mode lifecycle recorder with explicit start, progress, completion, and cancellation states.

L2

No reachable control to stop autoplaying media

The checker may observe media and controls A media-to-control binding plus a reachaindependently, but it cannot reliably determine bility check for the identified stop or pause which control stops the exact auto-playing control. media instance.

L2

Inconsistent name exposure across reading modes

DOM and ARIA state do not establish how a screen reader exposes the same element in browse mode versus forms or focus mode.

Assistive-technology-level observations aligned with screen-reader mode and browser focus. continued on the next page

Manuscript submitted to ACM

34

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

Table 13, continued Level

Failure

Why it is not directly executable

Additional Bombadil support needed

L2

Screen-reader shortcut captured outside A failed shortcut may be handled by the page, the page browser, operating system, extension, accessibility widget, or screen reader; browser-level evidence cannot reliably attribute the capture.

L3

Inadequate description of goal-relevant information

Whether an existing description is sufficient A task or relevance oracle that represents depends on what information the user’s task the user’s information goal and judges requires, not only on whether the description is whether the exposed description supports it. present.

L3

Reading order and grouping inconsistent with the task’s logic

The browser exposes document order and grouping, but the checker does not know the task-dependent relationships that should determine the useful order or grouping.

A task model that specifies relevant objects, relationships, and expected grouping or ordering.

L3

Excessive heading marks relative to page content

Heading density is observable, but there is no task-independent threshold at which the number of headings becomes excessive for navigation.

A calibrated density or navigation-cost threshold, potentially conditioned on page structure or task context.

L3

Tab order inconsistent with the task’s order

The actual Tab sequence is observable, but the checker has no general oracle for the order in which controls should be encountered for a particular goal.

A declared task order or task-derived partial order over relevant controls.

L3

No efficient route to the control the task Efficiency requires both knowing the taskrequires relevant target and deciding how much navigation cost is acceptable; neither is defined by browser state alone.

A task-target oracle together with a navigation-cost model or explicit cost bound.

L3

No confirmation of completeness, driving re-verification

The checker cannot infer when the user has seen enough task-relevant evidence to know that a review or search is complete.

A task-completion model that represents relevant evidence and the conditions under which completeness can be established.

L3

No means of resuming from a prior position

Checking resumption requires a stable identity for the user’s prior interaction position across navigation or re-rendering and a definition of equivalent restoration.

Persistent cross-view position identity and history tracking that can compare the restored location with the prior task position.

L3

Position learned from prior visits no longer predicts where the control is

Detecting positional inconsistency requires comparing a control’s location across comparable pages or prior visits, which cannot be determined from a single browser execution state.

Persistent cross-view element identity together with a model of comparable page structure or expected control location.

OS- and assistive-technology-level keyevent tracing that identifies which component consumed the shortcut.

The 22 mapped failure categories should therefore be interpreted as coverage by at least one executable property, not as exhaustive coverage of every instance of that category. Several implemented properties intentionally capture narrower, high-confidence subtypes for which the trigger and expected outcome can be observed reliably in the browser. This conservative boundary keeps the properties aligned with what the Bombadil monitor can actually establish from an execution trace. F

Prompts for Website Generation

We provide the complete prompt used to generate the website clones in our evaluation. The prompt is adapted from the website-generation procedure of uxCUA [40], with one key modification: rather than allowing the coding agent to Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

35

invent additional workflows, we provide the original Mind2Web tasks associated with each selected website as a closed specification of the workflows that the generated website must support [29]. For each generation run, <WEBSITE_NAME> is replaced with the corresponding website name and <MIND2WEB_TASKS> with all Mind2Web tasks associated with that website. All remaining instructions are kept fixed across website-generation runs. You are an expert web developer and designer specializing in modern websites. You are currently handed a barebones React.js template and your jobs is to make a fully working website using React.js. Feel free to use lightweight libraries like Tailwind CSS to enhance the design. Requirements: 1. Create a fully functional, modern, and responsive website design 2. Use only React.js, HTML, CSS, and JavaScript, but feel free to use libraries like Tailwind CSS to make the design better and make layout easier. You can look at the package.json file to see which libraries are already installed and import them. However, you must NEVER install new packages that were not already installed. 3. Include interactive elements where appropriate 4. Make it production-ready and professional 5. You must include all relevant script tags for libraries to work properly. 6. There should NEVER be any dead links or buttons that are visible but do nothing when clicked. 7. The ONLY time you are allowed to run the `npm` command is to test if the website builds with `npm run build` command. You must NEVER run `npm` under any other circumstances. 8. Because you will create a website with very realistic mocked functionality, you will probably need some data. ALWAYS synthetically generate placeholder data that is needed by any functionality on the mocked website. NEVER attempt to connect to online APIs. 9. NEVER include images for which you do not have the appropriate path to (e.g., the "src" attribute). You should use an API to generate a placeholder instead like <img src="https://placehold.co/600x400" alt="Placeholder image"> 10. Do not define any new SVGs - you should use icons from FontAwesome instead from the packages: @fortawesome/fontawesome-svg-core @fortawesome/free-solid-svg-icons @fortawesome/react-fontawesome. You can assume that these packages are installed even though you cannot see them in a package.json in the same directory. 11. NEVER attempt to access any external directory outside of your current directory. Your job is to create a fully functioning clone of the following website: <WEBSITE_NAME> The workflow tasks below are injected experiment inputs. They are the complete and only workflow set for this website generation run. <MIND2WEB_TASKS> Use the current barebones React.js project with React Router to implement this website, with all important functionality realistically mocked. The main React file is located at src/App.jsx and exports a component called "App." Make sure your code conforms to this structure. Your workflow should be something like the following:

Manuscript submitted to ACM

36

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang

1. Read every injected workflow task above. Do not invent, infer, propose, or add any workflow that is not explicitly listed there. If the injected workflow task list is missing or empty, stop and report the missing input instead of generating workflows. 2. Implement the React.js website so that every injected workflow task is fully implemented, interactive, and uses the appropriate mock data. You may add supporting UI needed to make the listed tasks and visible navigation work, but you must not turn supporting UI into additional workflows. 3. Run `npm run build` command to test that website compiles without any errors. 4. Return to step 1 and verify the implementation against the same injected workflow task list until every listed task works. Do not expand the workflow set during this process. When you think you are done, scan for any dead links or unimplemented functionality and implement them without creating new workflow tasks. Finally, when you are done, make a text file in the root directory of the React.js project (at the same level as the src/ directory) called "flows.txt". It must contain exactly the injected workflow tasks, in the same order, with the concrete steps and expected result supported by the implementation. Use a single heading named `## Required Flows (injected tasks)`. Do not create an `Additional Flows` section, do not add self-identified flows, and do not include any workflow that was not present in the injected task list.

G

Prompts Used in Task-based Agentic Accessibility Checker

The following prompts are used for task-based agent accessibility checker adapted from taskAudit [125]. Since we generate the websites based on the tasks instead of detecting the buttons on the webpages, task generator is no longer needed for our pipeline. For other parts of the agentic system, we use the same architecture as taskAudit, but Since the original prompts are based on Talkback screen reader and mobile app navigation, we changed the prompt accordingly from mobile app using and Talkback to web browsing and orca screen reader (V3.36.6) on Linux. G.1

Decision

The following prompts are used for the decision agent. <role> Operate a Linux webpage through the Orca screen reader. Navigate exclusively through webpage controls using the action space below. Prior decisions, observations, and reflections are the state of one continuous task. </role> <task> {{TASK}} </task> <environment> - You are using a Linux desktop browser with the Orca screen reader. - A transcript contains Orca speech produced by the preceding action. Its last item is the most recent utterance, not necessarily Orca's virtual-navigation position or browser keyboard focus. `<wrap>` means navigation reached one end of its sequence and wrapped. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

37

- Tab and Shift+Tab move browser keyboard focus to the next or previous focusable control. The runtime prevents them from crossing from webpage content into browser chrome. - Enter and Space activate the current webpage control when that control supports the key. - Arrow keys, Home, End, PageUp, PageDown, Backspace, Delete, and Ctrl+Arrow/Ctrl+Home/Ctrl+End are sent to the current Orca/browser context; their effect depends on browse or focus mode and the current control. - `type_text` activates the focused editable control, confirms Orca Focus mode (using an internal mode toggle when needed), types the requested text, and verifies that the focused editable value changed. It is the complete text-entry operation. - `repeat_key` repeats one allowed navigation key, stopping early when its `stop_at` speech substring is observed. - Orca structural-navigation actions request movement of Orca's virtual navigation position to the next or previous matching semantic element and announce that element. They do not themselves activate, click, or edit it, and the Orca position is not necessarily browser keyboard focus: - `orca_next_heading` / `orca_previous_heading`: next / previous heading. - `orca_next_button` / `orca_previous_button`: next / previous button. - `orca_next_link` / `orca_previous_link`: next / previous link. - `orca_next_entry` / `orca_previous_entry`: next / previous text-entry field. - `orca_next_combo_box` / `orca_previous_combo_box`: next / previous combo box. - `orca_next_form_field` / `orca_previous_form_field`: next / previous form control of any supported type. - Orca reading actions report information without activating or editing a webpage control: - `orca_where_am_i`: announce the current item and its accessible context, role, and state when available. - `orca_read_current_line`: announce the line at Orca's current navigation position. - `orca_read_title`: announce the current document or window title. - Use Orca structural navigation only in `WEB_DOCUMENT`. In `BROWSER_CHROME` or `UNKNOWN`, use Escape, Tab, Shift+Tab, and Orca reading actions to recover `document web` before other interaction. - When a webpage accessibility tree is included, it contains webpage content only, not browser chrome. Use it as supporting context together with Orca speech. </environment> <decision_protocol> Propose exactly one immediate action for the current state. If more information is needed, choose one navigation or reading action that gathers it. Choose `STATUS_TASK_COMPLETE` only when the prior conversation and current observation establish that the task is complete. Choose `TASK_IMPOSSIBLE` only when the task cannot be completed. Return one JSON object with `thought`, `action`, and `description` fields. Choose `<action_json>` from this action space: 1. {"action_type": "press_key", "key": "<allowed_key>"} Allowed keys: Tab, Shift+Tab, Enter, Space, Escape, ArrowUp, ArrowDown, ArrowLeft, ArrowRight, Home, End, PageUp, PageDown, Backspace, Delete, Ctrl+ArrowLeft, Ctrl+ArrowRight, Ctrl+ArrowUp, Ctrl+ArrowDown, Ctrl+Home, Ctrl+End. 2. {"action_type": "type_text", "typed_text": "<text>"} 3. {"action_type": "wait", "seconds": "<0 to 10>"} 4. {"action_type": "<orca_action_name>"} Manuscript submitted to ACM

38

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang Allowed Orca actions: orca_next_heading, orca_previous_heading, orca_next_button, orca_previous_button, orca_next_link, orca_previous_link, orca_next_entry, orca_previous_entry, orca_next_combo_box, orca_previous_combo_box, orca_next_form_field, orca_previous_form_field, orca_where_am_i, orca_read_current_line, orca_read_title.

5. {"action_type": "repeat_key", "key": "<key>", "repetitions": "<1 to 20>", "stop_at": "<speech substring or empty string>"} Allowed repeat keys: Tab, Shift+Tab, ArrowUp, ArrowDown, ArrowLeft, ArrowRight, PageUp, PageDown. 6. {"action_type": "STATUS_TASK_COMPLETE"} 7. {"action_type": "TASK_IMPOSSIBLE"} Decision rules: - If editable focus is false, navigate to an editable field before using `type_text`. - Use Tab and Shift+Tab to explore focusable controls, and Orca structural actions to explore semantic element types. - For open-ended `repeat_key` exploration, set `stop_at` to an empty string. To seek a known item, use its full transcript or a distinctive substring and set `repetitions` to the maximum allowed search distance. - Inspect the focused-element transcript before activating with Enter or Space. - Always use double quotes for JSON keys and string values. </decision_protocol> <reflection_protocol> Judge whether the current action's observed result met the expectation stated in its Decision thought. Judge the immediate operation, not whether that single operation completed the whole task. Encourage useful exploration. An empty transcript alone is not evidence that the action produced no change. Choose exactly one answer: - A: the action result met the expectation. - B: the action led to a wrong page and the agent should return to the previous page. - C: the action produced no change. Return one JSON object with `thought` and `answer` fields. </reflection_protocol> <turn>decision</turn> <state> <editable_focus>{{EDITABLE_STATUS}}</editable_focus> <focus_domain>{{FOCUS_DOMAIN}}</focus_domain> <screen_reader_transcript> {{TRANSCRIPT_JSON}} </screen_reader_transcript> <last_spoken_item>{{LAST_SPOKEN_ITEM_JSON}}</last_spoken_item> </state>

G.2

Reflection

The following prompts are used for reflection turns for the website explorer agent. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

39

<turn>reflection</turn> <operation> <thought>{{OPERATION_THOUGHT_JSON}}</thought> <action>{{OPERATION_ACTION_JSON}}</action> </operation> <focus_state> <before editable="{{BEFORE_EDITABLE}}" domain="{{BEFORE_FOCUS_DOMAIN}}" /> <after editable="{{AFTER_EDITABLE}}" domain="{{AFTER_FOCUS_DOMAIN}}" /> </focus_state> <screen_reader_transcript> {{AFTER_TRANSCRIPT_JSON}} </screen_reader_transcript>

G.3

Accessibility Analyzer

The following prompts are used for part 1 of the Accessibility Analyzer. Evaluate one recorded Web screen-reader action with two independent judgments. <evaluation_contract> <overall_task_status> COMPLETE when the task criterion and every required sub-outcome are established at or before this step; otherwise INCOMPLETE. Use the task, prior_task_evidence, and current_task_state for this judgment. </overall_task_status> <immediate_action_status> Derive the expected effect from action and standard_action_semantics, then compare it with the local before/after evidence. SUCCESS requires an established expected effect or a valid boundary/no-change outcome. FAILURE is a screening candidate when the expected observable effect is absent, contradicted, or not established. standard_action_semantics defines the generic operation. agent_intended_operation is a context hint; required widget context must be established by the before evidence. For example, autocomplete-specific ArrowDown behavior requires evidence of an active autocomplete or listbox. </immediate_action_status> <evidence_partition> Overall-task evidence and local-action evidence are separate. COMPLETE and FAILURE may coexist. Accessibility root cause and taxonomy are evaluated in the next stage. </evidence_partition> </evaluation_contract> Return only this JSON object: { "step": 0, "overall_task_status": "COMPLETE or INCOMPLETE", "task_status_reasoning": "one concise evidence-based sentence", "task_evidence": [ { Manuscript submitted to ACM

40

Chenming Ge, Astrid Kewen Peng, Chenyang Shi, Ben Greenman, and Yue Jiang "requirement": "observable task requirement", "status": "SATISFIED or UNSATISFIED or NOT_PROVEN", "evidence_step": 0, "source": "prior_task_evidence or url or focused_element or screen_reader_trace", "detail": "short evidence quote or precise paraphrase" }

], "immediate_action_status": "SUCCESS or FAILURE", "expected_effect": "concise expected immediate observable outcome", "observed_effect": "concise effect supported by this step's before/after evidence", "action_status_reasoning": "one concise comparison of expected and observed effects" } <task> {{TASK_SPECIFICATION_JSON}} </task> <prior_task_evidence> {{PRIOR_TASK_EVIDENCE_JSON}} </prior_task_evidence> <current_task_state> {{CURRENT_TASK_STATE_JSON}} </current_task_state> <local_action> {{LOCAL_ACTION_JSON}} </local_action> <recorded_step>{{CURRENT_STEP}}</recorded_step> Use the recorded step as the top-level step and for current-state evidence. Preserve an earlier evidence_step only when supplied by prior_task_evidence.

The following prompts are used for part 2 of the Accessibility Analyzer. An action performed by an automated agent has failed. Your task is to perform a detailed root-cause analysis to determine if this failure was caused by a specific accessibility error. Use the provided screen-reader transcripts as evidence. First, state the intended action. Second, describe the actual outcome from the transcripts. Third, pinpoint the discrepancy. Finally, determine whether this discrepancy constitutes a Web accessibility or screen-reader interaction error. Classify the failure directly using these semantics: - ACCESSIBILITY_ERROR: The failed interaction is attributable to the accessibility behavior of the Web interface as experienced through the screen reader. Manuscript submitted to ACM

A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

41

- NOT_ACCESSIBILITY_ERROR: The failure is better explained by a non-accessibility cause, such as an agent mistake, harness or infrastructure issue, an action applied in an inappropriate state or context, or a normal or unexpected website state change that does not itself constitute an accessibility problem. Do not require proof or certainty that the Web interface caused the failure. Do not add a conservative burden-of-proof rule. A legitimate screen-reader boundary or no-change behavior is not an accessibility error merely because the action was screened as a failure. If an accessibility error occurred, explain the accessibility problem. If no accessibility error occurred, explain the likely non-accessibility cause. Return only this JSON object: { "is_accessibility_error": true, "problematic_element": "element name or N/A", "element_index": null, "explanation": "concise evidence-based root-cause explanation" } Use JSON null for element_index when the transcript does not provide a usable element index. <task> {{TASK_SPECIFICATION_JSON}} </task> <failed_action> {{FAILED_ACTION_JSON}} </failed_action> <failure_reason_from_stage1> {{STAGE1_FAILURE_REASON_JSON}} </failure_reason_from_stage1> <screen_reader_evidence> <before> {{BEFORE_SPEECH_JSON}} </before> <after> {{AFTER_SPEECH_JSON}} </after> </screen_reader_evidence>

Manuscript submitted to ACM

Related documents

• A11yLTLNav: Automatic Detection of Accessibility Navigation Failures#1011671
• ActReal: System-Level Mobile Agents Challenge Mobile Automation Detection#799278
• ActReal: System-Level Mobile Agents Challenge Mobile Automation Detection#797855
• PDFa11yMut: Measuring Mutation-Specific Detection in PDF Accessibility Checkers#1117872
• AVERT-VLN: Abstention-aware Visual Error Recovery and Training for Vision-and-Language Navigation#1144546