A synthesis of two approaches for verifying finite state concurrent systems. (English) Zbl 0688.68019

Logic at Botik, Proc. Symposium on logical foundations of computer science, Pereslavl-Zalessky/USSR 1989, Lect. Notes Comput. Sci. 363, 81-90 (1989).
[For the entire collection see Zbl 0669.00003.]
The two approaches to prove correctness are based upon temporal logic and on certain automata.
The computation tree logics \(CTL^*\), which combines both branching time and linear time operators, is extended to ECTL; and the CTL model checker of CMU is compared to the COSPAN system of Bell Labs.
Bucchi-, Muller-, L-, and \(\forall\)-automaton are explicitely considered as well as Kripke structures. Fairness is a special topic.
There is a full paper to this journal version.
Reviewer: H.Fuss


68N25 Theory of operating systems
68-04 Software, source code, etc. for problems pertaining to computer science
68Q45 Formal languages and automata


Zbl 0669.00003