Although liveness and fairness have been used for a long time in classical model checking, with process-algebraic methods they have seen far less use. One problem is that it is difficult to combine fairness constraints with the compositionality of process algebra. Here we show how a class of fairness constraints can be applied in a consistent way to processes in the compositional setting. We use only ordinary, but possibly infinite, LTSs as our models of processes. In many cases the infinite LTSs are part of a larger system, which can again be represented as a finite LTS. We show how this finiteness can be recovered, namely, we present an algorithm that checks whether a finite representation exists and, if it does, constructs a finite LTS that is equivalent to the infinite system. Even in the negative case, the system produced by the algorithm is a conservative estimate of the infinite system. Such a finite representation can be placed as a component in further compositional analysis just like any other LTS. © Springer-Verlag Berlin Heidelberg 2005.

Puhakka A.

725.pdf    Gửi cho bạn bè

Từ khóa : Algorithms; Constraint theory; Mathematical models; Parameter estimation; Process engineering; Classical model; Compositional setting; fairness constraints; Process algebra; Algebra