전환 시스템의 카운터 루프 - Z3

Question

Z3의 PDR 엔진을 사용하여 전환 시스템의 불변 조건을 증명합니다. 전환 시스템에 특정 상태에 도달하기 위해 통과해야하는 카운터 루프가 포함되어 있으면 성능이 느립니다.

다음 소스 코드에서 Z3 Fixedpoint Homepage에 전환 시스템 파이썬 클래스로 구현 된 3 가지 상태와 3 가지 전환을 포함하는 전환 시스템의 예를 볼 수 있습니다. 마지막 줄에는 상태 L0에서 시작하여 상태 L2에 도달하는 쿼리가 있습니다. 따라서 천이 t2는 y 번 통과해야합니다.

y == 10으로 초기화하면 답이 빨리 계산됩니다. 하지만 초기화 y == 1000 성능이 느립니다.

L0 = L.L0 
L1 = L.L1 
L2 = L.L2 
y=Int('y') 
i = Int('i') 
state = Const('state', L) 

t1 = { "guard" : state == L0, 
    "effect" : [ L1, i ] } 
t2 = { "guard" : And(state == L1), 
    "effect" : [ L1, i+1 ] } 
t3 = { "guard" : And(state == L1,i>y), 
    "effect" : [ L2, i]} 

ptr = TransitionSystem(And(state == L0, i == 0, y==10),[t1, t2, t3],[state, i]) 
ptr.query(state==L2) 

더 나은 성능을 얻기 위해 Z3으로 L0에서 L2 로의 경로를 계산할 가능성이 있습니까?

Answer 1

예를 들어 현재 Z3에서 더 빠른 접근법이 없습니다. Z3의 구현은 펼치기 깊이에 걸쳐 (동일한) 속성을 밀어 넣으려고 시도 할 때 카운터 예제 루프의 깊이가 깊이에 대략 2 차 오버 헤드를 소비합니다.

일반적으로 Z3의 PDR 엔진은 계획 문제에 적합하지 않은 입니다. 흔적이 없다는 것을 확증하면 다소 더 좋습니다.