Towards Agents-Based Model Checking

A new logic, agents-indexed computation tree logic (ACTL), is obtained from the standard computation tree logic CTL by adding some agent operators. ACTL is intended to appropriately formalize reasoning about agents-based (or distributed) concurrent systems within an executable temporal logic by model checking. The model-checking, validity and satisfiability problems of ACTL are shown to be decidable.