← All problems
Unverified

Paired Counter Automata

Consider a DFA AA together with dd pairs off counters (x1,y1),…,(xd,yd)(x_1,y_1),\dots,(x_d,y_d). Each transition of AA is labelled with an update function for all counters. The update functions for the x-counters are id:n→nid:n\rightarrow n and ++:n→n+1++ : n\rightarrow n+1. The update function for the y-counters are id:n→nid:n\rightarrow n, ×2:n→2n\times 2:n\rightarrow 2n and ×2+1:n→2n+1\times 2+1:n\rightarrow 2n+1. An accepting configuration is a configuration in which we are in an accepting state and all the counter pairs have the same value, i.e. x1=y1,…,xd=ydx_1=y_1,\dots,x_d=y_d. Question: is the emptiness problem for this class of automata decidable?

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu