Publications

Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints

Authors
Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi
Tags
,
Title
Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints
Authors
Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
Type
In Proceedings
Book title
Formal Methods and Software Engineering
Series
Lecture Notes in Computer Science
Volume
8829
Pages
27-42
Publisher
Springer International Publishing
Editor
Stephan Merz, Jun Pang
Year
2014

Abstract

Reasoning about strategies has been a concern for several years, and many extensions of Alternating-time Temporal Logic have been proposed. One extension, ATLK_irF , allows the user to reason about the strategies of the agents of a system under partial observability and unconditional fairness constraints. However, the existing model-checking algorithm for ATLK_irF is inefficient when the user is only interested in the satisfaction of a formula in a small subset of states, such as the set of initial states of the system. We propose to generate fewer strategies by only focusing on partial strategies reachable from this subset of states, reducing the time needed to perform the verification. We also describe several practical improvements to further reduce the verification time and present experiments showing the practical impact of the approach.

Tags Tags: ,

BibTeX Record
  @INPROCEEDINGS{lvl-2014-825257,
    TITLE = {Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints},
    AUTHOR = {Simon Busard and Charles Pecheur and Hongyang Qu and Franco Raimondi},
    YEAR = {2014},
    VOLUME = {8829},
    PAGES =  {27-42},
    PUBLISHER = {Springer International Publishing},
    EDITOR = {Stephan Merz and Jun Pang},
    SERIES = {Lecture Notes in Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/ImprovingTheModelCheckingOfStrategiesUnderPartialObservabilityAndFairnessConstraints},
  }