arXiv subjects

Ryoma Senda

Publications and source records attributed to Ryoma Senda.

3 recordsLinked to original sources

arXiv2024

A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata

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.

cs.FL↗

arXiv2022

Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking

Pushdown systems (PDS) are known as an abstract model of recursive programs, and model checking methods for PDS have been studied. Register PDS (RPDS) are PDS augmented by registers to deal with data values from an infinite domain in a restricted way. A linear temporal logic (LTL) model checking method for RPDS with regular valuations has been proposed; however, the method requires the register automata (RA) used for representing 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. The construction in the proposed method 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 this 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 this model checking problem with regular valuations defined by general RA is undecidable, and thus the freshness constraint is essential in the proposed method.

cs.FL↗

arXiv2019

Complexity Results on Register Pushdown Automata

Register pushdown automata (RPDA) is an extension of classical pushdown automata to handle data values in a restricted way. RPDA attracts attention as a model of a query language for structured documents with data values. The membership and emptiness problems for RPDA are known to be EXPTIME-complete. This paper shows the membership problem becomes PSPACE-complete and NP-complete for nondecreasing and growing RPDA, respectively, while the emptiness problem remains EXPTIME-complete for these subclasses.

cs.FL↗