The Model-Checking Problem for Resource-Bounded Logics

Photograph of Berndt Muller

Berndt Muller

(University of Glamorgan)

The modelling and verification of multi-agent systems has attracted much attention in recent years. The vast majority of the literature neglects resource requirements. However, the availability of resources is essential for the success in achieving many goals. Some logics have been augmented with notions of resources and resource consumption or production. The talk introduces resource-bounded logics and asks the question whether it is possible to retain the decidability of model checking. We investigate the limits of what can be verified about resource-bounded agents by considering several variations and prove that the model-checking problem is usually undecidable, with the exception of bounded or otherwise restrictive models. The results extend previous work on Resource-Bounded Tree Logics RTL and RTL*, based on the well-known Computation Tree Logics CTL and CTL*.
Thursday 10th February 2011, 14:00
Video Conferencing Room - Far134
Department of Computer Science