"Unidirectional channel systems" (Chambart & Schnoebelen, CONCUR 2008) arefinite-state systems where one-way communication from a Sender to a Receivergoes via one reliable and one unreliable unbounded fifo channel. Whilereachability is decidable for these systems, equipping them with thepossibility of testing regular properties on the contents of channels makes itundecidable. Decidability is preserved when only emptiness and nonemptinesstests are considered: the proof relies on an elaborate reduction to ageneralized version of Post's Embedding Problem.
展开▼
