Resource Logics with a Diminishing Resource

TL;DR

This paper introduces a new assumption of a diminishing resource in resource logics, such as time, which makes previously undecidable model-checking problems decidable under certain conditions.

Contribution

It proposes a realistic assumption of a diminishing resource that simplifies the computational complexity of resource logics, enabling decidability in cases previously undecidable.

Findings

Model-checking becomes decidable with a diminishing resource.

Undecidability issues are resolved under the new assumption.

Applicable to resources like time that cannot be produced.

Abstract

Model-checking resource logics with production and consumption of resources is a computationally hard and often undecidable problem. We introduce a simple and realistic assumption that there is at least one diminishing resource, that is, a resource that cannot be produced and every action has a non-zero cost on this resource. An example of such resource is time. We show that, with this assumption, problems that are undecidable even for the underlying Alternating Time Temporal Logic, such as model-checking under imperfect information and perfect recall, become decidable for resource logics with a diminishing resource.