Model Checking Real-Time Value-Passing Systems  

作　　者：JingChen Zi-NingCao 

机构地区：[1]LaboratoryforComputerScience,InstituteofSoftware,TheChineseAcademyofSciences,Beijing100080P.R.China

出　　处：《Journal of Computer Science & Technology》2004年第4期459-471,共13页计算机科学技术学报（英文版）

基　　金：国家自然科学基金

摘　　要：In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.

关 键 词：model checking REAL-TIME value-passing timed predicate μ-calculus 

分 类 号：TP274[自动化与计算机技术—检测技术与自动化装置]