In this paper we present a logic to provide a framework for the formal specification of multiagent real-time systems which allows explicit reasoning about the actions of agents, the nondeterministic model of interaction between agents and environment, the cooperation and competition of agents and the reaction time limits of a system. The logic combines Propositional Dynamic Logic PDL and Alternating-time Temporal Logic ATL and extends the formalism with reaction time constraints. We introduce a multiagent system abstract model and show how the logic can be used to specify the model properties.
展开▼
