Extensional equivalences for transition systems (Q1098303)

The aim of the paper is comparing some of the notions of equivalence of concurrent and nondeterministic systems defined in the literature. Almost all the equivalences are based on the idea that two systems are equivalent whenever no external observation can distinguish them, as what is of interest is the effect of a system on the environment and its reactions to stimuli from the environment. In order to study interrelationships between notions which have been introduced for a number of CCS-like languages, the author adapts all the equivalences to the case of `labelled transition systems' (LTS). LTS model the behavior of machines which accept symbols from an external environment so to allow discussing their reaction to external experiments. String equivalence, observational equivalence, Kennaway's equivalence, Darondeau's equivalence and failure equivalence are reformulated for LTS, discussed and related to the equivalence generated by a new preorder on transition systems. Finally testing equivalence is presented. The idea is that of considering two processes equivalent with respect to a set of relevant tests if they pass exactly the same tests. The difficulty of proving in this framework that two processes are equivalent suggests to the author an alternative characterization of testing equivalence that is independent from the notion of observer and is based on the (finite or infinite) sequences of actions each system may perform and the set of actions the system must accept. This new characterization allows understanding the interrelationship with the equivalences analyzed before.