Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs | Springer Nature Link
Advertisement
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs
Conference paper
First Online:
13 August 2020
pp 265–280
Cite this conference paper
Formal Methods. FM 2019 International Workshops
(FM 2019)
Abstract
Teleo-Reactive (
TR
) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a
TR
programmed robotic agent has a deductive
Belief Store
comprising constantly changing predicate logic
percept
facts, and
knowledge
facts and rules for querying the percepts. In this paper we introduce
TR
programming using a simple example expressed in the teleo-reactive programming language
TeleoR
, which is a syntactic extension of
QuLog
, a typed logic programming language used for the agent’s
Belief Store
. We give a formal definition of the
regression
property that rules of
TeleoR
procedures should satisfy, and an informal operational semantics of the evaluation of a
TeleoR
procedure call. We then formally express key features of the evaluation in LTL. Finally we show how this LTL formalisation can be used to prove that a procedure’s rules satisfy the regression property by proving it holds for one rule of the example
TeleoR
program. The proof requires us: to formally link a
TeleoR
agent’s percept beliefs with sensed configurations of the external environment; to link the agent’s robotic device
action intentions
with actual robot actions; to specify the eventual physical effects of the robot’s actions on the environment state.
Dongol is supported by EPSRC Grants EP/R019045/2, EP/R032556/1 and EP/R025134/2.
This is a preview of subscription content,
log in via an institution
to check access.
Access this chapter
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Chapter
EUR 29.95
Price includes VAT (France)
eBook
EUR 42.79
Price includes VAT (France)
Softcover Book
EUR 52.74
Price includes VAT (France)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Institutional subscriptions
Similar content being viewed by others
Combining Model Checking and Runtime Verification for Safe Robotics
Chapter
Agent-Based Control of Robot Behavior Using Reasoning Language Models
Article
01 February 2025
Incorporating Monitors in Reactive Synthesis Without Paying the Price
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Logic in AI
Formal Logic
Linear Logic
Rehabilitation Robotics
Social Robotics
Symbolic AI
Formal Verification Techniques for Software Systems
Notes
1.
QuLog
actually has another rule type, imperative action rules for defining multi-threaded agent behaviour. They can call primitive actions for forking threads, updating
Belief Store
facts and message communication. The two thread architecture is implemented using these action rules.
2.
Of course, in reality, there are environments that could impede a robot’s motion—we do not make any claims about correctness of our implementation for such environments. In a full development, one would need to make sure that the physical environment in which a verified robot operates does indeed conform to any assumptions made in the proof.
References
Clark, K.L., Robinson, P.J.: Robotic agent programming in TeleoR. In: Proceedings of International Conference of Robotics and Automation. IEEE (2015)
Google Scholar
Clark, K.L., Robinson, P.J.: Chapter 3: introduction to QuLog. In: Programming Communicating Robotic Agents: A Multi-tasking Teleo-Reactive Approach. Springer (2020). (To appear)
Google Scholar
Dongol, B., Hayes, I.J.: Rely/Guarantee reasoning for teleo-reactive programs over multiple time bands. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 39–53. Springer, Heidelberg (2012).
Chapter
Google Scholar
Dongol, B., Hayes, I.J., Robinson, P.J.: Reasoning about goal-directed real-time teleo-reactive programs. Formal Asp. Comput.
26
(3), 563–589 (2014).
Article
MathSciNet
MATH
Google Scholar
Jones, J., Roth, D.: Robot Programming: A Practical Guide to Behavior-based Robotics. McGraw-Hill, New York (2004)
Google Scholar
Kamali, M., Linker, S., Fisher, M.: Modular verification of vehicle platooning with respect to decisions, space and time. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 18–36. Springer, Cham (2019).
Chapter
Google Scholar
Levesque, H.: Thinking as Computation. MIT Press, Cambridge (2012)
Book
Google Scholar
Mataric, M.J.: The Robotics Primer. MIT Press, Cambridge (2007)
Google Scholar
Quigley, M., et al.: ROS: an open-source Robot Operating System (2009).
www.robotics.stanford.edu/~ang/papers/icraoss09-ROS.pdf
Download references
Acknowledgements
We thank our anonymous FMAS reviewers for their careful readings of this paper and comments, which have helped improve quality overall.
Author information
Authors and Affiliations
Imperial College London, London, UK
Keith Clark
University of Surrey, Guildford, UK
Brijesh Dongol
University of Queensland, Brisbane, Australia
Peter Robinson
Authors
Keith Clark
View author publications
Search author on:
PubMed
Google Scholar
Brijesh Dongol
View author publications
Search author on:
PubMed
Google Scholar
Peter Robinson
View author publications
Search author on:
PubMed
Google Scholar
Corresponding author
Correspondence to
Brijesh Dongol
Editor information
Editors and Affiliations
McMaster University, Hamilton, ON, Canada
Emil Sekerinski
University of Porto, Porto, Portugal
Nelma Moreira
University of Minho, Braga, Portugal
José N. Oliveira
Argo Ai, Munich, Germany
Daniel Ratiu
University of Pisa, Pisa, Italy
Riccardo Guidotti
University of Liverpool, Liverpool, UK
Marie Farrell
University of Liverpool, Liverpool, UK
Matt Luckcuck
University of Exeter, Exeter, UK
Diego Marmsoler
University of Minho, Braga, Portugal
José Campos
University of Newcastle, Newcastle upon Tyne, UK
Troy Astarte
Claude Bernard University, Lyon, France
Laure Gonnord
Nazarbayev University, Nur-Sultan, Kazakhstan
Antonio Cerone
University of Surrey, Guildford, UK
Luis Couto
University of Surrey, Guildford, UK
Brijesh Dongol
University of Giessen, Giessen, Germany
Martin Kutrib
University of Lisbon, Lisbon, Portugal
Pedro Monteiro
Airbus Operations S.A.S., Toulouse, France
David Delmas
Rights and permissions
Reprints and permissions
Copyright information
About this paper
Cite this paper
Clark, K., Dongol, B., Robinson, P. (2020). Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs.

In: Sekerinski, E.,
et al.
Formal Methods. FM 2019 International Workshops. FM 2019. Lecture Notes in Computer Science(), vol 12232. Springer, Cham. https://doi.org/10.1007/978-3-030-54994-7_19
Download citation
.RIS
.ENW
.BIB
DOI
Published
13 August 2020
Publisher Name
Springer, Cham
Print ISBN
978-3-030-54993-0
Online ISBN
978-3-030-54994-7
eBook Packages
Computer Science
Computer Science (R0)
Springer Nature Proceedings Computer Science
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Publish with us
Policies and ethics
Profiles
Brijesh Dongol
View author profile
Access this chapter
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Chapter
EUR 29.95
Price includes VAT (France)
eBook
EUR 42.79
Price includes VAT (France)
Softcover Book
EUR 52.74
Price includes VAT (France)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Institutional subscriptions