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

Brookes, Stephen D.; Rounds, William C.

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

MSC:

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

Keywords:

descriptive power; programming logics; elementary equivalence relations; nondeterministic state transition systems; propositional dynamic logic; Hennessy-Milner logic; regular trace logic; behavioural specifications for concurrent programs; bisimilarity; Milnor’s observation equivalence; failure equivalence; trace equivalence

Citations:

Zbl 0511.00030