Reasoning about goal-directed real-time teleo-reactive programs
Reasoning about goal-directed real-time teleo-reactive programs
复制标题
关于目标导向的实时远程反应程序的推理
DOI：
--
复制
发表时间：
2013
影响因子：
1
通讯作者：
P. Robinson
中科院分区：
文献类型：
--
作者：
Brijesh Dongol;I. Hayes;P. Robinson
目的反应编程模型是开发支持层次组合和持续动作的实时系统的高级方法。该模型与动作系统、时间自动机和TLA+等框架不同，它允许程序更加紧凑，并描述其预期行为。Teleo反应程序是特别有用的实现控制器的自主代理，必须作出有力的反应，他们的动态变化的环境。在本文中，我们开发了一个实时的逻辑，是基于持续时间演算，并使用这种逻辑来形式化的语义teleo反应程序。我们开发的依赖/保证规则，促进推理的程序及其环境中的组合方式。我们提出了几个定理，简化证明的teleo反应程序，并提出了一个部分机械化的方法证明目标导向代理的进展性质。
The teleo-reactive programming model is a high-level approach to developing real-time systems that supports hierarchical composition and durative actions. The model is different from frameworks such as action systems, timed automata and TLA+, and allows programs to be more compact and descriptive of their intended behaviour. Teleo-reactive programs are particularly useful for implementing controllers for autonomous agents that must react robustly to their dynamically changing environments. In this paper, we develop a real-time logic that is based on Duration Calculus and use this logic to formalise the semantics of teleo-reactive programs. We develop rely/guarantee rules that facilitate reasoning about a program and its environment in a compositional manner. We present several theorems for simplifying proofs of teleo-reactive programs and present a partially mechanised method for proving progress properties of goal-directed agents.