Model Checking ATL* on vCGS
Logic in Computer Science
2019-03-12 v1
Abstract
We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model checking ATL* on iCGS.
Cite
@article{arxiv.1903.04350,
title = {Model Checking ATL* on vCGS},
author = {Francesco Belardinelli and Catalin Dima and Ioana Boureanu and Vadim Malvone},
journal= {arXiv preprint arXiv:1903.04350},
year = {2019}
}
Related papers
View all related →
Logic in Computer Science · Computer Science
Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
Catalin Dima, Ferucio Laurentiu Tiplea
2011-02-22
Logic in Computer Science · Computer Science
Model Checking Strategic Abilities in Information-sharing Systems
Francesco Belardinelli, Ioana Boureanu, Catalin Dima, Vadim Malvone
2022-04-20
Logic in Computer Science · Computer Science
Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
Steen Vester
2014-09-22
Logic in Computer Science · Computer Science
Decidability results for ATL* with imperfect information and perfect recall
Raphaël Berthon, Bastien Maubert, Aniello Murano
2018-09-05
Logic in Computer Science · Computer Science
CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics
Falke B. Ø. Carlsen, Lars Bo P. Frydenskov, Nicolaj Ø. Jensen, Jener Rasmussen +4
2023-10-03
Computer Science and Game Theory · Computer Science
Alternating-time temporal logic with finite-memory strategies
Steen Vester
2013-07-18
Computer Science and Game Theory · Computer Science
Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics
Rodica Bozianu, Catalin Dima, Constantin Enea
2013-10-28
Logic in Computer Science · Computer Science
On the Expressiveness and Complexity of ATL
Francois Laroussinie, Nicolas Markey, Ghassan Oreiby
2015-07-01
Logic in Computer Science · Computer Science
ATLsc with partial observation
François Laroussinie, Nicolas Markey, Arnaud Sangnier
2015-09-25
Logic in Computer Science · Computer Science
Realizability Problem for Constraint LTL
Ashwin Bhaskar, M. Praveen
2022-07-15
Logic in Computer Science · Computer Science
Model-checking an Epistemic \mu-calculus with Synchronous and Perfect Recall Semantics
Rodica Bozianu, Cătălin Dima, Constantin Enea
2012-07-17
Logic in Computer Science · Computer Science
Satisfiability of ATL with strategy contexts
François Laroussinie, Nicolas Markey
2013-07-18
Artificial Intelligence · Computer Science
Making Agents' Abilities Explicit
Yedi Zhang, Fu Song, Taolue Chen
2018-11-28
Logic in Computer Science · Computer Science
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen +1
2021-11-24
Artificial Intelligence · Computer Science
Relaxing Exclusive Control in Boolean Games
Francesco Belardinelli, Umberto Grandi, Andreas Herzig, Dominique Longin +3
2017-07-28
Logic in Computer Science · Computer Science
Scalar and Vectorial mu-calculus with Atoms
Bartek Klin, Mateusz Łełyk
2023-06-22
Logic in Computer Science · Computer Science
ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
Sofia Garcia de Blas Garcia-Alcalde, Francesco Belardinelli
2025-10-22
Logic in Computer Science · Computer Science
Robust Verification of Concurrent Stochastic Games
Angel Y. He, David Parker
2026-01-22
Logic in Computer Science · Computer Science
On Reducing Linearizability to State Reachability
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2015-05-26
Logic in Computer Science · Computer Science
Rational Capability in Concurrent Games
Yinfeng Li, Emiliano Lorini, Munyque Mittelmann
2025-02-19
Multiagent Systems · Computer Science
Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information
Angelo Ferrando, Vadim Malvone
2023-06-19
Multiagent Systems · Computer Science
Model Checking of vGOAL
Yi Yang, Tom Holvoet
2024-06-26
Logic in Computer Science · Computer Science
Model Checking Resource Bounded Systems with Shared Resources via Alternating B\"uchi Pushdown Systems
Nils Bulling, Hoang Nga Nguyen
2015-08-17
Logic in Computer Science · Computer Science
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
Angelo Ferrando, Vadim Malvone
2023-06-19
Logic in Computer Science · Computer Science
Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems
Deren Lin, Tianrong Lin
2025-07-02