Logical formalism for specification of real-time multiagent systems
D. Yu. Bugaichenko, И. П. Соловьев · Vestnik St Petersburg University Mathematics · 2007
We present logical formalism for specification of multiagent systems, which allows us to formalize explicitly the notion of agent’s action, a nondeterministic method for interaction with environment, a cooperation mechanism of agents, ant time constraints on system reaction. Introducing new constructions for time constraint descriptions and offering thereby the natural formalism for specification of a multiagent system mathematical model, the method extends capabilities of dynamic logic PDL and altering-time temporal logic ATL. The model checking problem for the formalism offered is solvable in polynomial time.