Persistent sets

Abstract

The first technique for computing the set of transitions T to consider in a selective search actually corresponds to a whole family of algorithms lOve81, Va191, GW91b] that have been proposed independently by several researchers. In this chapter, we show that all these algorithms actually compute persistent sets, and compare them with each other. Then we present an algorithm that generalizes the previous ones in a sense that will be given later. 4.1 Definition Persistent sets were introduced in [GP93]. Intuitively, a subset T of the set of tran-sitions enabled in a state s of Aa is called persistent in s if all transitions not in T that are enabled in s, or in a state reachable from s through transitions not in T, are independent with all transitions in T. In other words, whatever one does from s, while remaining outside of T, does not interact with or affect T. Formally, we have the following. Definition 4.1 A set T of transitions enabled in a state s is persistent in s iff, for all nonempty sequences of transitions t I t 2 tn--1 tn S ~-S 1 ~ S 2 ~ $3... ~ S n ~ Sn+ 1 from s in Aa and including only transitions ti fL T, 1 < i