An expressive logic for basic process algebra

In this paper we present a branching time temporal logic for Basic Process Algebra. This logic is an enrichment of the branching temporal logic CTL with a branching sequential composition operator, namled chop branching. The logic so obtained is proved to be expressive with respect to the bisimulation semantics delined on BPA_?rec terms, and is able to describe context-free properties of systems.