Modeling Fuzzy Behaviours in Concurrent Systems

The behaviour of concurrent systems has been classically specified by means of Labelled Transition Systems. Uncertainty can be modeled in LTS by means of non-determinism that can be used for modeling systems whose behaviour is not completely specified or for specifying unpredictable behaviours like, for instance, errors. However, such approach is not completely satisfactory. Indeed, it is not able to give a measure of such uncertainty. In this paper we propose a new variant of LTS, named Fuzzy Labelled Transition Systems (FLTS), where fuzziness is used for modeling uncertainty in concurrent systems. In FLTS, transition relation is defined in term of a L-Fuzzy Set that gives the membership degree of a given transition/computation. To reason about FLTS, a variant of Hennessy-Milner Logic is also proposed. The proposed logic will be used for specifying behavioural properties of systems for which a measure of the satisfaction is defined.