On Reachability for Unidirectional Channel Systems Extended with Regular Tests
LOGICAL METHODS IN COMPUTER SCIENCE(2015)
摘要
Unidirectional channel systems (Chambart & Schnoebelen, CONCUR 2008) are finitestate systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equipping them with the possibility of testing regular properties on the contents of channels makes it undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on an elaborate reduction to a generalized version of Post's Embedding Problem.
更多查看译文
关键词
Lossy channel systems,Post Embedding Problem,Automatic verification of programs
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要