In: Philippi, Stephan: Fachberichte Informatik, No. 7-2000: 7. Workshop Algorithmen und Werkzeuge für Petrinetze, 2.-3. Oktober 2000, Koblenz, Germany, pages 75-80. Universität Koblenz-Landau, Institut für Informatik, October 2000.
Abstract: We define an extension of CTL in which we are able to quantify over a selectable set of next states and use transition formulae to limit the range of quantifiers in temporal operators. We present ideas of the implementation and show some applications.