Publications

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

Authors
Simon Busard, Charles Pecheur
Tags
,
Title
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
Authors
Simon Busard, Charles Pecheur
gandalf2017.pdf Δ   247Kb   28 May 2020
Type
In Proceedings
Book title
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, Roma, Italy, 20-22 September 2017
Series
Electronic Proceedings in Theoretical Computer Science
Volume
256
Pages
253-267
Publisher
Open Publishing Association
Editor
Patricia Bouyer, Andrea Orlandini, Pierluigi San Pietro
Year
2017

Abstract

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 are the ones the agents can effectively play by only looking at what they observe from the current state. ATL_ir can be seen as the core logic to reason about such uniform strategies. Nevertheless, its model-checking problem is difficult (it requires a polynomial number of calls to an NP oracle), and practical algorithms to solve it appeared only recently.

This paper proposes a technique for model checking uniform memoryless strategies. Existing techniques build the strategies from the states of interest, such as the initial states, through a forward traversal of the system. On the other hand, the proposed approach builds the winning strategies from the target states through a backward traversal, making sure that only uniform strategies are explored. Nevertheless, building the strategies from the ground up limits its applicability to constrained reachability objectives only. This paper describes the approach in details and compares it experimentally with existing approaches implemented into a BDD-based framework. These experiments show that the technique is competitive on the cases it can handle.

Tags Tags: ,

BibTeX Record
  @INPROCEEDINGS{lvl-2017-815241,
    TITLE = {A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability},
    AUTHOR = {Simon Busard and Charles Pecheur},
    YEAR = {2017},
    VOLUME = {256},
    PAGES =  {253-267},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {Patricia Bouyer and Andrea Orlandini and Pierluigi San Pietro},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/ABackward-traversal-basedApproachForSymbolicModelCheckingOfUniformStrategiesForConstrainedReachability},
  }