A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability

Since the introduction of Alternating-time Temporal Logic (ATL), many logics have been proposed to reason about different strategic capabilities of the agents of a system. In particular, some logics have been designed to reason about the uniform memoryless strategies of such agents. These strategies...

Full description

Bibliographic Details
Main Authors: Simon Busard, Charles Pecheur
Format: Article
Language:English
Published: Open Publishing Association 2017-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1709.02106v1