부분 차수 축소에 대한 대부분의 논문에서는 분석 할 시스템이 일부 합성 연산자를 사용하는 프로세스 세트로 제공된다고 가정합니다. 상태 공간을 먼저 계산하고 부분 순서 감소를 사용하여 상태 공간을 줄이기를 원하지 않기 때문에 이것은 매우 이해가됩니다.주어진 상태 공간에서 정적 부분 차수 감소
그러나 이미 평면 상태 공간을 제공한다고 가정 할 때 부분 차수 축소를 사용하여 축소 할 수 있습니까? 나는 이것이 수정 된 DFS를 사용하여 가능해야한다고 생각했다. 일부 속성은 로컬에서 확인할 수 있으며 스택의 상태에 대한 정보를 사용하여주기 조건을 고려할 수 있습니다.
이러한 알고리즘이 제시된 논문이나 참고 문헌이 있습니까?
예, 가능합니다. 앞에서 설명한 것처럼이 알고리즘은 기존 방식과 매우 유사합니다. 유일한 차이점은 행동의 독립성에 대한 정보가 수집되는 방식입니다. 개념적으로 이것은 모두 매우 간단합니다. 따라서 그러한 알고리즘에 대한 논문이 없다고 생각합니다.
유즈 케이스의 경우, 이중 자극 최소화가 더 유용합니다. 바이에르 (Baier)와 카토 넨 (Katoen)은 "Model Checking Principles"에서 훌륭한 소개를합니다. 첨단 기술은 강력한 bisimulation을위한 "Paige and Tarjan - Three partition refinement algorithms"과 분기 이등화를위한 "Stuttering Equivalence와 Branching Bisimulation을위한 Groote and Wijs - O (m log n) 알고리즘"에 설명되어 있습니다.