ﻻ يوجد ملخص باللغة العربية
Quite some work in the ATL-tradition uses the differences between various types of strategies (positional, uniform, perfect recall) to give alternative semantics to the same logical language. This paper contributes to another perspective on strategy types, one where we characterise the differences between them on the syntactic (object language) level. This is important for a more traditional knowledge representation view on strategic content. Leaving differences between strategy types implicit in the semantics is a sensible idea if the goal is to use the strategic formalism for model checking. But, for traditional knowledge representation in terms of object language level formulas, we need to extent the language. This paper introduces a strategic STIT syntax with explicit operators for knowledge that allows us to charaterise strategy types. This more expressive strategic language is interpreted on standard ATL-type concurrent epistemic game structures. We introduce rule-based strategies in our language and fruitfully apply them to the representation and characterisation of positional and uniform strategies. Our representations highlight crucial conditions to be met for strategy types. We demonstrate the usefulness of our work by showing that it leads to a critical reexamination of coalitional uniform strategies.
As a contribution to the challenge of building game-playing AI systems, we develop and analyse a formal language for representing and reasoning about strategies. Our logical language builds on the existing general Game Description Language (GDL) and
In asynchronous games, Melli{`e}s proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e.
Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to ac
Concurrent strategies based on event structures are examined from the viewpoint of may and must testing in traditional process calculi. In their pure form concurrent strategies fail to expose the deadlocks and divergences that can arise in their comp
We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining the Pareto front. We focus on strategies that are easy to employ