论文部分内容阅读
介绍了一种基于自动机理论的参数化LTL（parameterized LTL（1inear temporal logic），简称PALTL）公式运行时预测监控器构造方法．一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念，从语法层面保证公式中参数化变量的正确绑定（binding）和使用（using）；另一方面给出参数化预测监控器的概念．它由静态和动态两部分组成，静态部分由参数化Biichi自动机表示，动态部分为当前状态处的变量赋值．在系统运行过程中，预测监控器基于静态部分的参数化Bii