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
1433-299X
Publication date 2014-05-01
Year available 2013
Sub-type Article (original research)
DOI 10.1007/s00165-012-0272-1
Open Access Status DOI
Volume 26
Issue 3
Start page 563
End page 589
Total pages 27
Place of publication London, United Kingdom
Publisher Springer
Language eng
Subject 1712 Software
2614 Theoretical Computer Science
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.
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
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 4 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 6 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Mon, 05 Aug 2013, 19:40:42 EST by Ms May Balagaize on behalf of School of Information Technol and Elec Engineering