用形式化语言LTL(linear temporal logic)离线测试系统。程序SystemMonitor采用系统运行在线测试，本程序采用离线测试。输入为系统运行数据和LTL表达式，输出为该系统的鲁棒特征值。本程序采用了动态程序设计方法。对从事系统验证工作的开发人员和研究人员非常有帮助。-Its very useful for researchers and programmers who are working on system control and verification. it i