Infinite-state high-level MCS: Model-checking and realizability: (Extended abstract)
International Congress of Mathematicans(2002)
摘要
We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.
更多查看译文
关键词
state machine,model checking
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络