시각 장애 및 저시력(BLV) 스크린 리더 사용자의 경우, 정적 스냅샷에서는 접근 가능해 보이는 웹사이트라도 상호작용이 시작되면 탐색하기 어렵거나 불가능할 수 있습니다. 그러나 대부분의 자동화된 접근성 검사기는 상호작용 전반에 걸친 포커스(focus), 인터페이스 상태(interface state), 그리고 접근 가능한 피드백(accessible feedback)과 관련된 실패를 놓칩니다. 본 논문에서는 접근성 내비게이션 실패를 자동으로 감지하는 속성 기반 접근 방식인 A11yLTLNav를 제시합니다. 선행 연구에 대한 구조화된 검토를 통해, 우리는 접근성 내비게이션 실패를 실패 분류 체계(failure taxonomy)로 정리하고, 브라우저에서 관찰 가능한 부분집합을 액션-상태 추적(action-state traces)에 대한 실행 가능한 Linear Temporal Logic 속성으로 형식화합니다. A11yLTLNav는 무작위 키보드 탐색과 런타임 속성 모니터링을 결합하여 상호작용 중 이러한 실패를 감지합니다. 우리는 실제 웹사이트와 작업을 기반으로 생성된 31개의 웹사이트에 대해 A11yLTLNav를 평가했습니다. 이 시스템은 총 309개의 접근성 실패를 보고했으며, 그중 274개가 확인되었고, 이는 88.7%의 정밀도(precision)를 달성하며 비교 검사기보다 더 많은 확인된 실패를 식별했습니다. 우리의 결과는 A11yLTLNav가 접근성 지식을 시간 경과에 따른 인터페이스 동작의 재사용 가능한 검사로 변환시킨다는 것을 보여줍니다.