We present a simulation preorder for reactive systems modeled by fair Kripke structures whose transition relation is divided into two parts, internal and external. The first one models the internal behaviour of the system, while the second one is used to model the interaction with an environment. We show that our simulation preorder preserves a substantial subset of $forall CTL^*$. Then, we present an abstraction technique for systems composed by

Time-varying codes associate variable length code words to letters being encoded depending on their positions in the input string. These codes have been introduced in cite{TiME2002} as a proper extension of L-codes. This paper is devoted to a further study of time-varying codes. First, we show that adaptive Huffman encodings are special cases of encodings by time-varying codes. Then, we focus on three kinds of characterization results: characterization

The problem of deciding whether a given workflow net is k-sound for some k>=1 is known as structural soundness. We prove that structural soundness of workflow nets is decidable.

The use of abstraction in the context of abstract data types, is investigated. Properties to be checked are formulas in a first order logic under Kleene's 3-valued interpretation. Abstractions are defined as pairs consisting of a congruence and a predicate interpretation. Three types of abstractions are considered, (forall,forall), (forall,exists), and (exists,forall), and for each of them corresponding property preservation results are established.