文章基本信息

标题：Compositional Model Checking of Real Time Systems
本地全文：下载
作者：Francois Laroussinie ; Kim G. Larsen
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1995
卷号：2
期号：19
出版社：Aarhus University
摘要：A major problem in applying model checking to finite-state systems is the potential combinatorial explosion of the state space arising from parallel composition. Solutions of this problem have been attempted for practical applications using a variety of techniques. Recent work by Andersen [And95] proposes a very promising compositional model checking technique, which has experimentally been shown to improve results obtained using Binary Decision Diagrams. In this paper we make Andersen's technique applicable to systems described by networks of timed automata. We present a quotient construction, which allows timed automata components to be gradually moved from the network expression into the specification. The intermediate specifications are kept small using minimization heuristics suggested by Andersen. The potential of the combined technique is demonstrated using a prototype implemented in CAML.