Finite transition systems. Semantics of communicating systems. Transl. from French by John Plaice. (Systèmes de transitions finis et sémantique de processus communicants). (English) Zbl 0796.68141

Prentice Hall International Series in Computer Science. Hemel Hempstead: Prentice Hall. Paris: Masson, 177 p. $ 60.00 /hc (1994).
Finite transition systems form one of the formalisms used to describe systems of processes. The term transition system is used to better show that the fundamental concept of automata are formal systems containing states \((s\in S)\) and transitions \((t\in T)\), rather than machines to recognize certain languages. Transition used here is labeled by action or event name. A labeled transition system is a quintuple \((S,T,\alpha,\beta,\lambda)\), where \((S,T,\alpha,\beta)\) is a transition system and \(\lambda\) is a mapping from set \(T\) of transitions to set \(A\) taking each transition \(t\) to its label \(\lambda(t)\). A label of a transition indicates the action or the event which triggers the transition. Transition \(t\) can be designed by the triple (source state \(\mapsto\) action/event \(\to\) target state). The relations between transition systems and Petri nets respectively process algebras are shown. After introduction of the synchronous product of transition systems different transition system logics are described (propositional logic, linear temporal logic, Wolper logic, Hennessy-Milner logic, Dicky logic and computation tree logic (CTL)).
The major problem of semantics of systems of processes is that of their equivalence. The author expressed, that the question of equivalence has two parts: what are the criteria to be taken into consideration to affirm that two systems are equivalent and how is the equivalence relation between systems defined formally. Different ways for proof of equivalence are discussed.
The final chapter gives an overview to software tools for verification of transition systems properties and for comparison of transition systems, either using the language to describe processes like simply transition systems, or higher level languages, such as process algebras, or protocol description languages such as ESTELLE or LOTUS, or real-time languages such as ESTEREL or LUSTRE.
This book also gives an good insight into French work in this area.
Reviewer: H.Stahn (Dresden)


68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68-02 Research exposition (monographs, survey articles) pertaining to computer science
03B70 Logic in computer science