Australian National University
Current approaches to analyzing dynamic systems are mostly grounded in propositional (temporal) logics. As a consequence, they often lack expressivity for modeling rich data structures and reasoning about them in the course of a computation. To address this problem, the authors propose a rich modeling framework based on first-order logic over background theories (arithmetic's, lists, records, etc) and state transition systems over corresponding interpretations. On the reasoning side, they introduce a tableau calculus for bounded model checking of properties expressed in a certain fragment of CTL over that first-order logic.