Accessibility
New Tool Detects Accessibility Failures in Website Navigation for Screen-Reader Users
A11yLTLNav uses formal logic to automatically identify problems that blind and low-vision users encounter when interacting with websites, catching issues that standard accessibility checkers miss.
Many websites pass static accessibility audits but fail in practice once users begin navigating. A new automated detection system called A11yLTLNav addresses this gap by identifying navigation problems that affect blind and low-vision screen-reader users during real interactions.
The Core Problem#
Static accessibility snapshots often hide problems that emerge only when users interact with a website. Existing automated checkers typically overlook failures related to focus management, interface state changes, and accessible feedback across multiple interactions. This leaves screen-reader users discovering usability barriers through trial and error.
How A11yLTLNav Works#
The approach combines two techniques: it uses random keyboard exploration to navigate websites programmatically, paired with runtime property monitoring to verify behavior against formal logic rules. The system translates accessibility knowledge into reusable checks expressed as Linear Temporal Logic properties—a mathematical framework for describing how systems should behave over time and across action-state transitions.
First, the research organized navigation-related accessibility failures into a structured taxonomy based on prior work, then formalized the observable subset as executable properties that a browser can verify automatically.
Validation Results#
Testing on 31 websites modeled after real-world sites and tasks, A11yLTLNav detected 309 accessibility failures, of which 274 were confirmed by human review. This delivered 88.7% precision and identified more confirmed issues than comparison accessibility checkers. The results demonstrate that translating accessibility principles into time-aware interface checks can catch problems that conventional tools miss.
For more details, see the full research paper on arXiv.

