A11yLTLNav: Automatic Detection of Accessibility Navigation Failures

Chenming Ge1, Kewen Peng2, Chengyang Shi1, Ben Greenman2, Yue Jiang2
1University of Michigan 2University of Utah

arXiv preprint, 2026 · Under review at CHI 2027

arXiv Examples

Before: Email button focused

The Email article button has keyboard focus before the email dialog opens.
Ready for the next keypress.

After pressing Enter

The email dialog is now open, but the yellow focus annotation still points to the Email article button behind the dialog.
Dialog opens. Focus stays behind.

The dialog opens. Keyboard focus stays behind.
A11yLTLNav catches accessibility failures across interactions.

Yellow = keyboard focus, where the next keypress goes.

Abstract

A11yLTLNav detects web accessibility navigation failures by checking explicit temporal rules while exploring keyboard interactions. The rules are grounded in studies with blind and low-vision users. Across 31 generated websites, 274 of 309 reported failures were confirmed correct (88.7% precision), without language-model inference during testing.

Try an action. Check what happens next.

The checker selects a keyboard action, observes the resulting accessibility state, and checks temporal rules. A violation produces a failure log. The cycle repeats.
Explore actions → observe states → check rules.
Figure 1 · Enlarge

One rule: open a dialog → move focus inside.

G(openModal(d)→XfocusInside(d))
How the rules and random testing work

G means “every time”; X means “in the next checked state”; d is the dialog. The checker observes the relevant state after the interaction settles.

Linear Temporal Logic (LTL) expresses rules about action sequences. Random testing tries varied sequences of available keyboard actions against those fixed rules. Each failure report records the interaction and resulting state.

Exploration does not guarantee that every failure will be found. Read the method.

See it happen

Watch the checker

00:03 · Focus stays outside. 01:47 · Escape does not close the player.

Checker replay reconstructed from timed screenshots.
Full replay · Evidence & checker output

The task succeeds. Focus is still lost.

After preparing the email

The dialog says Email ready, but the yellow focus annotation identifies the page body instead of a dialog control.
“Email ready.” Focus falls to the page body.

After closing the dialog

The dialog is closed and keyboard focus remains on the page body rather than returning to the Email button.
Dialog closed. Original focus is not restored.
Watch the full agent recording
Task: prepare an email, close the dialog, search for Chiefs.
All four annotated states

Tab inserts text. How does the user leave?

SynthVis Pro's Audio editor, Visual editor, and preview. Open the walkthrough to see the annotated keyboard-focus explanation.
Explore the 3-step illustration →
An exit-path check needs more than one Tab press.

How many errors did each checker find?

Human-reviewed, deduplicated reports · 31 generated websites
CheckerReportedConfirmed
errors		False
positives		Precision
AxeStatic1817194.4%
WAVEStatic68343450.0%
Adapted TaskAuditAgentic27615811857.2%
A11yLTLNavRun 13092743588.7%

Confirmed errors were verified by human reviewers. Static checkers scanned the first page only; counts include findings relevant to blind and low-vision users. Paper · Table 4

Review protocol and evaluation details

Reports were deduplicated by website, component, and checker. Two authors reviewed every report; disagreements were resolved through discussion. Precision is confirmed errors divided by reported findings, not recall.

Across three A11yLTLNav runs, precision ranged from 85.9% to 88.7%. No language-model inference was used during its testing. Detection depends on the paths explored and the state exposed by the browser.

These checks complement static tools and studies with screen-reader users. Read the full evaluation.