On identification of input/output extended automata with finite bisimilar quotients
ACC'09 Proceedings of the 2009 conference on American Control Conference（2009）
摘要
We study the problem of finding a finite bisimilar abstraction for a class of reactive untimed infinite-state systems, modeled as input-output extended finite automata (I/O-EFA). We identify a lower bound abstraction (that is coarser than any finite bisimilar abstraction), and present an iterative refinement algorithm whose termination guarantees the existence of a finite bisimilar abstraction. The termination condition is weaker than the one given in [15] for the existence of a finite bisimilar quotient, and thus, the paper identifies a larger class of I/O-EFAs possessing a finite bisimilar abstraction (than that given in [15]).
更多查看译文
关键词
finite bisimilar quotient,lower bound abstraction,input-output extended finite automaton,termination condition,larger class,finite bisimilar abstraction,iterative refinement algorithm,output extended automaton,reactive untimed infinite-state system,mathematical model,finite automata,software modeling,software verification,logic,probability density function,formal verification,lower bound,input output,automata,concrete,nonlinear systems,computational modeling,encoding,system modeling,data mining,identification,automatic control
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要