Nothing Special   »   [go: up one dir, main page]

IEICE Transactions on Information and Systems
Online ISSN : 1745-1361
Print ISSN : 0916-8532
Special Section on Foundations of Computer Science — Foundations of Computer Science Supporting the Information Society —
A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata
Yoshiaki TAKATAAkira ONISHIRyoma SENDAHiroyuki SEKI
Author information
JOURNAL FREE ACCESS

2023 Volume E106.D Issue 3 Pages 294-302

Details
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.

Content from these authors
© 2023 The Institute of Electronics, Information and Communication Engineers
Previous article Next article
feedback
Top