Reasoning about goal-directed real-time teleo-reactive programs

Dongol, Brijesh, Hayes, Ian J. and Robinson, Peter J. (2014) Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26 3: 563-589. doi:10.1007/s00165-012-0272-1

Related Publications and Datasets
  • Prolog Data Collection (deposited 02-08-2012)
Author Dongol, Brijesh
Hayes, Ian J.
Robinson, Peter J.
Title Reasoning about goal-directed real-time teleo-reactive programs
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 0934-5043
Publication date 2014-05
Year available 2013
Sub-type Article (original research)
DOI 10.1007/s00165-012-0272-1
Open Access Status
Volume 26
Issue 3
Start page 563
End page 589
Total pages 27
Place of publication London, United Kingdom
Publisher Springer
Collection year 2014
Language eng
Formatted abstract
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.
Keyword Teleo reactive programming
Goal directed agents
Rely/guarantee reasoning
Real time programs
Reactive systems
Interval-based logics
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ
Additional Notes Published online: 08 Jan 2013

Document type: Journal Article
Sub-type: Article (original research)
Collections: Official 2014 Collection
School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 1 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Mon, 05 Aug 2013, 09:40:42 EST by Ms May Balagaize on behalf of School of Information Technol and Elec Engineering