Key points are not available for this paper at this time.
Die Unterschiede zwischen und die Angemessenheit von verzweigter versus linearer zeitlicher Logik zur Argumentation über konkurrierende Programme werden untersucht. Diese Themen wurden zuvor von Lamport betrachtet. Um eine sorgfältige Prüfung dieser Themen zu erleichtern, wird eine Sprache, CTL*, definiert, in der ein universeller oder existenzieller Pfadquantor eine beliebige lineare Zeitbehauptung voranstellen kann. Die Ausdruckskraft mehrerer Untersprachen wird dann verglichen. CTL* steht auch in Beziehung zu den Logiken MPL von Abrahamson und PL von Harel, Kozen und Parikh. Das Papier schließt mit einem Vergleich des Nutzens von verzweigter und linearer zeitlicher Logik.
Emerson et al. (Do,) haben diese Frage untersucht.