Expressive power and complexity of temporal logics for model-checking

用于模型检查的时序逻辑的表达能力和复杂性

• 批准号: ARC : LX0242359
• 负责人: Dr Jennifer Davoren
• 金额: $ 1.1万
• 依托单位: Australian National University
• 依托单位国家: 澳大利亚
• 项目类别: Linkage - International
• 财政年份: 2002
• 资助国家: 澳大利亚
• 起止时间: 2002-01-01 至 2003-12-31
• 项目状态: 已结题
• 来源: https://researchdata.edu.au/expressive-power-complexity-model-checking/75312
• 关键词: Expressive; power; complexity; temporal; logics

Expressive power and complexity of temporal logics for model-checking. Hardware verification based upon mathematical logic is now routinely\r\nused in industry to verify the correctness of large digital circuits\r\nusing a technique called model-checking. Such discrete systems move\r\nfrom one state to another according to the regular ticks of a clock.\r\nThe challenge now is to find tractable methods for reasoning about\r\nreal-time systems and hybrid systems that move in a continuous manner\r\nwith respect to time: examples include aeroplanes flying according to\r\nthe laws of physics and a moving robot arm. We shall invent new logics\r\nwhich are specifically tailored for tractable reasoning about\r\nreal-time and hybrid systems.

用于模型检验的时态逻辑的表达能力和复杂性。基于数学逻辑的硬件验证现在通常用于工业中，以验证大型数字电路的正确性，使用称为模型检查的技术。这样的离散系统根据时钟的规律从一个状态移动到另一个状态。现在的挑战是找到易于处理的方法，用于推理\r\n实时系统和\r\n相对于时间以连续方式移动的混合系统：例子包括根据物理定律飞行的飞机和移动的机器人手臂。我们将发明新的逻辑，\r\n这些逻辑专门针对\r\n实时和混合系统的易于处理的推理。