A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909225343516672 |
|---|---|
| author | Takata, Yoshiaki Onishi, Akira Senda, Ryoma Seki, Hiroyuki |
| author_facet | Takata, Yoshiaki Onishi, Akira Senda, Ryoma Seki, Hiroyuki |
| contents | Register automaton (RA) is an extension of finite automaton for dealing with data values in an infinite domain. In the previous work, we proposed disjunctive mu$^\downarrow$-calculus, which is a subclass of modal mu-calculus with the freeze quantifier, and showed that it has the same expressive power as RA. However, disjunctive mu$^\downarrow$-calculus is defined as a logic on finite words, whereas temporal specifications in model checking are usually given in terms of infinite words. In this paper, we re-define the syntax and semantics of disjunctive mu$^\downarrow$-calculus to be suitable for infinite words and prove that the obtained temporal logic has the same expressive power as Buchi RA. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_11351 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata Takata, Yoshiaki Onishi, Akira Senda, Ryoma Seki, Hiroyuki Formal Languages and Automata Theory Logic in Computer Science Register automaton (RA) is an extension of finite automaton for dealing with data values in an infinite domain. In the previous work, we proposed disjunctive mu$^\downarrow$-calculus, which is a subclass of modal mu-calculus with the freeze quantifier, and showed that it has the same expressive power as RA. However, disjunctive mu$^\downarrow$-calculus is defined as a logic on finite words, whereas temporal specifications in model checking are usually given in terms of infinite words. In this paper, we re-define the syntax and semantics of disjunctive mu$^\downarrow$-calculus to be suitable for infinite words and prove that the obtained temporal logic has the same expressive power as Buchi RA. |
| title | A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2406.11351 |