More Web Proxy on the site http://driver.im/

research-article

Open access

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

Authors:

Brijesh Dongol,

Peter J. RobinsonAuthors Info & Claims

Formal Aspects of Computing, Volume 26, Issue 3

Pages 563 - 589

https://doi.org/10.1007/s00165-012-0272-1

Published: 01 May 2014 Publication History

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.

References

References

[1]

Burns A, Baxter G (2006) Time bands in systems structure, chap 4. In: Besnard D, Gacek C, Jones CB (eds) Structure for dependability: computer-based systems from an interdisciplinary perspective. Springer, London, pp 74–88

[2]

Burns A. and Hayes IJ. A timeband framework for modelling real-time systems Real Time Syst 2010 45 1 106-142

Digital Library

[3]

Back R-JR, Petre L, Porres I (2000) Generalizing action systems to hybrid systems. In: Joseph M (ed) FTRTFT. LNCS, vol 1926. Springer, Berlin, pp 202–213

[4]

Chaochen Z, Ravn AP, Hansen MR (1993) An extended duration calculus for hybrid real-time systems. In: Grossman et al. [GNRR93], pp 36–59

[5]

Dongol B and Hayes IJ Approximating idealised real-time specifications using time bands ECEASST 2012 46 1-16 (11th international workshop on automated verification of critical systems)

[6]

Dongol B, Hayes IJ (2012) Deriving real-time action systems controllers from multiscale system specifications. In: Gibbons, J, Nogueira P (eds) MPC. Lecture notes in computer science, vol 7342. Springer, Berlin, pp 102–131

[7]

Dongol B, Hayes IJ (2012) Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In: Derrick J, Gnesi S, Latella D, Treharne H (eds) IFM. Lecture notes in computer science, vol 7321. Springer, Berlin, pp 39–53

[8]

