The Hybrid -Calculus

Abstract

We present an ExpTime decision procedure for the full - Calculus (including converse programs) extended with nominals and a universal program, thus devising a new, highly expressive ExpTime logic. The decision procedure is based on tree automata, and makes explicit the problems caused by nominals and how to overcome them. Roughly speak- ing, we show how to reason in a logic lacking the tree model property using techniques for logics with the tree model property. The contribu- tion of the paper is two-fold: we extend the family of ExpTime logics, and we present a technique to reason in the presence of nominals.