Resource Logics with a Diminishing Resource

2018/06/24 by Alechina, Natasha, Logan, Brian
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1806.11559

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.

Related

• Technical Report: Model-Checking for Resource-Bounded ATL with\n Production and Consumption of Resources
• Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
• Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• On resources and tasks