Emerson EA (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science, vol B. Elsevier Science Publishers, Amsterdam, pp 996–1072

[9]

Fritsch S, Senart A, Schmidt DC, Clarke S (2008) Time-bounded adaptation for automotive system software. In: ICSE ’08: proceedings of the 30th international conference on software engineering, New York, NY, USA. ACM, New York, pp 571–580

[10]

Gargantini A. and Morzenti A. Automated deductive requirements analysis of critical systems ACM Trans Softw Eng Methodol 2001 10 255-307

Digital Library

[11]

Grossman RL, Nerode A, Ravn AP, Rischel H (eds) (1993) Hybrid systems. LNCS, vol 736. Springer, Berlin

[12]

Gubisch G, Steinbauer G, Weiglhofer M, Wotawa F (2008) A teleo-reactive architecture for fast, reactive and robust control of mobile robots. In: IEA/AIE ’08: proceedings of the 21st international conference on industrial, engineering and other applications of applied intelligent systems. Springer, Berlin, pp 541–550

[13]

Hawthorne J, Anthony R (2010) Using a teleo-reactive programming style to develop self-healing applications. In: ACCS. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol 23. Springer, Berlin, pp 114–129

[14]

Hayes IJ (2008) Towards reasoning about teleo-reactive programs for robust real-time systems. In: SERENE ’08: proceedings of the 2008 RISE/EFTS joint international workshop on software engineering for resilient systems, New York, NY, USA. ACM, New York, pp 87–94

[15]

Hayes IJ, Burns A, Dongol B, Jones C (2011) Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, Newcastle University

[16]

Henzinger TA (1996) The theory of hybrid automata. In: LICS’96, Washington, DC, USA. IEEE Computer Society, New York, pp 278–292

[17]

Hoare CAR An axiomatic basis for computer programming Commun ACM 1969 12 10 576-580

Digital Library

[18]

Jones CB. Tentative steps toward a development method for interfering programs ACM Trans Program Lang Syst 1983 5 4 596-619

Digital Library

[19]

Lamport L (1993) Hybrid systems in TLA⁺. In Grossman et al. [GNRR93], pp 77–102

[20]

Lamport L (2002) Specifying systems: the TLA⁺ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc., Boston

[21]

Lewerentz C, Lindner T (eds) (1995) Formal development of reactive systems—case study production cell. LNCS, vol 891. Springer, Berlin

[22]

Lynch N., Segala R., and Vaandraager F. Hybrid I/O automata Inf Comput 2003 185 1 105-157

Digital Library

[23]

Meinicke L, Hayes IJ (2006) Continuous action system refinement. In: Uustalu T (ed) MPC. LNCS, vol 4014. Springer, Berlin, pp 316–337

[24]

Moszkowski BC (1997) Compositional reasoning using interval temporal logic and Tempura. In: de Roever WP, Langmaack H, Pnueli A (eds) COMPOS. Lecture notes in computer science, vol 1536. Springer, Berlin, pp 439–464

[25]

Manna Z, Pnueli A (1992) Temporal verification of reactive and concurrent systems: specification. Springer-Verlag New York, Inc., New York

[26]

Nilsson NJ. Teleo-reactive programs and the triple-tower architecture Electron Trans Artif Intell 2001 5 99-110

[27]

Nafz F, Ortmeier F, Seebach H, Steghöfer JP, Reif W (2009) A universal self-organization mechanism for role-based organic computing systems. In: Reif W, Wang G, Indulska J (eds) ATC. LNCS, vol 5586. Springer, Berlin, pp 17–31

[28]

Rönkkö M., Ravn AP., and Sere K. Hybrid action systems Theor Comput Sci 2003 290 937-973

Digital Library

[29]

Twidle KP, Marinovic S, Dulay N (2010) Teleo-reactive policies in Ponder2. In: POLICY. IEEE Computer Society, New York, pp 57–60

[30]

Zhou C. and Hansen MR. Duration calculus: a formal approach to real-time systems EATCS: monographs in theoretical computer science 2004 Berlin Springer

Cited By

Meinicke LHayes I(2024)Reasoning About Distributive Laws in a Concurrent Refinement AlgebraThe Practice of Formal Methods10.1007/978-3-031-66673-5_1(1-22)Online publication date: 4-Sep-2024
https://doi.org/10.1007/978-3-031-66673-5_1
Durant SWilkins BWoods CUliana EStathis K(2021)Attention Guidance Agents with Eye-TrackingEngineering Multi-Agent Systems10.1007/978-3-030-97457-2_6(92-113)Online publication date: 3-May-2021
https://dl.acm.org/doi/10.1007/978-3-030-97457-2_6
Clark KDongol BRobinson P(2019)Temporal Logic Semantics for Teleo-Reactive Robotic Agent ProgramsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54994-7_19(265-280)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-54994-7_19
Show More Cited By

Index Terms

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

Index terms have been assigned to the content through auto-classification.

Recommendations

Teleo-Reactive abductive logic programs
Logic Programs, Norms and Action

Teleo-reactive (TR) programs are a variety of production systems with a destructively updated database that represents the current state of the environment. They combine proactive behaviour, which is goal-oriented, with reactive behaviour, which is ...
On goal-directed provability in classical logic

One of the key features of logic programming is the notion of goal-directed provability. In intuitionistic logic, the notion of uniform proof has been used as a proof-theoretic characterization of this property. Whilst the connections between ...
A systematic literature review of the Teleo-Reactive paradigm

The Teleo-Reactive approach designed by N. J. Nilsson offers a high-level programming model for the development of reactive systems such as robotic vehicles. Teleo-Reactive programs are written in a way that allows engineers to define behaviour taking ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 26, Issue 3

May 2014

184 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2013.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 May 2014

Accepted: 19 November 2012

Revision received: 01 November 2012

Received: 07 March 2012

Published in FAC Volume 26, Issue 3

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
85
Total Downloads

Downloads (Last 12 months)52
Downloads (Last 6 weeks)6

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Meinicke LHayes I(2024)Reasoning About Distributive Laws in a Concurrent Refinement AlgebraThe Practice of Formal Methods10.1007/978-3-031-66673-5_1(1-22)Online publication date: 4-Sep-2024
https://doi.org/10.1007/978-3-031-66673-5_1
Durant SWilkins BWoods CUliana EStathis K(2021)Attention Guidance Agents with Eye-TrackingEngineering Multi-Agent Systems10.1007/978-3-030-97457-2_6(92-113)Online publication date: 3-May-2021
https://dl.acm.org/doi/10.1007/978-3-030-97457-2_6
Clark KDongol BRobinson P(2019)Temporal Logic Semantics for Teleo-Reactive Robotic Agent ProgramsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54994-7_19(265-280)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-54994-7_19
Sánchez PÁlvarez BAntolinos EFernández DIborra A(2018)A Teleo-Reactive Node for Implementing Internet of Things SystemsSensors10.3390/s1804105918:4(1059)Online publication date: 1-Apr-2018
https://doi.org/10.3390/s18041059
Estivill-Castro VHexel R(2018)Deterministic High-Level Executable Models Allowing Efficient Runtime VerificationModel-Driven Engineering and Software Development10.1007/978-3-319-94764-8_6(119-144)Online publication date: 8-Jul-2018
https://doi.org/10.1007/978-3-319-94764-8_6
Snchez Plvarez BMartnez RIborra A(2017)Embedding statecharts into Teleo-Reactive programs to model interactions between agentsJournal of Systems and Software10.1016/j.jss.2017.05.081131:C(78-97)Online publication date: 1-Sep-2017
https://dl.acm.org/doi/10.1016/j.jss.2017.05.081
Estivill-Castro VHexel RStover J(2015)Modeling, Validation, and Continuous Integration of Software Behaviours for Embedded Systems2015 IEEE European Modelling Symposium (EMS)10.1109/EMS.2015.24(89-95)Online publication date: Oct-2015
https://doi.org/10.1109/EMS.2015.24

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents