Behavioural equivalence relations induced by programming logics. (English) Zbl 0536.68042

Automata, languages and programming, 10th Colloq., Barcelona/Spain 1983, Lect. Notes Comput. Sci. 154, 97-108 (1983).
[For the entire collection see Zbl 0511.00030.]
This paper compares the descriptive power of three programming logics by examining the elementary equivalence relations induced on nondeterministic state transition systems by these logics. These three comprise propositional dynamic logic introduced by Fischer and Ladner, Hennessy-Milner logic and a new logic called regular trace logic intended for study on behavioural specifications for concurrent programs. The authors consider, besides the elementary equivalence relations mentioned above, the notions of bisimilarity of Park and Ogden, Milnor’s observation equivalence, failure equivalence and trace equivalence.
Reviewer: H.Nishimura


68Q65 Abstract data types; algebraic specification
03B60 Other nonclassical logic
68Q60 Specification and verification (program logics, model checking, etc.)


Zbl 0511.00030