Abstract: This paper introduces an object-oriented modeling language based on concurrently executing and communicating objects. A logical framework to formally design object systems and prove their properties will be briefly presented. This framework is based on a local and system logics which are variants of linear temporal logic. In order to prove system properties, we have developed tableau methods (with decision procedures) for both levels. Unlike other decision methods for checking satisfiability or validity, who construct the full set of all possible states of the satisfaction graph, these algorithms construct only those states reachable by the system (or object) from its initial state and satisfying the formula to be checked.