English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Strategy Logic with imperfect information (SLiR) is a very expressive logicdesigned to express complex properties of strategic abilities in distributedsystems. Previous work on SLiR focused on finite systems, and showed that themodel-checking problem is decidable when information on the control states ofthe system is hierarchical among the players or components of the system,meaning that the players or components can be totally ordered according totheir respective knowledge of the state. We show that moving from finite toinfinite systems generated by collapsible (higher-order) pushdown systemspreserves decidability, under the natural restriction that the stack content isvisible. The proof follows the same lines as in the case of finite systems, butrequires to use (collapsible) alternating pushdown tree automata. Such automataare undecidable, but semi-alternating pushdown tree automata were introducedand proved decidable, to study a strategic problem on pushdown systems with twoplayers. In order to tackle multiple players with hierarchical information, werefine further these automata: we define direction-guided (collapsible)pushdown tree automata, and show that they are stable under projection,nondeterminisation and narrowing. For the latter operation, used to deal withimperfect information, stability holds under some assumption that is satisfiedwhen used for systems with visible stack. We then use these automata to proveour main result.

Reasoning about strategies on collapsible pushdown arenas with imperfect information