Model Checking Resource Bounded Systems with Shared Resources via Alternating B\"uchi Pushdown Systems

TL;DR

This paper studies the decidability of model checking resource-bounded multiagent systems with shared resources, showing undecidability with multiple resources but decidability with a single shared resource through automata-based techniques.

Contribution

It proves that model checking is undecidable with multiple resources but decidable with a single shared resource, using reductions to alternating B"uchi pushdown systems.

Findings

Model checking is undecidable with two or more unbounded resources.

Model checking is decidable with a single shared resource.

Decidability is established via automata-theoretic reductions.

Abstract

It is well known that the verification of resource-constrained multiagent systems is undecidable in general. In many such settings, resources are private to agents. In this paper, we investigate the model checking problem for a resource logic based on Alternating-Time Temporal Logic (ATL) with shared resources. Resources can be consumed and produced up to any amount. We show that the model checking problem is undecidable if two or more of such unbounded resources are available. Our main technical result is that in the case of a single shared resource, the problem becomes decidable. Although intuitive, the proof of decidability is non-trivial. We reduce model checking to a problem over alternating B\"uchi pushdown systems. An intermediate result connects to general automata-based verification: we show that model checking Computation Tree Logic (CTL) over (compact) alternating B\"uchi pushdown systems is decidable.