Back to Search Start Over

Alternating Tree Automata with Qualitative Semantics

Authors :
Sasha Rubin
Emmanuel Filiot
Aniello Murano
Sophie Pinchinat
Olivier Serre
Shibashis Guha
Bastien Maubert
Nathanaël Fijalkow
Laureline Pinault
Raphaël Berthon
Université libre de Bruxelles (ULB)
Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)
Département d'Informatique [Bruxelles] (ULB)
Faculté des Sciences [Bruxelles] (ULB)
Université libre de Bruxelles (ULB)-Université libre de Bruxelles (ULB)
Tata Institute of Fundamental Research [Bangalore]
University of Naples Federico II = Università degli studi di Napoli Federico II
Université de Lyon
Université de Rennes (UR)
Logic and applications (LOGICA)
LANGAGE ET GÉNIE LOGICIEL (IRISA-D4)
Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA)
Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes)
Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes)
Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA)
Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)
The University of Sydney
Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243))
Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)
Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)
University of Naples Federico II
Università degli studi di Napoli Federico II
Preuves et Langages (PLUME)
Laboratoire de l'Informatique du Parallélisme (LIP)
École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
Université de Rennes 1 (UR1)
Université de Rennes (UNIV-RENNES)
Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP)
Berthon, R.
Fijalkow, N.
Filiot, E.
Guha, S.
Maubert, B.
Murano, A.
Pinault, L.
Pinchinat, S.
Rubin, S.
Serre, O.
École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Source :
ACM Transactions on Computational Logic, ACM Transactions on Computational Logic, 2021, 22 (1), pp.1-24. ⟨10.1145/3431860⟩, ACM Transactions on Computational Logic, Association for Computing Machinery, 2020, 22 (1), ⟨10.1007/s00037-021-00214-1⟩, ACM Transactions on Computational Logic, 2020, 22 (1), ⟨10.1145/3431860⟩
Publication Year :
2020
Publisher :
Association for Computing Machinery (ACM), 2020.

Abstract

We study alternating automata with qualitative semantics over infinite binary trees: Alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this article, we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent non-deterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information. The negative result is the undecidability of the emptiness problem for the case of co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier and the undecidability of the emptiness problem for alternating tree automata with non-zero semantics, a recently introduced probabilistic model of alternating tree automata.

Details

ISSN :
1557945X and 15293785
Volume :
22
Database :
OpenAIRE
Journal :
ACM Transactions on Computational Logic
Accession number :
edsair.doi.dedup.....a29793e85dc009632be016f2eabbf743