Show description

Since Rψ does not contain edges out-going from nodes where ψ1 is not satisfied, then (K, x) |= ψ1 for all x in πl , except at most wr , and CTL Model-Checking with Graded Quantifiers 25 therefore each πl is an evidence of ψ1 Uψ2 . Thus (K, s) |= ψ. Now, let π0 , . . , πk be k + 1 distinct finite paths connecting s to nodes where ψ2 holds; from the definition of Gψ , πi is an evidence of ψ1 Uψ2 for all 0 ≤ i ≤ k, and therefore (K, s) |= ψ, as well. (only if ): If (K, s) |= E >k ψ1 Uψ2 then obviously (K, s) |= E >0 ψ1 Uψ2 , therefore s ∈ Sψ .

T. ψ ← True; end Our algorithm considers the graph (S , R ), subgraph of K, of the states where the formula E >0 ψ1 Uψ2 holds (without the edges outgoing from states where ψ1 doesn’t hold), and adds a new destination node d with incoming edges from all the nodes where ψ2 holds (the capacity of the link (s, d) is the in-degree of s, while the remaining edges have capacity 1). g. [CLRS01]. However, it is easy to see that in our network the maximum flow from a node s to d is equal to the maximum number of edge-disjoint paths from s to the set {t ∈ S \ {d} | (t, d) ∈ R }, therefore our algorithm has only to evaluate the maximum flow from each state to d.

Journal of Algorithms 48(1), 239–256 (2003) 32 A. Ferrante, M. Napoli, and M. : Counterexamples revisited: Principles, algorithms, applications. In: Verification: Theory and Practice, pp. : Model checking and evidence exploration. In: ECBS, pp. : In so many possible worlds. : Graded CTL. : The two–variable guarded fragment with transitive relations. In: LICS, pp. : Two–variable logic with counting is decidable. In: LICS, pp. : Qualifying number restrictions in concept languages. In: KR, pp. : The model checker SPIN.