하이퍼속성은 개별 실행을 고립적으로 추론하는 것이 아니라 여러 실행 흔적을 연결하여 전통적인 흔적 속성을 일반화합니다. 이는 정보 흐름 및 강건성 속성과 같은 중요한 요구 사항을 표현하는 통합된 방법을 제공합니다. HyperLTL과 같은 시공간 논리는 시스템의 실행에 대해 명시적으로 양화하는 방식으로 이러한 속성을 포착합니다. 그러나, 실제로 관련된 많은 하이퍼속성은 양화사 교대를 포함하며, 이러한 특징은 자동 검증에 상당한 도전을 제기합니다. 완전한 검증 방법은 각 양화사 교대를 위해 시스템 보완을 요구하므로 실제로는 실행 가능하지 않습니다. 더 저렴한 (그러나 불완전한) 방법은 HyperLTL 공식을 보편적 및 존재적 양화사 간의 2인 게임으로 해석합니다. 게임 기반 접근은 상당히 저렴하며, 대화형 증명을 촉진하고, 만족의 증명서를 쉽게 확인할 수 있게 합니다. 그러나 이는 ^*^* 속성에 제한되어 있으며, 중요한 속성은 도달할 수 없습니다. 본 논문에서는 부분 정보 하의 다인 게임을 활용하여 임의의 양화사 교대를 갖는 하이퍼속성을 검증할 수 있음을 보여줍니다. 부분 정보 하의 게임은 일반적으로 결정 불가능하지만, 우리는 우리의 게임이 계층적 정보 하에서 진행되며 따라서 결정 가능한 게임 클래스에 속함을 보여줍니다. 우리는 게임의 완전성에 대해 논의하고 부분 정보 설정에서 예언 변수에 대해 연구합니다.
Beutner et al. (Sat,)는 이 질문을 연구했습니다.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: