Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/9747
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Dongol, B | - |
dc.contributor.author | Hayes, IJ | - |
dc.contributor.author | Robinson, PJ | - |
dc.date.accessioned | 2015-01-14T13:55:35Z | - |
dc.date.available | 2014 | - |
dc.date.available | 2015-01-14T13:55:35Z | - |
dc.date.issued | 2014 | - |
dc.identifier.citation | Formal Aspects of Computing, 26:3, pp. 563 - 589, 2014 | en_US |
dc.identifier.issn | 0934-5043 | - |
dc.identifier.uri | http://link.springer.com/article/10.1007/s00165-012-0272-1 | - |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/9747 | - |
dc.description.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. © 2013 British Computer Society. | en_US |
dc.language | eng | - |
dc.language.iso | en | en_US |
dc.publisher | Springer-Verlag London Ltd | en_US |
dc.subject | Goal-directed agents | en_US |
dc.subject | Interval-based logics | en_US |
dc.subject | Reactive systems | en_US |
dc.subject | Real-time programs | en_US |
dc.subject | Rely/guarantee reasoning | en_US |
dc.subject | Teleo-reactive programming | en_US |
dc.title | Reasoning about goal-directed real-time teleo-reactive programs | en_US |
dc.type | Article | en_US |
dc.identifier.doi | http://dx.doi.org/10.1007/s00165-012-0272-1 | - |
dc.relation.isPartOf | Formal Aspects of Computing | - |
dc.relation.isPartOf | Formal Aspects of Computing | - |
pubs.organisational-data | /Brunel | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division/College of Engineering, Design and Physical Sciences | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division/College of Engineering, Design and Physical Sciences/Dept of Computer Science | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division/College of Engineering, Design and Physical Sciences/Dept of Computer Science/Computer Science | - |
Appears in Collections: | Electronic and Electrical Engineering |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 368.11 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.