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
Le système pushdown de registre (RPDS) est une extension du système pushdown (PDS) qui dispose de registres pour traiter les valeurs de données. Une méthode de vérification de modèle LTL pour les RPDS avec des évaluations régulières a été proposée dans des travaux antérieurs ; cependant, la méthode nécessite que les automates de registre (RA) utilisés pour définir une évaluation régulière soient déterministes en arrière. Cet article propose une autre approche du même problème, dans laquelle le problème de vérification de modèle pour RPDS est réduit à celui pour PDS en construisant une bisimulation PDS équivalente à un RPDS donné. Cette construction est plus simple que la méthode de vérification de modèle précédente et ne nécessite pas d'AR déterministe ou rétro-déterministe, et l'équivalence de bisimulation garantit clairement l'exactitude de la réduction. D'un autre côté, la méthode proposée nécessite que chaque RPDS (et RA) ait la propriété de fraîcheur, dans laquelle chaque fois que le RPDS met à jour un registre avec une valeur de données non stockée dans aucun registre ou dans le sommet de la pile, la valeur doit être fraîche. Cet article montre également que le problème de vérification de modèle avec des valuations régulières définies par le RA général est indécidable, et donc la contrainte de fraîcheur est essentielle dans la méthode proposée.
Yoshiaki TAKATA
Kochi University of Technology
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, Ryoma SENDA, Hiroyuki SEKI, "Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking" in IEICE TRANSACTIONS on Information,
vol. E105-D, no. 9, pp. 1620-1623, September 2022, doi: 10.1587/transinf.2022EDL8030.
Abstract: Register pushdown system (RPDS) is an extension of pushdown system (PDS) that has registers for dealing with data values. An LTL model checking method for RPDS with regular valuations has been proposed in previous work; however, the method requires the register automata (RA) used for defining a regular valuation to be backward-deterministic. This paper proposes another approach to the same problem, in which the model checking problem for RPDS is reduced to that problem for PDS by constructing a PDS bisimulation equivalent to a given RPDS. This construction is simpler than the previous model checking method and does not require RAs deterministic or backward-deterministic, and the bisimulation equivalence clearly guarantees the correctness of the reduction. On the other hand, the proposed method requires every RPDS (and RA) to have the freshness property, in which whenever the RPDS updates a register with a data value not stored in any register or the stack top, the value should be fresh. This paper also shows that the model checking problem with regular valuations defined by general RA is undecidable, and thus the freshness constraint is essential in the proposed method.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2022EDL8030/_p
Copier
@ARTICLE{e105-d_9_1620,
author={Yoshiaki TAKATA, Ryoma SENDA, Hiroyuki SEKI, },
journal={IEICE TRANSACTIONS on Information},
title={Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking},
year={2022},
volume={E105-D},
number={9},
pages={1620-1623},
abstract={Register pushdown system (RPDS) is an extension of pushdown system (PDS) that has registers for dealing with data values. An LTL model checking method for RPDS with regular valuations has been proposed in previous work; however, the method requires the register automata (RA) used for defining a regular valuation to be backward-deterministic. This paper proposes another approach to the same problem, in which the model checking problem for RPDS is reduced to that problem for PDS by constructing a PDS bisimulation equivalent to a given RPDS. This construction is simpler than the previous model checking method and does not require RAs deterministic or backward-deterministic, and the bisimulation equivalence clearly guarantees the correctness of the reduction. On the other hand, the proposed method requires every RPDS (and RA) to have the freshness property, in which whenever the RPDS updates a register with a data value not stored in any register or the stack top, the value should be fresh. This paper also shows that the model checking problem with regular valuations defined by general RA is undecidable, and thus the freshness constraint is essential in the proposed method.},
keywords={},
doi={10.1587/transinf.2022EDL8030},
ISSN={1745-1361},
month={September},}
Copier
TY - JOUR
TI - Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
T2 - IEICE TRANSACTIONS on Information
SP - 1620
EP - 1623
AU - Yoshiaki TAKATA
AU - Ryoma SENDA
AU - Hiroyuki SEKI
PY - 2022
DO - 10.1587/transinf.2022EDL8030
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E105-D
IS - 9
JA - IEICE TRANSACTIONS on Information
Y1 - September 2022
AB - Register pushdown system (RPDS) is an extension of pushdown system (PDS) that has registers for dealing with data values. An LTL model checking method for RPDS with regular valuations has been proposed in previous work; however, the method requires the register automata (RA) used for defining a regular valuation to be backward-deterministic. This paper proposes another approach to the same problem, in which the model checking problem for RPDS is reduced to that problem for PDS by constructing a PDS bisimulation equivalent to a given RPDS. This construction is simpler than the previous model checking method and does not require RAs deterministic or backward-deterministic, and the bisimulation equivalence clearly guarantees the correctness of the reduction. On the other hand, the proposed method requires every RPDS (and RA) to have the freshness property, in which whenever the RPDS updates a register with a data value not stored in any register or the stack top, the value should be fresh. This paper also shows that the model checking problem with regular valuations defined by general RA is undecidable, and thus the freshness constraint is essential in the proposed method.
ER -