Abstract:
The study of situated systems that are capable of reactive and goal-directed behaviour has received increased attention in recent years. One important class are the so-called agent-oriented systems, which model the system as a rational agent with certain mental attitudes that determine its decision-making and acting capabilities. This approach has led to the development of expressive, but computationally intractable, logics for describing or specifying the behaviours of situated systems. In this paper, we present three propositional variants of such logics, with different expressive power, and analyze the computational complexity of verifying if a given property is satisfied by a given abstract situated program. The linear time and polynomial time complexity of the verification algorithms for two of these logics provides encouraging results with respect to the practical use of such logics for verifying situated systems.