This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of (...) the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning (...) about branching time. (shrink)

ABSTRACT A complete axiomatic system CTLrp is introduced for a temporal logic for finitely branching ω+ -trees in a language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTLrp. In particular, that yields a complete axiomatization for the translations of all valid CTL*-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for (...) reasoning about branching time. (shrink)

This article appraises efforts by the National University of Lesotho (NUL) to provide continuing professional development for lecturers. The findings of a previous study suggested that the majority of lecturers at this university were not trained as teachers, and that this could negatively impact on their teaching. The establishment of a staff academic development centre was long overdue. In April 2014, the university established the Centre for Teaching and Learning (CTL). Drawing on a constructivist perspective, a qualitative approach was adopted (...) to explore the current situation. The findings indicate that efforts to roll out continuing professional development for lecturers have not borne any significant results. The problem is exacerbated by a lack of support from the university community as well as lecturers’ poor attendance at the staff academic development workshops hosted by the CTL. It is thus recommended that management put mechanisms in place to support the centre and ensure compulsory staff participation. (shrink)