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

Clarke, E. M.; Grumberg, O.; Kurshan, R. P.

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

MSC:

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

Keywords:

concurrent systems; temporal logic; automata; computation tree logics

Citations:

Zbl 0669.00003