The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
L'automate de registre (RA) est une extension de l'automate fini en ajoutant des registres stockant des valeurs de données. RA a de bonnes propriétés telles que la décidabilité des membres et les problèmes de vide. Logique temporelle linéaire avec le quantificateur de gel (LTL↓) proposé par Demri et Lazić est un pendant de RA. Cependant, le pouvoir expressif de LTL↓ est trop élevé pour être appliqué à la vérification automatique. Dans cet article, nous proposons une sous-classe de modal µ-calcul avec le quantificateur gel, qui a le même pouvoir expressif que RA. Depuis une conjonction ψ1 ∧ ψ2 dans un LTL général↓ formule ne peut pas être simulée par RA, la sous-classe proposée interdit au moins un des ψ1 et à la ψ2 de contenir le quantificateur de gel ou un opérateur temporel autre que X (suivant). Depuis la sous-classe obtenue de LTL↓ n’a pas la capacité de représenter un cycle dans la PR, nous adoptons µ-calcul sur la sous-classe de LTL↓, qui permet la définition récursive de formules temporelles. Nous fournissons des traductions équivalentes de la sous-classe proposée de µ-calculer à RA et vice versa et prouver leur exactitude.
Yoshiaki TAKATA
Kochi University of Technology
Akira ONISHI
Nagoya University
Ryoma SENDA
Nagoya University
Hiroyuki SEKI
Nagoya University
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Yoshiaki TAKATA, Akira ONISHI, Ryoma SENDA, Hiroyuki SEKI, "A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata" in IEICE TRANSACTIONS on Information,
vol. E106-D, no. 3, pp. 294-302, March 2023, doi: 10.1587/transinf.2022FCP0003.
Abstract: Register automaton (RA) is an extension of finite automaton by adding registers storing data values. RA has good properties such as the decidability of the membership and emptiness problems. Linear temporal logic with the freeze quantifier (LTL↓) proposed by Demri and Lazić is a counterpart of RA. However, the expressive power of LTL↓ is too high to be applied to automatic verification. In this paper, we propose a subclass of modal µ-calculus with the freeze quantifier, which has the same expressive power as RA. Since a conjunction ψ1 ∧ ψ2 in a general LTL↓ formula cannot be simulated by RA, the proposed subclass prohibits at least one of ψ1 and ψ2 from containing the freeze quantifier or a temporal operator other than X (next). Since the obtained subclass of LTL↓ does not have the ability to represent a cycle in RA, we adopt µ-calculus over the subclass of LTL↓, which allows recursive definition of temporal formulas. We provide equivalent translations from the proposed subclass of µ-calculus to RA and vice versa and prove their correctness.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2022FCP0003/_p
Copier
@ARTICLE{e106-d_3_294,
author={Yoshiaki TAKATA, Akira ONISHI, Ryoma SENDA, Hiroyuki SEKI, },
journal={IEICE TRANSACTIONS on Information},
title={A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata},
year={2023},
volume={E106-D},
number={3},
pages={294-302},
abstract={Register automaton (RA) is an extension of finite automaton by adding registers storing data values. RA has good properties such as the decidability of the membership and emptiness problems. Linear temporal logic with the freeze quantifier (LTL↓) proposed by Demri and Lazić is a counterpart of RA. However, the expressive power of LTL↓ is too high to be applied to automatic verification. In this paper, we propose a subclass of modal µ-calculus with the freeze quantifier, which has the same expressive power as RA. Since a conjunction ψ1 ∧ ψ2 in a general LTL↓ formula cannot be simulated by RA, the proposed subclass prohibits at least one of ψ1 and ψ2 from containing the freeze quantifier or a temporal operator other than X (next). Since the obtained subclass of LTL↓ does not have the ability to represent a cycle in RA, we adopt µ-calculus over the subclass of LTL↓, which allows recursive definition of temporal formulas. We provide equivalent translations from the proposed subclass of µ-calculus to RA and vice versa and prove their correctness.},
keywords={},
doi={10.1587/transinf.2022FCP0003},
ISSN={1745-1361},
month={March},}
Copier
TY - JOUR
TI - A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata
T2 - IEICE TRANSACTIONS on Information
SP - 294
EP - 302
AU - Yoshiaki TAKATA
AU - Akira ONISHI
AU - Ryoma SENDA
AU - Hiroyuki SEKI
PY - 2023
DO - 10.1587/transinf.2022FCP0003
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E106-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 2023
AB - Register automaton (RA) is an extension of finite automaton by adding registers storing data values. RA has good properties such as the decidability of the membership and emptiness problems. Linear temporal logic with the freeze quantifier (LTL↓) proposed by Demri and Lazić is a counterpart of RA. However, the expressive power of LTL↓ is too high to be applied to automatic verification. In this paper, we propose a subclass of modal µ-calculus with the freeze quantifier, which has the same expressive power as RA. Since a conjunction ψ1 ∧ ψ2 in a general LTL↓ formula cannot be simulated by RA, the proposed subclass prohibits at least one of ψ1 and ψ2 from containing the freeze quantifier or a temporal operator other than X (next). Since the obtained subclass of LTL↓ does not have the ability to represent a cycle in RA, we adopt µ-calculus over the subclass of LTL↓, which allows recursive definition of temporal formulas. We provide equivalent translations from the proposed subclass of µ-calculus to RA and vice versa and prove their correctness.
ER -