The first part of the chapter is dedicated to extend the notion of concurrent game structures by adding weights to actions so that taking some action may produce or consume resources. Alternating-time temporal logics ATL(r) with r resource types are introduced as well as its counterparts ATL+(r) and ATL*(r). The satisfaction relation is designed so that strategies witnessing the satisfaction of formulae whose outermost connective is a strategy modality should guarantee that the proponent coalition stays within the budget, assuming an initial budget. The treatment of the resource availabilities is analogous to what is done in energy games. We show that slightly deviating from this energy semantics can lead to undecidability. Then, we introduce the energy parity game problem and we provide its main complexity results from the literature. To show that ATL* with resources admits a model-checking problem in 2EXPTIME, we reduce its core model-checking problem to the energy parity game problem. Furthermore, we discuss several variants of ATL(r), typically those admitting some idle action, those assuming the proponent restriction condition or those admitting infinite supplies as initial budget value. For all these variant logics that are used in the literature, we demonstrate that there is no essential complexity differences with the version of ATL(r) studied in this chapter. The chapter concludes by stating a few results about the model-checking problem for ATL+ with one resource.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On Resources: the Energy Viewpoint

  • Stéphane Demri

摘要

The first part of the chapter is dedicated to extend the notion of concurrent game structures by adding weights to actions so that taking some action may produce or consume resources. Alternating-time temporal logics ATL(r) with r resource types are introduced as well as its counterparts ATL+(r) and ATL*(r). The satisfaction relation is designed so that strategies witnessing the satisfaction of formulae whose outermost connective is a strategy modality should guarantee that the proponent coalition stays within the budget, assuming an initial budget. The treatment of the resource availabilities is analogous to what is done in energy games. We show that slightly deviating from this energy semantics can lead to undecidability. Then, we introduce the energy parity game problem and we provide its main complexity results from the literature. To show that ATL* with resources admits a model-checking problem in 2EXPTIME, we reduce its core model-checking problem to the energy parity game problem. Furthermore, we discuss several variants of ATL(r), typically those admitting some idle action, those assuming the proponent restriction condition or those admitting infinite supplies as initial budget value. For all these variant logics that are used in the literature, we demonstrate that there is no essential complexity differences with the version of ATL(r) studied in this chapter. The chapter concludes by stating a few results about the model-checking problem for ATL+ with one resource.