국내 최대 기계 및 로봇 연구정보

기술보고서

기술보고서 게시판 내용
타이틀	Model-Checking with Edge-Valued Decision Diagrams
저자	Roux, Pierre;; Siminiceanu, Radu I.
Keyword	AEROSPACE SYSTEMS;; ALGORITHMS;; ARITHMETIC;; CODING;; FORMALISM;; FUNCTIONS (MATHEMATICS); IDENTITIES;; LIBRARIES
URL	http://hdl.handle.net/2060/20100024139
보고서번호	NASA/CR-2010-216710
발행년도	2010
출처	NTRS (NASA Technical Report Server)
ABSTRACT	We describe an algebra of Edge-Valued Decision Diagrams (EVMDDs) to encode arithmetic functions and its implementation in a model checking library along with state-of-the-art algorithms for building the transition relation and the state space of discrete state systems. We provide efficient algorithms for manipulating EVMDDs and give upper bounds of the theoretical time complexity of these algorithms for all basic arithmetic and relational operators. We also demonstrate that the time complexity of the generic recursive algorithm for applying a binary operator on EVMDDs is no worse than that of Multi-Terminal Decision Diagrams. We have implemented a new symbolic model checker with the intention to represent in one formalism the best techniques available at the moment across a spectrum of existing tools: EVMDDs for encoding arithmetic expressions, identity-reduced MDDs for representing the transition relation, and the saturation algorithm for reachability analysis. We compare our new symbolic model checking EVMDD library with the widely used CUDD package and show that, in many cases, our tool is several orders of magnitude faster than CUDD.