3 papers
cs.FL2024
A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata
Yoshiaki Takata, Akira Onishi, Ryoma Senda +1
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-calcul…
cs.FL2022
Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
Yoshiaki Takata, Ryoma Senda, Hiroyuki Seki
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 register…
cs.FL2019
Complexity Results on Register Pushdown Automata
Ryoma Senda, Yoshiaki Takata, Hiroyuki Seki
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 f…